fix #3268

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/rewriter/rewriter_def.h

@@ -678,10 +678,15 @@ 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()) {
+    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;
@@ -713,10 +718,12 @@ 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()) {
+        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();
         expr * t   = fr.m_curr;

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());
 
     }

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());
 }

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;

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() {