diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index f76eca9a6..90fd64fd9 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1800,7 +1800,7 @@ static void track_id(ast* n, unsigned id) {
     if (n->get_id() != id) return;
     ++s_count;
     std::cout << s_count << "\n";
-//    SASSERT(s_count != 7);
+    //SASSERT(s_count != 23);
 }
 #endif
 
diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp
index e26419829..51098bafb 100644
--- a/src/smt/smt_context_inv.cpp
+++ b/src/smt/smt_context_inv.cpp
@@ -264,7 +264,7 @@ namespace smt {
     bool context::check_th_diseq_propagation() const {
         TRACE("check_th_diseq_propagation", tout << "m_propagated_th_diseqs.size() " << m_propagated_th_diseqs.size() << "\n";);
         int num = get_num_bool_vars();
-        if (inconsistent()) {
+        if (inconsistent() || get_manager().canceled()) { 
             return true;
         }
         for (bool_var v = 0; v < num; v++) {
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 81a1364f9..eb4092cd4 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -585,7 +585,8 @@ struct ctx_simplify_tactic::imp {
             for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
                 expr * t = g.form(i);
                 process(t, r);
-                proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(t, r));
+                proof_ref new_pr(m.mk_rewrite(t, r), m);
+                new_pr = m.mk_modus_ponens(g.pr(i), new_pr);
                 g.update(i, r, new_pr, g.dep(i));
             }
         }