diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 753ec37da..3c3b6e884 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -490,6 +490,8 @@ namespace euf {
             apply_solver(m_qsolver);
         if (num_nodes < m_egraph.num_nodes()) 
             return sat::check_result::CR_CONTINUE;
+        if (cont)
+            return sat::check_result::CR_CONTINUE;
         TRACE("after_search", s().display(tout););
         if (give_up)
             return sat::check_result::CR_GIVEUP;
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index cb5144a2b..2d8ac8afd 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -605,7 +605,9 @@ namespace q {
         }
         if (propagate(true))
             return true;
-        return m_inst_queue.lazy_propagate();
+        if (m_inst_queue.lazy_propagate())
+            return true;
+        return false;
     }
 
     void ematch::collect_statistics(statistics& st) const {