#5953

src/model/model.h

@@ -81,6 +81,8 @@ class model : public model_core {
     expr_ref get_inlined_const_interp(func_decl* f, bool force_inline);
     expr_ref unfold_as_array(expr* e);
 
+    void set_inline() { m_inline = true; }
+
     //
     // Primitives for building models
     //

src/qe/mbp/mbp_arith.cpp

@@ -68,6 +68,8 @@ namespace mbp {
             DEBUG_CODE(expr_ref val(m);
             eval(lit, val);
             CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";);
+            if (m.is_false(val))
+                return false;
             SASSERT(m.limit().is_canceled() || !m.is_false(val)););
 
             if (!m.inc())
@@ -291,6 +293,7 @@ namespace mbp {
             model_evaluator eval(model);
             TRACE("qe", tout << model;);
             eval.set_model_completion(true);
+            model.set_inline();
             compute_def |= m_apply_projection;
 
             opt::model_based_opt mbo;

src/qe/mbp/mbp_plugin.cpp

@@ -98,6 +98,7 @@ namespace mbp {
     bool project_plugin::reduce(model_evaluator& eval, model& model, expr* fml, expr_ref_vector& fmls) {
         expr* nfml, * f1, * f2, * f3;
         expr_ref val(m);
+        model.set_inline();
         if (m.is_not(fml, nfml) && m.is_distinct(nfml))
             push_back(fmls, pick_equality(m, model, nfml));
         else if (m.is_or(fml)) {