From 7cb6f41d0a00b19f5b834feedc207b1b640a7add Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 18 Mar 2020 11:15:15 -0700
Subject: [PATCH] fix #3390

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qe_arith.cpp |  2 +-
 src/qe/qe_mbp.cpp   | 10 ++++++----
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp
index fa2871a85..d46bdde5a 100644
--- a/src/qe/qe_arith.cpp
+++ b/src/qe/qe_arith.cpp
@@ -65,7 +65,7 @@ namespace qe {
             DEBUG_CODE(expr_ref val(m); 
                        eval(lit, val); 
                        CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";);
-                       SASSERT(m.is_true(val)););
+                       SASSERT(m.canceled() || m.is_true(val)););
 
             TRACE("opt", tout << mk_pp(lit, m) << " " << a.is_lt(lit) << " " << a.is_gt(lit) << "\n";);
             bool is_not = m.is_not(lit, lit);
diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index 366d70075..07a65563a 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -528,7 +528,7 @@ public:
         preprocess_solve(model, vars, fmls);
         filter_variables(model, vars, fmls, unused_fmls);
         project_bools(model, vars, fmls);
-        while (progress && !vars.empty() && !fmls.empty()) {
+        while (progress && !vars.empty() && !fmls.empty() && m.limit().inc()) {
             app_ref_vector new_vars(m);
             progress = false;
             for (project_plugin * p : m_plugins) {
@@ -536,7 +536,7 @@ public:
                     (*p)(model, vars, fmls);
                 }
             }
-            while (!vars.empty() && !fmls.empty()) {                
+            while (!vars.empty() && !fmls.empty() && m.limit().inc()) {
                 var = vars.back();
                 vars.pop_back();
                 project_plugin* p = get_plugin(var);
@@ -547,7 +547,7 @@ public:
                     new_vars.push_back(var);
                 }
             }
-            if (!progress && !new_vars.empty() && !fmls.empty() && force_elim) {
+            if (!progress && !new_vars.empty() && !fmls.empty() && force_elim && m.limit().inc()) {
                 var = new_vars.back();
                 new_vars.pop_back();
                 expr_safe_replace sub(m);
@@ -564,7 +564,9 @@ public:
                     }
                 }            
                 progress = true;
-            }
+            }        
+            if (!m.limit().inc()) 
+                return;
             vars.append(new_vars);
             if (progress) {
                 preprocess_solve(model, vars, fmls);