From 6d8daacdecc84bafbb7c493aeeccfe5660d19d43 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Oct 2014 08:35:05 -0700
Subject: [PATCH] fix check for satisfiability before calling final_check

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qe.cpp | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index e573508bb..192d97c3b 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -1451,10 +1451,15 @@ namespace qe {
             if (assumption) m_solver.assert_expr(assumption);
             bool is_sat = false;   
             lbool res = l_true;
-            while (res == l_true) {
+            while (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);