fix #3867

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

3 files changed, 10 insertions, 1 deletions

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 9bf959c..328afad 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -744,3 +744,7 @@ void model_evaluator::set_solver(expr_solver* solver) {
 bool model_evaluator::has_solver() {
     return m_imp->m_cfg.m_seq_rw.has_solver();
 }
+
+model_core const & model_evaluator::get_model() const {
+    return m_imp->cfg().m_model;
+}
diff --git a/src/model/model_evaluator.h b/src/model/model_evaluator.h
index 9f2320a..e57e1f3 100644
--- a/src/model/model_evaluator.h
+++ b/src/model/model_evaluator.h
@@ -37,6 +37,7 @@ public:
     ~model_evaluator();
 
     ast_manager & m () const;
+    model_core const& get_model() const;
     void set_model_completion(bool f);
     bool get_model_completion() const; 
     void set_expand_array_equalities(bool f);
diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp
index c30e77c..1fa65a1 100644
--- a/src/qe/qe_arith.cpp
+++ b/src/qe/qe_arith.cpp
@@ -564,7 +564,11 @@ namespace qe {
                 if (!tids.find(v, id)) {
                     rational r;
                     expr_ref val = eval(v);
-                    VERIFY(a.is_numeral(val, r));                    
+                    if (!a.is_numeral(val, r)) {
+                        TRACE("qe", tout << eval.get_model() << "\n";);
+
+                        throw default_exception("mbp evaluation was only partial");
+                    }
                     id = mbo.add_var(r, a.is_int(v));
                     tids.insert(v, id);
                 }