diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index 1caeede92..ee09a9fa3 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -231,6 +231,9 @@ public:
                     mc = concat(fmc.get(), mc.get());
                     in->add(mc.get());
                 }
+                if (m_ctx->canceled() && !pr) {
+                    throw tactic_exception(Z3_CANCELED_MSG);
+                }
                 return;
             }
             case l_false: {