diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp
index d24ae4f49..c40927179 100644
--- a/src/tactic/bv/elim_small_bv_tactic.cpp
+++ b/src/tactic/bv/elim_small_bv_tactic.cpp
@@ -307,9 +307,8 @@ public:
 
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        imp * d = alloc(imp, m, m_params);
-        std::swap(d, m_imp);
-        dealloc(d);
+        m_imp->~imp();
+        m_imp = new (m_imp) imp(m, m_params);
     }
 
 };
diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp
index 91f1d9020..79526a101 100644
--- a/src/tactic/core/elim_term_ite_tactic.cpp
+++ b/src/tactic/core/elim_term_ite_tactic.cpp
@@ -171,9 +171,8 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        imp * d = alloc(imp, m, m_params);
-        std::swap(d, m_imp);        
-        dealloc(d);
+        m_imp->~imp();
+        m_imp = new (m_imp) imp(m, m_params);
     }
 
 };
diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index a4b9825cc..476c21232 100644
--- a/src/tactic/core/reduce_args_tactic.cpp
+++ b/src/tactic/core/reduce_args_tactic.cpp
@@ -502,9 +502,8 @@ void reduce_args_tactic::operator()(goal_ref const & g,
 }
 
 void reduce_args_tactic::cleanup() {
-    ast_manager & m   = m_imp->m();    
-    imp * d = alloc(imp, m);
-    std::swap(d, m_imp);    
-    dealloc(d);
+    ast_manager & m   = m_imp->m();
+    m_imp->~imp();
+    m_imp = new (m_imp) imp(m);
 }