diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index f4438a63c..56e3b93b6 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -479,16 +479,17 @@ namespace euf {
             if (s().inconsistent())
                 return sat::check_result::CR_CONTINUE;
         }
-        if (m_qsolver) 
-            apply_solver(m_qsolver);
 
-	if (s().inconsistent())
+
+        if (s().inconsistent())
             return sat::check_result::CR_CONTINUE;
         if (cont)
             return sat::check_result::CR_CONTINUE;
+        if (m_qsolver)
+            apply_solver(m_qsolver);
         if (num_nodes < m_egraph.num_nodes()) {
             IF_VERBOSE(1, verbose_stream() << "new nodes created, but not detected\n");
-            return sat::check_result::CR_CONTINUE;           
+            return sat::check_result::CR_CONTINUE;
         }
         TRACE("after_search", s().display(tout););
         if (give_up)