diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index f95b77b2d..6b6728e07 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -118,6 +118,12 @@ namespace smt {
         if (!m_setup.already_configured()) {
             m_fparams.updt_params(p);
         }
+        else {
+            // selected parameters are safe to update after initialization
+            params_ref new_p;
+            new_p.set_uint("max_conflicts", p.get_uint("max_conflicts", UINT_MAX));
+            m_fparams.updt_params(new_p);
+        }
         for (auto th : m_theory_set)
             if (th)
                 th->updt_params();
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index f691dfa05..3687f1194 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -267,15 +267,6 @@ namespace {
             m_context.set_preprocess(f);
         }
 
-        void set_max_conflicts(unsigned max_conflicts) override {
-            auto& ctx = m_context.get_context();
-            ctx.get_fparams().m_max_conflicts = max_conflicts;
-        }
-
-        unsigned get_max_conflicts() const override {
-            return m_context.get_context().get_fparams().m_max_conflicts;
-        }
-
         void get_backbone_candidates(vector<solver::scored_literal>& candidates, unsigned max_num) override {
             ast_manager& m = get_manager();
             auto& ctx = m_context.get_context();
diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp
index dcd844b09..c6f7891bc 100644
--- a/src/solver/parallel_tactical2.cpp
+++ b/src/solver/parallel_tactical2.cpp
@@ -106,6 +106,12 @@ static bool is_cancellation_exception(char const* msg) {
     return msg && (strstr(msg, "canceled") != nullptr || strstr(msg, "cancelled") != nullptr);
 }
 
+static void set_max_conflicts(solver_ref& s, unsigned max_conflicts) {
+    params_ref p;
+    p.set_uint("max_conflicts", max_conflicts);
+    s->updt_params(p);
+}
+
 /* ------------------------------------------------------------------ */
 /* parallel_solver – the core portfolio engine                         */
 /* ------------------------------------------------------------------ */
@@ -950,7 +956,7 @@ class parallel_solver {
         }
 
         lbool check_cube(expr_ref_vector const& cube) {
-            s->set_max_conflicts(std::min(m_config.m_threads_max_conflicts, m_config.m_max_conflicts));
+            set_max_conflicts(s, std::min(m_config.m_threads_max_conflicts, m_config.m_max_conflicts));
 
             expr_ref_vector combined(m);
             combined.append(asms);
@@ -1341,16 +1347,16 @@ class parallel_solver {
                         else
                             ++m_stats.m_fallback_singleton_checks;
 
-                        unsigned old_max_conflicts = s->get_max_conflicts();
-                        s->set_max_conflicts(10);
+                        unsigned old_max_conflicts = s->get_params().get_uint("max_conflicts", UINT_MAX);
+                        set_max_conflicts(s, 10);
 
                         for (expr* lit : chunk_lits) {
                             if (is_retry && b.has_new_backbone_candidates(bb_candidate_epoch)) {
-                                s->set_max_conflicts(old_max_conflicts);
+                                set_max_conflicts(s, old_max_conflicts);
                                 return;
                             }
                             if (!m.inc() || canceled()) {
-                                s->set_max_conflicts(old_max_conflicts);
+                                set_max_conflicts(s, old_max_conflicts);
                                 return;
                             }
                             if (!bb_candidate_lits.contains(lit))
@@ -1378,7 +1384,7 @@ class parallel_solver {
                                         lbool terminal_result = probe_literal(mk_not(m, bb_ref), is_retry);
                                         LOG_BB_WORKER(1, " RESULT: " << terminal_result << " FOR CANDIDATE: " << mk_bounded_pp(bb_ref.get(), m, 3) << "\n");
                                         if (terminal_result != l_undef) {
-                                            s->set_max_conflicts(old_max_conflicts);
+                                            set_max_conflicts(s,old_max_conflicts);
                                             return;
                                         }
                                     }
@@ -1387,7 +1393,7 @@ class parallel_solver {
                             bb_candidate_lits.erase(lit);
                         }
 
-                        s->set_max_conflicts(old_max_conflicts);
+                        set_max_conflicts(s, old_max_conflicts);
                     };
 
                 ++m_stats.m_batches_total;
@@ -1459,7 +1465,7 @@ class parallel_solver {
                         for (expr* a : bb_asms)
                             asms.push_back(a);
 
-                        s->set_max_conflicts(m_bb_conflicts_per_chunk);
+                        set_max_conflicts(s,m_bb_conflicts_per_chunk);
                         lbool r = l_undef;
                         try {
                             r = s->check_sat(asms);
@@ -1584,7 +1590,7 @@ class parallel_solver {
             : id(id), b(p.m_batch_manager),
               asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) {
             s = src.translate(m, params);
-            s->set_max_conflicts(m_bb_conflicts_per_chunk);
+            set_max_conflicts(s, m_bb_conflicts_per_chunk);
             s->pop_to_base_level();
             for (expr* a : src_asms)
                 asms.push_back(m_g2l(a));
@@ -1680,7 +1686,7 @@ class parallel_solver {
 
                 lbool r = l_undef;
                 try {
-                    s->set_max_conflicts(m_core_minimize_conflict_budget);
+                    set_max_conflicts(s, m_core_minimize_conflict_budget);
                     r = s->check_sat(trial);
                 }
                 catch (z3_error&) {
diff --git a/src/solver/solver.h b/src/solver/solver.h
index 73a83a6dd..45a3a28a9 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -321,15 +321,6 @@ public:
     virtual void setup_for_parallel() {}
 
     virtual void set_preprocess(bool) {}
-
-    virtual void set_max_conflicts(unsigned max_conflicts) {
-        params_ref p;
-        p.set_uint("max_conflicts", max_conflicts);
-        updt_params(p);
-    }
-
-    virtual unsigned get_max_conflicts() const { return UINT_MAX; }
-
     
     virtual void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) = 0;