diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index 7275ff71f..aa6287030 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -1453,8 +1453,13 @@ namespace qe {
             lbool res = l_true;
             while (res == l_true) {
                 res = m_solver.check();
-                if (res == l_true) is_sat = true;
-                final_check();
+                if (res == l_true) {
+                    is_sat = true;
+                    final_check();
+                }
+                else {
+                    break;
+                }
             }
             if (res == l_undef) {
                 free_vars.append(num_vars, vars);