diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 017ee5024..4f4ce1db2 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -155,7 +155,8 @@ namespace smt {
                 unsigned best_param_state_idx = replay_proof_prefixes(candidate_param_states);
 
                 if (best_param_state_idx != 0) {
-                    best_param_state = candidate_param_states[best_param_state_idx];
+                    m_param_state = candidate_param_states[best_param_state_idx];
+                    b.set_param_state(m_param_state);
                     IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found better param state at index " << best_param_state_idx << "\n");
                 } else {
                     IF_VERBOSE(1, verbose_stream() << " PARAM TUNER retained current param state\n");
@@ -192,6 +193,13 @@ namespace smt {
 
         check_cube_start:
             LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n");
+            
+            // apply current best param state from batch manager
+            smt_params params = b.get_best_param_state();
+            params_ref p;
+            params.updt_params(p);
+            ctx->updt_params(p);
+
             lbool r = check_cube(cube);
 
             if (!m.inc()) {
@@ -424,6 +432,11 @@ namespace smt {
         }
     }
 
+    smt_params parallel::batch_manager::get_best_param_state() {
+        std::scoped_lock lock(mux);
+        return m_param_state;
+    }
+
     void parallel::worker::collect_shared_clauses() {
         expr_ref_vector new_clauses = b.return_shared_clauses(m_g2l, m_shared_clause_limit, id);
         // iterate over new clauses and assert them in the local context
diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h
index 41dab51f1..f0a438a47 100644
--- a/src/smt/smt_parallel.h
+++ b/src/smt/smt_parallel.h
@@ -80,6 +80,7 @@ namespace smt {
             std::mutex mux;
             state m_state = state::is_running;
             stats m_stats;
+            smt_params m_param_state;
             using node = search_tree::node<cube_config>;
             search_tree::tree<cube_config> m_search_tree;
             
@@ -104,8 +105,10 @@ namespace smt {
             void set_sat(ast_translation& l2g, model& m);
             void set_exception(std::string const& msg);
             void set_exception(unsigned error_code);
+            void set_param_state(smt_params const& p) { m_param_state = p; }
             void collect_statistics(::statistics& st) const;
-
+            
+            smt_params get_best_param_state();
             bool get_cube(ast_translation& g2l, unsigned id, expr_ref_vector& cube, node*& n);
             void backtrack(ast_translation& l2g, expr_ref_vector const& core, node* n);
             void split(ast_translation& l2g, unsigned id, node* n, expr* atom);