fix #4104

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 27, 2020 · 6d4bd37 · 6d4bd37
1 parent fc1321f
commit 6d4bd37
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
@@ -1460,10 +1460,10 @@ namespace qe {
             if (assumption) m_solver.assert_expr(assumption);
             bool is_sat = false;   
             lbool res = l_true;
-            if (has_uninterpreted(m_fml))
-                res = l_undef;
             while (res == l_true) {
                 res = m_solver.check();
+                if (res == l_true && has_uninterpreted(m_fml))
+                    res = l_undef;
                 if (res == l_true) {
                     is_sat = true;
                     final_check();