From 6a54c0bc044bbd2f712d931daf95cc6c3732ffc2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 21 Jun 2020 17:43:05 -0700
Subject: [PATCH] fix issues reported in #4525

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

diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp
index 4d46929a9..e0b7eaac4 100644
--- a/src/qe/qe_arith.cpp
+++ b/src/qe/qe_arith.cpp
@@ -209,7 +209,9 @@ namespace qe {
             else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) {
                 rational r;
                 val = eval(t);
-                VERIFY(a.is_numeral(val, r));
+                if (!a.is_numeral(val, r)) {
+                    throw default_exception("mbp evaluation didn't produce an integer");
+                }
                 c += mul*r;
                 // t1 mod mul1 == r               
                 rational c0(-r), mul0(1);
@@ -347,8 +349,8 @@ namespace qe {
                     expr_ref val = eval(v);
                     if (!m.inc())
                         return vector<def>();
-
-                    VERIFY(a.is_numeral(val, r));
+                    if (!a.is_numeral(val, r))
+                        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)));
                 }
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index b82bcfa8b..1d158ca94 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -2238,11 +2238,16 @@ class qe_lite::impl {
             if (is_forall(q)) {
                 result = push_not(result);
             }
-            result = m.update_quantifier(
+            expr_ref tmp(m);
+            tmp = m.update_quantifier(
                 q,
                 q->get_num_patterns(), new_patterns,
                 q->get_num_no_patterns(), new_no_patterns, result);
-            m_imp.m_rewriter(result, result, result_pr);
+            m_imp.m_rewriter(tmp, result, result_pr);
+            if (m.proofs_enabled()) {
+                result_pr = m.mk_transitivity(m.mk_rewrite(q, tmp), result_pr);
+            }
+
             return true;
         }
     };