diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 55e750980..b0abc0de0 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2773,6 +2773,7 @@ namespace smt {
     }
 
     void context::assert_expr_core(expr * e, proof * pr) {
+        if (m_cancel_flag) return;
         SASSERT(is_well_sorted(m_manager, e));
         TRACE("begin_assert_expr", tout << mk_pp(e, m_manager) << "\n";);
         TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m_manager) << "\n";);
@@ -2802,6 +2803,7 @@ namespace smt {
     }
 
     void context::internalize_assertions() {
+        if (m_cancel_flag) return;
         TRACE("internalize_assertions", tout << "internalize_assertions()...\n";);
         timeit tt(get_verbosity_level() >= 100, "smt.preprocessing");
         reduce_assertions();
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index c441a7d45..725d38ed5 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -229,6 +229,9 @@ public:
                     m_ctx->assert_expr(in->form(i));
                 }
             }
+            if (m_ctx->canceled()) {
+                throw tactic_exception("smt_tactic canceled");
+            }
             
             lbool r;
             if (assumptions.empty())