diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index 28300e569..7fa3328fb 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -233,10 +233,16 @@ public:
             }
 
             lbool r;
-            if (assumptions.empty())
-                r = m_ctx->setup_and_check();
-            else
-                r = m_ctx->check(assumptions.size(), assumptions.c_ptr());
+            try {
+                if (assumptions.empty())
+                    r = m_ctx->setup_and_check();
+                else
+                    r = m_ctx->check(assumptions.size(), assumptions.c_ptr());
+            }
+            catch(...) {
+                m_ctx->collect_statistics(m_stats);
+                throw;
+            }
             m_ctx->collect_statistics(m_stats);
             switch (r) {
             case l_true: {
@@ -284,6 +290,9 @@ public:
                 return;
             }
             case l_undef:
+                if (m_ctx->canceled()) {
+                    throw tactic_exception(Z3_CANCELED_MSG);
+                }
                 if (m_fail_if_inconclusive)
                     throw tactic_exception("smt tactic failed to show goal to be sat/unsat");
                 result.push_back(in.get());