diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 01b78b80e..8e5c2aaa2 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -122,7 +122,7 @@ namespace smt {
         smt_params m_smt_params_save;
 
         void push_params() override {
-            m_params_save.reset();
+            m_params_save = params_ref();
             m_params_save.copy(solver::get_params());
             m_smt_params_save = m_smt_params;
         }
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index cc1d472ca..84b5eb588 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -206,14 +206,13 @@ void solver::collect_param_descrs(param_descrs & r) {
     r.insert("solver.enforce_model_conversion", CPK_BOOL, "(default: false) enforce model conversion when asserting formulas");
 }
 
-void solver::reset_params(params_ref const & p) { 
-    m_params.reset();
-    m_params.copy(p); 
+void solver::reset_params(params_ref const & p) {
+    m_params = p;
     m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", false);
 }
 
-void solver::updt_params(params_ref const & p) { 
-    m_params.copy(p); 
+void solver::updt_params(params_ref const & p) {
+    m_params.copy(p);
     m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", false);
 }