From 1352aa06f3e9683da2ed411d574474f64bf73ee7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 20 Sep 2021 12:08:04 -0700
Subject: [PATCH] #5532

---
 src/sat/smt/euf_solver.cpp | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index f4438a63c15..56e3b93b606 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)