From 1a995da0aebfae0b5b4ddbfd5461da781a9fe2b8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 28 Mar 2020 12:54:06 -0700
Subject: [PATCH] fix #3538, turn on proof checking assertions in goal.cpp for
 earlier coverage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/pb2bv_rewriter.cpp  | 9 ++++++++-
 src/tactic/arith/card2bv_tactic.cpp  | 2 +-
 src/tactic/arith/lia2card_tactic.cpp | 6 +++---
 src/tactic/goal.cpp                  | 6 +++---
 4 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index c277ba704..1fcd4991f 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -936,6 +936,9 @@ struct pb2bv_rewriter::imp {
         bool flat_assoc(func_decl * f) const { return false; }
         br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
             result_pr = nullptr;
+            if (m_r.m.proofs_enabled()) {
+                return BR_FAILED;
+            }
             return m_r.mk_app_core(f, num, args, result);
         }
         card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {}
@@ -958,9 +961,13 @@ struct pb2bv_rewriter::imp {
         void set_min_arity(unsigned ma) { m_cfg.set_min_arity(ma); }
         void rewrite(bool full, expr* e, expr_ref& r, proof_ref& p) {
             expr_ref ee(e, m());
+            if (m().proofs_enabled()) {
+                r = e;
+                return;
+            }
+            proof_ref rp(m());
             if (m_cfg.m_r.mk_app(full, e, r)) {
                 ee = r;
-                // mp proof?
             }
             (*this)(ee, r, p);
         }
diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp
index 345fffc23..385476e75 100644
--- a/src/tactic/arith/card2bv_tactic.cpp
+++ b/src/tactic/arith/card2bv_tactic.cpp
@@ -65,8 +65,8 @@ public:
         }
                 
         expr_ref new_f1(m), new_f2(m);
-        proof_ref new_pr1(m), new_pr2(m);
         for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) {
+            proof_ref new_pr1(m), new_pr2(m);
             rw1(g->form(idx), new_f1, new_pr1);
             TRACE("card2bv", tout << "Rewriting " << new_f1 << "\n" << new_pr1 << std::endl;);
             rw2(false, new_f1, new_f2, new_pr2);
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index 372913ffb..0c5661cf0 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -204,11 +204,11 @@ public:
             if (g->form(i) != tmp && m.proofs_enabled()) {
                 pr1 = m.mk_rewrite(g->form(i), tmp);
             }
-            m_rw(tmp, new_curr, new_pr);
-            if (m.proofs_enabled() && tmp != new_curr) {
+            m_rw(tmp, new_curr, pr2);
+            if (m.proofs_enabled() && tmp != new_curr && !pr2) {
                 pr2 = m.mk_rewrite(tmp, new_curr);
             }
-            if (m.proofs_enabled()) {
+            if (m.proofs_enabled() && g->pr(i)) {
                 new_pr = m.mk_transitivity(pr1, pr2);
                 new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
             }
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index 28e7f2f4e..57ae78d75 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -133,7 +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(!pr || m().get_fact(pr) == f);
         SASSERT(!m_inconsistent);
         m().push_back(m_forms, f);
         m().push_back(m_proofs, pr);
@@ -253,7 +253,7 @@ void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) {
         return;
     }
     if (pr) {
-        // SASSERT(f == m().get_fact(pr));
+        SASSERT(f == m().get_fact(pr));
         slow_process(f, pr, d);
     }
     else {
@@ -284,7 +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));
+        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);