diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index 3a6e8e56f..8c6227d7d 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -585,7 +585,7 @@ extern "C" {
         to_fixedpoint_ref(d)->collect_param_descrs(descrs);
         to_params(p)->m_params.validate(descrs);
         to_fixedpoint_ref(d)->updt_params(to_param_ref(p));
-        to_fixedpoint(d)->m_params = to_param_ref(p);
+        to_fixedpoint(d)->m_params.append(to_param_ref(p));
         Z3_CATCH;
     }
 
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 0c2461dd6..097dff6db 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -859,8 +859,8 @@ ast_manager & th_rewriter::m() const {
 }
 
 void th_rewriter::updt_params(params_ref const & p) {
-    m_params = p;
-    m_imp->cfg().updt_params(p);
+    m_params.append(p);
+    m_imp->cfg().updt_params(m_params);
 }
 
 void th_rewriter::get_param_descrs(param_descrs & r) {
diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp
index 5b648741c..5a628ce58 100644
--- a/src/cmd_context/extra_cmds/dbg_cmds.cpp
+++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp
@@ -199,12 +199,12 @@ void tst_params(cmd_context & ctx) {
     params_ref p1;
     params_ref p2;
     p1.set_uint("val", 100);
-    p2 = p1;
+    p2.append(p1);
     SASSERT(p2.get_uint("val", 0) == 100);
     p2.set_uint("val", 200);
     SASSERT(p2.get_uint("val", 0) == 200);
     SASSERT(p1.get_uint("val", 0) == 100);
-    p2 = p1;
+    p2.append(p1);
     SASSERT(p2.get_uint("val", 0) == 100);
     SASSERT(p1.get_uint("val", 0) == 100);
     ctx.regular_stream() << "worked" << std::endl;
diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp
index 1bc0cb630..6124e726e 100644
--- a/src/math/subpaving/tactic/subpaving_tactic.cpp
+++ b/src/math/subpaving/tactic/subpaving_tactic.cpp
@@ -227,8 +227,8 @@ public:
     }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index b66ddf275..6ffd0f745 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -395,8 +395,8 @@ public:
     char const* name() const override { return "horn"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
 
diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp
index ddf85ce19..3baf9da87 100644
--- a/src/nlsat/tactic/nlsat_tactic.cpp
+++ b/src/nlsat/tactic/nlsat_tactic.cpp
@@ -55,8 +55,8 @@ class nlsat_tactic : public tactic {
         }
         
         void updt_params(params_ref const & p) {
-            m_params = p;
-            m_solver.updt_params(p);
+            m_params.append(p);
+            m_solver.updt_params(m_params);
         }
         
         bool contains_unsupported(expr_ref_vector & b2a, expr_ref_vector & x2t) {
@@ -226,7 +226,7 @@ public:
     char const* name() const override { return "nlsat"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
+        m_params.append(p);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/params/context_params.cpp b/src/params/context_params.cpp
index 4bc37b86b..294c5cbbe 100644
--- a/src/params/context_params.cpp
+++ b/src/params/context_params.cpp
@@ -190,7 +190,8 @@ void context_params::get_solver_params(params_ref & p, bool & proofs_enabled, bo
     proofs_enabled     &= p.get_bool("proof", m_proof);
     models_enabled     &= p.get_bool("model", m_model);
     unsat_core_enabled = m_unsat_core || p.get_bool("unsat_core", false);
-    p = merge_default_params(p);
+    if (!m_auto_config && !p.contains("auto_config"))
+        p.set_bool("auto_config", false);
 }
 
 
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index f6dd9c712..68ab215a2 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -2466,7 +2466,7 @@ public:
     }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
+        m_params.append(p);
         // m_imp->updt_params(p);
     }
 
diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp
index da1ce5efd..76f4f5715 100644
--- a/src/qe/qe_tactic.cpp
+++ b/src/qe/qe_tactic.cpp
@@ -103,8 +103,8 @@ public:
     char const* name() const override { return "qe"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
    
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index 38c25eae3..892a88f89 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -201,8 +201,8 @@ public:
     char const* name() const override { return "sat"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        if (m_imp) m_imp->updt_params(p);
+        m_params.append(p);
+        if (m_imp) m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index f9ab54327..03f55585a 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -124,7 +124,7 @@ namespace {
         smt_params m_smt_params_save;
 
         void push_params() override {
-            m_params_save = params_ref();
+            m_params_save.reset();           
             m_params_save.copy(solver::get_params());
             m_smt_params_save = m_smt_params;
         }
diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
index c99e50393..943facb98 100644
--- a/src/smt/tactic/smt_tactic_core.cpp
+++ b/src/smt/tactic/smt_tactic_core.cpp
@@ -127,7 +127,8 @@ public:
 
         scoped_init_ctx(smt_tactic & o, ast_manager & m):m_owner(o) {
             m_params = o.fparams();
-            m_params_ref = o.params();
+            m_params_ref.reset();
+            m_params_ref.append(o.params());
             smt::kernel * new_ctx = alloc(smt::kernel, m, m_params, m_params_ref);
             TRACE("smt_tactic", tout << "logic: " << o.m_logic << "\n";);
             new_ctx->set_logic(o.m_logic);
diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp
index 97ce4a1c1..e0197d15d 100644
--- a/src/smt/tactic/unit_subsumption_tactic.cpp
+++ b/src/smt/tactic/unit_subsumption_tactic.cpp
@@ -50,7 +50,7 @@ struct unit_subsumption_tactic : public tactic {
     }
 
     void updt_params(params_ref const& p) override {
-        m_params = p;
+        m_params.append(p);
         // m_context.updt_params(p); does not exist.
     }
     
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index b53e3daed..7dcca2ecc 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -226,7 +226,7 @@ void solver::collect_param_descrs(param_descrs & r) {
 }
 
 void solver::reset_params(params_ref const & p) {
-    m_params = p;
+    m_params.append(p);
     solver_params sp(m_params);
     m_cancel_backup_file = sp.cancel_backup_file();
 }
diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp
index 4493568bf..33ffbf282 100644
--- a/src/tactic/arith/add_bounds_tactic.cpp
+++ b/src/tactic/arith/add_bounds_tactic.cpp
@@ -149,8 +149,8 @@ public:
     char const* name() const override { return "add_bounds"; }
     
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp
index fce096f23..3cc7436d1 100644
--- a/src/tactic/arith/card2bv_tactic.cpp
+++ b/src/tactic/arith/card2bv_tactic.cpp
@@ -45,7 +45,7 @@ public:
     char const* name() const override { return "card2bv"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
+        m_params.append(p);
     }
 
     void collect_param_descrs(param_descrs & r) override {  
diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp
index 92ce7cd29..4269aff85 100644
--- a/src/tactic/arith/diff_neq_tactic.cpp
+++ b/src/tactic/arith/diff_neq_tactic.cpp
@@ -360,8 +360,8 @@ public:
     char const* name() const override { return "diff_neq"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp
index 07b59a3f9..6b9b226b3 100644
--- a/src/tactic/arith/factor_tactic.cpp
+++ b/src/tactic/arith/factor_tactic.cpp
@@ -297,8 +297,8 @@ public:
     char const* name() const override { return "factor"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->m_rw.cfg().updt_params(p);
+        m_params.append(p);
+        m_imp->m_rw.cfg().updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp
index f2039c378..87061b189 100644
--- a/src/tactic/arith/fix_dl_var_tactic.cpp
+++ b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -303,8 +303,8 @@ public:
     char const* name() const override { return "fix_dl_var"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index ef8109de0..569dbff21 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -1645,8 +1645,8 @@ public:
     char const* name() const override { return "fm"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index 77786e267..5f6edf6ea 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -135,8 +135,8 @@ public:
     char const* name() const override { return "lia2card"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_compile_equality = p.get_bool("compile_equality", true);
+        m_params.append(p);
+        m_compile_equality = m_params.get_bool("compile_equality", true);
     }
 
     expr_ref mk_bounded(expr_ref_vector& axioms, app* x, unsigned lo, unsigned hi) {
diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp
index d67f49a37..46404ffb0 100644
--- a/src/tactic/arith/lia2pb_tactic.cpp
+++ b/src/tactic/arith/lia2pb_tactic.cpp
@@ -308,8 +308,8 @@ public:
     char const* name() const override { return "lia2pb"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp
index b63c85f1b..2d405895f 100644
--- a/src/tactic/arith/pb2bv_tactic.cpp
+++ b/src/tactic/arith/pb2bv_tactic.cpp
@@ -1010,8 +1010,8 @@ public:
     char const* name() const override { return "pb2bv"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp
index d55ea4ecf..0f62b45f4 100644
--- a/src/tactic/arith/propagate_ineqs_tactic.cpp
+++ b/src/tactic/arith/propagate_ineqs_tactic.cpp
@@ -543,8 +543,8 @@ propagate_ineqs_tactic::~propagate_ineqs_tactic() {
 }
 
 void propagate_ineqs_tactic::updt_params(params_ref const & p) {
-    m_params = p;
-    m_imp->updt_params(p);
+    m_params.append(p);
+    m_imp->updt_params(m_params);
 }
 
 void propagate_ineqs_tactic::operator()(goal_ref const & g, 
diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index db43a3ee6..9c07bcadc 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -906,7 +906,7 @@ public:
     char const* name() const override { return "purify_arith"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
+        m_params.append(p);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp
index a7cef82e3..251d78e72 100644
--- a/src/tactic/arith/recover_01_tactic.cpp
+++ b/src/tactic/arith/recover_01_tactic.cpp
@@ -401,8 +401,8 @@ public:
     char const* name() const override { return "recover_01"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp
index 744f207f3..978a0a9a6 100644
--- a/src/tactic/bv/bit_blaster_tactic.cpp
+++ b/src/tactic/bv/bit_blaster_tactic.cpp
@@ -122,8 +122,8 @@ public:
     char const* name() const override { return "bit_blaster"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp
index 3af58bf66..0fc38f2db 100644
--- a/src/tactic/bv/bv1_blaster_tactic.cpp
+++ b/src/tactic/bv/bv1_blaster_tactic.cpp
@@ -434,8 +434,8 @@ public:
     char const* name() const override { return "bv1_blaster"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->m_rw.cfg().updt_params(p);
+        m_params.append(p);
+        m_imp->m_rw.cfg().updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp
index e0b6e4d81..7ea7c0a69 100644
--- a/src/tactic/bv/bv_bound_chk_tactic.cpp
+++ b/src/tactic/bv/bv_bound_chk_tactic.cpp
@@ -206,8 +206,8 @@ tactic * bv_bound_chk_tactic::translate(ast_manager & m) {
 
 
 void bv_bound_chk_tactic::updt_params(params_ref const & p) {
-    m_params = p;
-    m_imp->updt_params(p);
+    m_params.append(p);
+    m_imp->updt_params(m_params);
 }
 
 void bv_bound_chk_tactic::cleanup() {
diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp
index d0bd6538b..da86ed663 100644
--- a/src/tactic/bv/bvarray2uf_tactic.cpp
+++ b/src/tactic/bv/bvarray2uf_tactic.cpp
@@ -116,8 +116,8 @@ public:
     char const* name() const override { return "bvarray2uf"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp
index 7c72abde9..eef85ebba 100644
--- a/src/tactic/bv/elim_small_bv_tactic.cpp
+++ b/src/tactic/bv/elim_small_bv_tactic.cpp
@@ -207,7 +207,7 @@ class elim_small_bv_tactic : public tactic {
         }
 
         void updt_params(params_ref const & p) {
-            m_params = p;
+            m_params.append(p);
             m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
             m_max_steps = p.get_uint("max_steps", UINT_MAX);
             m_max_bits = p.get_uint("max_bits", 4);
@@ -241,8 +241,8 @@ public:
     }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_rw.cfg().updt_params(p);
+        m_params.append(p);
+        m_rw.cfg().updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp
index 0efe4f58c..2bc99806e 100644
--- a/src/tactic/bv/max_bv_sharing_tactic.cpp
+++ b/src/tactic/bv/max_bv_sharing_tactic.cpp
@@ -280,8 +280,8 @@ public:
     char const* name() const override { return "max_bv_sharing"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->m_rw.cfg().updt_params(p);
+        m_params.append(p);
+        m_imp->m_rw.cfg().updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp
index fe1269732..38b4e172e 100644
--- a/src/tactic/core/blast_term_ite_tactic.cpp
+++ b/src/tactic/core/blast_term_ite_tactic.cpp
@@ -174,8 +174,8 @@ public:
     char const* name() const override { return "blast_term_ite"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->m_rw.m_cfg.updt_params(p);
+        m_params.append(p);
+        m_imp->m_rw.m_cfg.updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp
index d1b8f5b1b..234b7262c 100644
--- a/src/tactic/core/cofactor_term_ite_tactic.cpp
+++ b/src/tactic/core/cofactor_term_ite_tactic.cpp
@@ -52,7 +52,7 @@ public:
 
     ~cofactor_term_ite_tactic() override {}
     char const* name() const override { return "cofactor"; }
-    void updt_params(params_ref const & p) override { m_params = p; m_elim_ite.updt_params(p); }
+    void updt_params(params_ref const & p) override { m_params.append(p); m_elim_ite.updt_params(m_params); }
     void collect_param_descrs(param_descrs & r) override { m_elim_ite.collect_param_descrs(r); }
     
     void  operator()(goal_ref const & g, goal_ref_buffer& result) override {
diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp
index 3d8ebfb12..e507f49dd 100644
--- a/src/tactic/core/collect_statistics_tactic.cpp
+++ b/src/tactic/core/collect_statistics_tactic.cpp
@@ -60,7 +60,7 @@ public:
     }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
+        m_params.append(p);
     }
 
     void collect_param_descrs(param_descrs & r) override {}
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index c8aa1a4c4..47b2fa389 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -605,8 +605,8 @@ ctx_simplify_tactic::~ctx_simplify_tactic() {
 }
 
 void ctx_simplify_tactic::updt_params(params_ref const & p) {
-    m_params = p;
-    m_imp->updt_params(p);
+    m_params.append(p);
+    m_imp->updt_params(m_params);
 }
 
 void ctx_simplify_tactic::get_param_descrs(param_descrs & r) {
diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp
index 42adf04a9..2a0593ade 100644
--- a/src/tactic/core/elim_term_ite_tactic.cpp
+++ b/src/tactic/core/elim_term_ite_tactic.cpp
@@ -143,8 +143,8 @@ public:
     }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->m_rw.cfg().updt_params(p);
+        m_params.append(p);
+        m_imp->m_rw.cfg().updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index a9f5ffcf8..26a69fd4a 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -862,9 +862,9 @@ public:
     }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
-        m_max_steps  = p.get_uint("max_steps", UINT_MAX);
+        m_params.append(p);
+        m_max_memory = megabytes_to_bytes(m_params.get_uint("max_memory", UINT_MAX));
+        m_max_steps  = m_params.get_uint("max_steps", UINT_MAX);
     }
     
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp
index 485eda4dd..dfcb152a2 100644
--- a/src/tactic/core/injectivity_tactic.cpp
+++ b/src/tactic/core/injectivity_tactic.cpp
@@ -258,8 +258,8 @@ public:
     char const* name() const override { return "injectivity"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_finder->updt_params(p);
+        m_params.append(p);
+        m_finder->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp
index 164cf9311..fccfdf53e 100644
--- a/src/tactic/core/nnf_tactic.cpp
+++ b/src/tactic/core/nnf_tactic.cpp
@@ -51,7 +51,7 @@ public:
 
     char const* name() const override { return "nnf"; }
 
-    void updt_params(params_ref const & p) override { m_params = p; }
+    void updt_params(params_ref const & p) override { m_params.append(p); }
 
     void collect_param_descrs(param_descrs & r) override { nnf::get_param_descrs(r); }
 
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index b735de4b7..b2ed7cab9 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -219,9 +219,9 @@ public:
     char const* name() const override { return "propagate_values"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
+        m_params.append(p);
         m_r.updt_params(p);
-        updt_params_core(p);
+        updt_params_core(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp
index ca76cafc7..8d9ff759f 100644
--- a/src/tactic/core/simplify_tactic.cpp
+++ b/src/tactic/core/simplify_tactic.cpp
@@ -80,8 +80,8 @@ simplify_tactic::~simplify_tactic() {
 }
 
 void simplify_tactic::updt_params(params_ref const & p) {
-    m_params = p;
-    m_imp->m_r.updt_params(p);
+    m_params.append(p);
+    m_imp->m_r.updt_params(m_params);
 }
 
 void simplify_tactic::get_param_descrs(param_descrs & r) {
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 9d844b7ed..a73fe88b6 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -1092,8 +1092,8 @@ public:
     char const* name() const override { return "solve_eqs"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {        
diff --git a/src/tactic/core/special_relations_tactic.h b/src/tactic/core/special_relations_tactic.h
index a1cafb7c0..dae38304a 100644
--- a/src/tactic/core/special_relations_tactic.h
+++ b/src/tactic/core/special_relations_tactic.h
@@ -49,7 +49,7 @@ public:
 
     ~special_relations_tactic() override {}
 
-    void updt_params(params_ref const & p) override { m_params = p; }
+    void updt_params(params_ref const & p) override { m_params.append(p); }
     
     void collect_param_descrs(param_descrs & r) override { }
     
diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp
index e26fded8f..c141aaa3b 100644
--- a/src/tactic/core/tseitin_cnf_tactic.cpp
+++ b/src/tactic/core/tseitin_cnf_tactic.cpp
@@ -894,8 +894,8 @@ public:
     char const* name() const override { return "tseitin_cnf"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp
index be98dea00..282439228 100644
--- a/src/tactic/fpa/fpa2bv_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_tactic.cpp
@@ -123,8 +123,8 @@ public:
     char const* name() const override { return "fp2bv"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp
index 6b275508b..c92968c8c 100644
--- a/src/tactic/portfolio/solver_subsumption_tactic.cpp
+++ b/src/tactic/portfolio/solver_subsumption_tactic.cpp
@@ -136,8 +136,8 @@ public:
     char const* name() const override { return "solver_subsumption"; }
 
     void updt_params(params_ref const& p) override { 
-        m_params = p; 
-        unsigned max_conflicts = p.get_uint("max_conflicts", 2);
+        m_params.append(p);
+        unsigned max_conflicts = m_params.get_uint("max_conflicts", 2);
         m_params.set_uint("sat.max_conflicts", max_conflicts);
         m_params.set_uint("smt.max_conflicts", max_conflicts);
     }
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index ece6940f3..e631c23e9 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -53,8 +53,8 @@ public:
     char const* name() const override { return "sls"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_engine->updt_params(p);
+        m_params.append(p);
+        m_engine->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp
index c5745d85c..2358abcd1 100644
--- a/src/tactic/ufbv/macro_finder_tactic.cpp
+++ b/src/tactic/ufbv/macro_finder_tactic.cpp
@@ -108,8 +108,8 @@ public:
     char const* name() const override { return "macro_finder"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp
index 0e0cb7cb2..b0eb113b8 100644
--- a/src/tactic/ufbv/quasi_macros_tactic.cpp
+++ b/src/tactic/ufbv/quasi_macros_tactic.cpp
@@ -103,8 +103,8 @@ public:
     char const* name() const override { return "quasi_macros"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        m_imp->updt_params(p);
+        m_params.append(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
index d5bfec8fe..e254523c0 100644
--- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
@@ -35,7 +35,7 @@ public:
     }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
+        m_params.append(p);
     }
 
     void collect_param_descrs(param_descrs & r) override {
diff --git a/src/util/params.cpp b/src/util/params.cpp
index 1819684e0..4911664f1 100644
--- a/src/util/params.cpp
+++ b/src/util/params.cpp
@@ -520,7 +520,7 @@ params_ref::~params_ref() {
 
 params_ref::params_ref(params_ref const & p):
     m_params(nullptr) {
-    operator=(p);
+    set(p);
 }
 
 void params_ref::display(std::ostream & out) const {
@@ -553,18 +553,18 @@ void params_ref::validate(param_descrs const & p) {
         m_params->validate(p);
 }
 
-params_ref & params_ref::operator=(params_ref const & p) {
+
+void params_ref::set(params_ref const & p) {
     if (p.m_params)
         p.m_params->inc_ref();
     if (m_params)
         m_params->dec_ref();
     m_params = p.m_params;
-    return *this;
 }
 
 void params_ref::copy(params_ref const & src) {
-    if (m_params == nullptr)
-        operator=(src);
+    if (m_params == nullptr || m_params->empty())
+        set(src);
     else {
         init();
         copy_core(src.m_params);
diff --git a/src/util/params.h b/src/util/params.h
index 989d112bd..da05dff90 100644
--- a/src/util/params.h
+++ b/src/util/params.h
@@ -35,6 +35,8 @@ class params_ref {
     params * m_params;
     void init();
     void copy_core(params const * p);
+    params_ref& operator=(params_ref const& p) = delete;
+    void set(params_ref const& p);
 public:
     params_ref():m_params(nullptr) {}
     params_ref(params_ref const & p);
@@ -42,8 +44,7 @@ public:
     
     static params_ref const & get_empty() { return g_empty_params_ref; }
     
-    params_ref & operator=(params_ref const & p);
-    
+        
     // copy params from src
     void copy(params_ref const & src);
     void append(params_ref const & src) { copy(src); }