#5532

Z3Prover · Sep 20, 2021 · 1352aa0 · 1352aa0
1 parent 0170f1f
commit 1352aa0
Showing 1 changed file with 5 additions and 4 deletions.
diff --git 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)