diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp
index 76dd2c5b7..7d078476f 100644
--- a/src/sat/smt/synth_solver.cpp
+++ b/src/sat/smt/synth_solver.cpp
@@ -96,14 +96,12 @@ namespace synth {
     }
 
     sat::check_result solver::check() {
-        // TODO: need to know if there are quantifiers to instantiate
-        if (m_solved.size() < m_synth.size()) {
-            IF_VERBOSE(2, ctx.display(verbose_stream()));
+        if (m_synth.empty())
             return sat::check_result::CR_DONE;
-        }
-        if (!compute_solutions())
-            return sat::check_result::CR_GIVEUP;
-        return sat::check_result::CR_CONTINUE;
+        
+        SASSERT(m_solved.size() < m_synth.size());
+        IF_VERBOSE(2, ctx.display(verbose_stream()));
+        return sat::check_result::CR_GIVEUP;        
     }
 
     // display current state (eg. current set of realizers)
@@ -118,6 +116,13 @@ namespace synth {
         return alloc(solver, ctx);
     }
 
+    void solver::asserted(sat::literal lit) {
+        // lit corresponds to a Boolean output variable.
+        // it is asserted.
+        // assume that we attach this theory to such Boolean output variables.
+    }
+
+
     void solver::on_merge_eh(euf::enode* root, euf::enode* other) {
 
         auto is_computable = [&](euf::enode* n) { return !contains_uncomputable(n->get_expr()) || m_is_computable.get(n->get_root_id(), false); };
diff --git a/src/sat/smt/synth_solver.h b/src/sat/smt/synth_solver.h
index 0b0c99521..ab2cf3208 100644
--- a/src/sat/smt/synth_solver.h
+++ b/src/sat/smt/synth_solver.h
@@ -24,7 +24,7 @@ namespace synth {
     public:
         solver(euf::solver& ctx);
         ~solver() override;        
-        void asserted(sat::literal lit) override {}
+        void asserted(sat::literal lit) override;
         sat::check_result check() override;
         void push_core() override {}
         void pop_core(unsigned n) override {}