diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
index a9fd2fc72..d6b2d4114 100644
--- a/src/smt/tactic/smt_tactic_core.cpp
+++ b/src/smt/tactic/smt_tactic_core.cpp
@@ -140,6 +140,7 @@ public:
         ~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);