From 0bdb2f16910779f02af3d401cb589c11f847743f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 2 Sep 2022 18:03:56 -0700
Subject: [PATCH] add verbose=1 log for mbp failure

---
 src/qe/mbp/mbp_arith.cpp  | 10 ++++++++--
 src/qe/mbp/mbp_plugin.cpp |  4 +++-
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
index 79f931d5096..a886a5a7075 100644
--- a/src/qe/mbp/mbp_arith.cpp
+++ b/src/qe/mbp/mbp_arith.cpp
@@ -215,6 +215,7 @@ namespace mbp {
                     linearize(mbo, eval, mul, t3, c, fmls, ts, tids);
                 }
                 else {
+                    IF_VERBOSE(1, verbose_stream() << "mbp failed on if: " << mk_pp(t, m) << " := " << val << "\n");
                     throw default_exception("mbp evaluation didn't produce a truth value");
                 }
             }
@@ -234,8 +235,10 @@ namespace mbp {
             else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) {
                 rational r;
                 val = eval(t);
-                if (!a.is_numeral(val, r))
+                if (!a.is_numeral(val, r)) {
+                    IF_VERBOSE(1, verbose_stream() << "mbp failed on " << mk_pp(t, m) << " := " << val << "\n");
                     throw default_exception("mbp evaluation didn't produce an integer");
+                }
                 c += mul * r;
 
                 rational c0(-r), mul0(1);
@@ -335,8 +338,10 @@ namespace mbp {
                     expr_ref val = eval(v);
                     if (!m.inc())
                         return false;
-                    if (!a.is_numeral(val, r))
+                    if (!a.is_numeral(val, r)) {
+                        IF_VERBOSE(1, verbose_stream() << "mbp failed on " << mk_pp(v, m) << " := " << val << "\n");
                         throw default_exception("evaluation did not produce a numeral");
+                    }
                     TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";);
                     tids.insert(v, mbo.add_var(r, a.is_int(v)));
                 }
@@ -623,6 +628,7 @@ namespace mbp {
                     expr_ref val = eval(v);
                     if (!a.is_numeral(val, r)) {
                         TRACE("qe", tout << eval.get_model() << "\n";);
+                        IF_VERBOSE(1, verbose_stream() << "mbp failed on " << mk_pp(v, m) << " := " << val << "\n");
                         throw default_exception("mbp evaluation was only partial");
                     }
                     id = mbo.add_var(r, a.is_int(v));
diff --git a/src/qe/mbp/mbp_plugin.cpp b/src/qe/mbp/mbp_plugin.cpp
index 2717f65cb1d..2584a4ce1ca 100644
--- a/src/qe/mbp/mbp_plugin.cpp
+++ b/src/qe/mbp/mbp_plugin.cpp
@@ -246,8 +246,10 @@ namespace mbp {
     bool project_plugin::is_true(model_evaluator& eval, expr* e) {
         expr_ref val = eval(e);
         bool tt = m.is_true(val);
-        if (!tt && !m.is_false(val) && contains_uninterpreted(val))
+        if (!tt && !m.is_false(val) && contains_uninterpreted(val)) {
+            IF_VERBOSE(1, verbose_stream() << "mbp failed on " << mk_pp(e, m) << " := " << val << "\n");
             throw default_exception("could not evaluate Boolean in model");
+        }
         SASSERT(tt || m.is_false(val));
         return tt;
     }