diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
index a9fd2fc729e..d6b2d411461 100644
--- a/src/smt/tactic/smt_tactic_core.cpp
+++ b/src/smt/tactic/smt_tactic_core.cpp
@@ -140,6 +140,7 @@ class smt_tactic : public tactic {
         ~scoped_init_ctx() {
             smt::kernel * d = m_owner.m_ctx;
             m_owner.m_ctx = nullptr;
+            m_owner.m_user_ctx = nullptr;
 
             if (d)
                 dealloc(d);