From 56358a6b94c9648bea6007ceb05f7f7cdf5b1c44 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 8 Apr 2020 18:06:37 -0700
Subject: [PATCH] fix #3867

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/model/model_evaluator.cpp | 4 ++++
 src/model/model_evaluator.h   | 1 +
 src/qe/qe_arith.cpp           | 6 +++++-
 3 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 9bf959cf2..328afad73 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 9f2320a66..e57e1f368 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 c30e77cc9..1fa65a1b4 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);
                 }