From 825fbf1832d1e6edf4af2059503f2c7844c732c4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 13 Mar 2020 10:49:39 -0700
Subject: [PATCH] fix #3268

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/rewriter_def.h | 19 +++++++++++++------
 src/solver/tactic2solver.cpp    |  3 ++-
 src/tactic/goal.cpp             | 14 ++++++++++++++
 src/tactic/goal.h               |  1 +
 src/tactic/tactic.cpp           |  2 +-
 5 files changed, 31 insertions(+), 8 deletions(-)

diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 613c928b0..5cd3ec239 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -678,9 +678,14 @@ 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) {
-    if (m_cancel_check && m().canceled()) {
-        reset();
-        throw rewriter_exception(m().limit().get_cancel_msg());
+    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());
@@ -713,9 +718,11 @@ template<bool ProofGen>
 void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr) {
     SASSERT(!frame_stack().empty());
     while (!frame_stack().empty()) {
-        if (m_cancel_check && m().canceled()) {
-            reset();
-            throw rewriter_exception(m().limit().get_cancel_msg());
+        if (m().canceled()) {
+            if (m_cancel_check) {
+                reset();
+                throw rewriter_exception(m().limit().get_cancel_msg());
+            }
         }
         SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
         frame & fr = frame_stack().back();
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 006d21e41..740afbf5c 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -196,9 +196,10 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
         }
         TRACE("tactic", 
               if (m_mc) m_mc->display(tout << "mc:\n");
-              if (g->mc()) g->mc()->display(tout << "\ng\n:");
+              if (g->mc()) g->mc()->display(tout << "\ng:\n");
               if (md) tout << "\nmodel:\n" << *md.get() << "\n";
               );
+        //m_mc = concat(m_mc.get(), g->mc());
         m_mc = concat(g->mc(), m_mc.get());
 
     }
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index a363313bc..b9f0ee138 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -393,6 +393,20 @@ void goal::display_with_dependencies(std::ostream & out) const {
     out << "\n  :precision " << prec() << " :depth " << depth() << ")" << std::endl;
 }
 
+
+void goal::display_with_proofs(std::ostream& out) const {
+    out << "(goal";
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        out << "\n  |-";
+        if (pr(i)) {
+            out << mk_ismt2_pp(pr(i), m(), 4);
+        }
+        out << "\n  " << mk_ismt2_pp(form(i), m(), 2);
+    }
+    out << "\n  :precision " << prec() << " :depth " << depth() << ")" << std::endl;
+}
+
 void goal::display(ast_printer_context & ctx) const {
     display(ctx, ctx.regular_stream());
 }
diff --git a/src/tactic/goal.h b/src/tactic/goal.h
index c964c55b4..ac376857e 100644
--- a/src/tactic/goal.h
+++ b/src/tactic/goal.h
@@ -141,6 +141,7 @@ public:
     void display_with_dependencies(ast_printer & prn, std::ostream & out) const;
     void display_with_dependencies(ast_printer_context & ctx) const;
     void display_with_dependencies(std::ostream & out) const;
+    void display_with_proofs(std::ostream& out) const;
 
     bool sat_preserved() const;
     bool unsat_preserved() const;
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 6833f991d..898a7a232 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -34,7 +34,7 @@ struct tactic_report::imp {
         m_goal(g),
         m_start_memory(static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024)) {
         m_watch.start();
-        TRACE("tactic", g.display(tout << id << "\n"););
+        TRACE("tactic", g.display_with_proofs(tout << id << "\n"););
     }
         
     ~imp() {