diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
index 2af794e13..a9fd2fc72 100644
--- a/src/smt/tactic/smt_tactic_core.cpp
+++ b/src/smt/tactic/smt_tactic_core.cpp
@@ -106,12 +106,6 @@ public:
     }
 
     void cleanup() override {
-        m_user_ctx = nullptr;
-        m_vars.reset();
-        m_fixed_eh = nullptr;
-        m_final_eh = nullptr;
-        m_eq_eh = nullptr;
-        m_diseq_eh = nullptr;
     }
 
     void reset_statistics() override {
@@ -417,7 +411,11 @@ public:
         user_propagator::push_eh_t& push_eh,
         user_propagator::pop_eh_t& pop_eh,
         user_propagator::fresh_eh_t& fresh_eh) override {
-        SASSERT(!m_user_ctx);
+        m_vars.reset();
+        m_fixed_eh = nullptr;
+        m_final_eh = nullptr;
+        m_eq_eh = nullptr;
+        m_diseq_eh = nullptr;
         m_user_ctx = ctx;
         m_push_eh = push_eh;
         m_pop_eh = pop_eh;