diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index d78b82cc6..a4e97380b 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -236,8 +236,8 @@ namespace smt {
         params_ref ps          = m_imp->params();
         #pragma omp critical (smt_kernel)
         {
-            dealloc(m_imp);
-            m_imp = alloc(imp, _m, fps, ps);
+            m_imp->~imp();
+            m_imp = new (m_imp) imp(_m, fps, ps);
         }
     }
 
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index b76fb6c74..f824cb3f1 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -361,8 +361,8 @@ namespace smt {
             context & ctx        = m_imp->m_context;
             smt_params & p = m_imp->m_params;
             quantifier_manager_plugin * plugin = m_imp->m_plugin->mk_fresh();
-            dealloc(m_imp);
-            m_imp = alloc(imp, *this, ctx, p, plugin);
+            m_imp->~imp();
+            m_imp = new (m_imp) imp(*this, ctx, p, plugin);
             plugin->set_manager(*this);
         }
     }