From d06f4bd3378697d3da09993a5dfdd995b2ebc35c Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Thu, 24 May 2018 11:14:51 -0700
Subject: [PATCH] Fix reset of params_ref in solver

params_ref is not a ref, and params_ref::reset is not ref::reset.

params_ref::reset resets the params object being pointed to by
params_ref.

A proper way to reset a params_ref as a reference is to assign an
empty params_ref object to it.
---
 src/smt/smt_solver.cpp | 2 +-
 src/solver/solver.cpp  | 9 ++++-----
 2 files changed, 5 insertions(+), 6 deletions(-)

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);
 }