From ea396a008af7aa37ee6213d8e8d5d858e5659d67 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 25 Mar 2020 02:30:51 -0700
Subject: [PATCH] fix #3504

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/rewriter_def.h   |  4 ++--
 src/tactic/arith/eq2bv_tactic.cpp | 12 +++++++++---
 src/tactic/goal.cpp               |  5 ++++-
 3 files changed, 15 insertions(+), 6 deletions(-)

diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index fdfb6023f..f228a216b 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -683,20 +683,20 @@ void rewriter_tpl<Config>::update_binding_at(unsigned i, expr* binding) {
 template<typename Config>
 template<bool ProofGen>
 void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & result_pr) {
+    result_pr = nullptr;
     if (m().canceled()) {
         if (m_cancel_check) {
             reset();
             throw rewriter_exception(m().limit().get_cancel_msg());
         }
         result = t;
-        result_pr = nullptr;
         return;
     }
     SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
     SASSERT(not_rewriting());
     m_root      = t;
     m_num_qvars = 0;
-    m_num_steps = 0;
+    m_num_steps = 0;    
     if (visit<ProofGen>(t, RW_UNBOUNDED_DEPTH)) {
         result = result_stack().back();
         result_stack().pop_back();
diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index 75ce78860..bfb907e9f 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -200,13 +200,19 @@ public:
             func_decl_ref var(m);
             unsigned val;
             if (is_bound(g->form(i), var, val) && !m_has_eq.is_marked(var)) {
-                g->update(i, m.mk_true(), nullptr, nullptr);
+                if (m.proofs_enabled()) {
+                    new_pr = m.mk_rewrite(g->form(i), m.mk_true());
+                    new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
+                }
+                g->update(i, m.mk_true(), new_pr, nullptr);
                 mc1->insert(var, val);
                 continue;
             }
             m_rw(g->form(i), new_curr, new_pr);
-            if (m.proofs_enabled() && !new_pr) {
-                new_pr = m.mk_rewrite(g->form(i), new_curr);
+            if (g->form(i) == new_curr)
+                continue;
+            if (m.proofs_enabled()) {
+                if (!new_pr) new_pr = m.mk_rewrite(g->form(i), new_curr);
                 new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
             }
             g->update(i, new_curr, new_pr, g->dep(i));
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index a55b1cafc..28e7f2f4e 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -133,6 +133,7 @@ void goal::push_back(expr * f, proof * pr, expr_dependency * d) {
             m().push_back(m_dependencies, saved_d);
     }
     else {
+        // SASSERT(!pr || m().get_fact(pr) == f);
         SASSERT(!m_inconsistent);
         m().push_back(m_forms, f);
         m().push_back(m_proofs, pr);
@@ -252,6 +253,7 @@ void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) {
         return;
     }
     if (pr) {
+        // SASSERT(f == m().get_fact(pr));
         slow_process(f, pr, d);
     }
     else {
@@ -282,6 +284,7 @@ void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
     if (m_inconsistent)
         return;
     if (pr) {
+        // SASSERT(f == m().get_fact(pr));
         expr_ref out_f(m());
         proof_ref out_pr(m());
         slow_process(true, f, pr, d, out_f, out_pr);
@@ -591,7 +594,7 @@ bool goal::is_well_formed() const {
         if (!::is_well_sorted(m(), t))
             return false;
 #if 0
-        if (m().get_fact(pr(i)) != form(i)) {
+        if (pr(i) && m().get_fact(pr(i)) != form(i)) {
             TRACE("tactic", tout << mk_ismt2_pp(pr(i), m()) << "\n" << mk_ismt2_pp(form(i), m()) << "\n";);
             SASSERT(m().get_fact(pr(i)) == form(i));
             return false;