diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 95d3b34b7..917884193 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -64,8 +64,47 @@ namespace smt {
 
 namespace smt {
 
-    void parallel::param_generator::run() {
-        
+    lbool parallel::param_generator::run_prefix_step() {
+        IF_VERBOSE(1, verbose_stream() << " Param generator running prefix step\n");
+        ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts;
+        lbool r = l_undef;
+        try {
+            r = ctx->check();
+        } catch (z3_error &err) {
+            b.set_exception(err.error_code());
+        } catch (z3_exception &ex) {
+            b.set_exception(ex.what());
+        } catch (...) {
+            b.set_exception("unknown exception");
+        }
+        return r;
+    }
+
+    void parallel::param_generator::protocol_iteration() {
+        IF_VERBOSE(1, verbose_stream() << " Param generator running protocol iteration\n");
+        ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts;
+        lbool r = run_prefix_step();
+
+        switch (r) {
+            case l_undef: {
+                return;
+            }
+            case l_true: {
+                IF_VERBOSE(1, verbose_stream() << " Param tuning thread found formula sat\n");
+                model_ref mdl;
+                ctx->get_model(mdl);
+                b.set_sat(m_l2g, *mdl);
+                return;
+            }
+            case l_false: {
+                expr_ref_vector const &unsat_core = ctx->unsat_core();
+                IF_VERBOSE(2, verbose_stream() << " unsat core:\n";
+                           for (auto c : unsat_core) verbose_stream() << mk_bounded_pp(c, m, 3) << "\n");
+                IF_VERBOSE(1, verbose_stream() << " Param tuning thread determined formula unsat\n");
+                b.set_unsat(m_l2g, unsat_core);
+                return;
+            }
+        }
     }
 
     void parallel::worker::run() {
@@ -148,8 +187,8 @@ namespace smt {
     }
 
     parallel::param_generator::param_generator(parallel& p)
-        : p(p), b(p.m_batch_manager), m_params(p.ctx.get_fparams()), m_p(p.ctx.get_params()) {
-        ctx = alloc(context, m, m_params, m_p);
+        : p(p), b(p.m_batch_manager), m_best_param_state(p.ctx.get_fparams()), m_p(p.ctx.get_params()), m_l2g(m, p.ctx.m) {
+        ctx = alloc(context, m, m_best_param_state, m_p);
         context::copy(p.ctx, *ctx, true);
         // don't share initial units
         ctx->pop_to_base_lvl();
@@ -515,7 +554,7 @@ namespace smt {
             threads[i] = std::thread([&, i]() { m_workers[i]->run(); });
         }
         // the final thread runs the parameter generator
-        threads[num_threads - 1] = std::thread([&]() { m_param_generator.run(); });
+        threads[num_threads - 1] = std::thread([&]() { m_param_generator.protocol_iteration(); });
 
         // Wait for all threads to finish
         for (auto &th : threads)
diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h
index 106d413db..d8da5e34a 100644
--- a/src/smt/smt_parallel.h
+++ b/src/smt/smt_parallel.h
@@ -109,32 +109,38 @@ namespace smt {
             parallel& p;
             batch_manager& b;
             ast_manager m;
+            scoped_ptr<context> ctx;
+            ast_translation m_l2g;
+            
             unsigned N = 4; // number of prefix permutation testers
+            unsigned m_max_prefix_conflicts = 1000;
+            
             scoped_ptr<context> m_prefix_solver;
             scoped_ptr_vector<context> m_testers; // N testers
-            smt_params m_params;
+            smt_params m_best_param_state;
             params_ref m_p;
-            scoped_ptr<context> ctx;
             
             private:
                 void init_param_state() {
-                    m_params.m_nl_arith_branching = true;
-                    m_params.m_nl_arith_cross_nested = true;
-                    m_params.m_nl_arith_delay = 10;
-                    m_params.m_nl_arith_expensive_patching = false;
-                    m_params.m_nl_arith_gb = true;
-                    m_params.m_nl_arith_horner = true;
-                    m_params.m_nl_arith_horner_frequency = 4;
-                    m_params.m_nl_arith_optimize_bounds = true;
-                    m_params.m_nl_arith_propagate_linear_monomials = true;
-                    m_params.m_nl_arith_tangents = true;
+                    m_best_param_state.m_nl_arith_branching = true;
+                    m_best_param_state.m_nl_arith_cross_nested = true;
+                    m_best_param_state.m_nl_arith_delay = 10;
+                    m_best_param_state.m_nl_arith_expensive_patching = false;
+                    m_best_param_state.m_nl_arith_gb = true;
+                    m_best_param_state.m_nl_arith_horner = true;
+                    m_best_param_state.m_nl_arith_horner_frequency = 4;
+                    m_best_param_state.m_nl_arith_optimize_bounds = true;
+                    m_best_param_state.m_nl_arith_propagate_linear_monomials = true;
+                    m_best_param_state.m_nl_arith_tangents = true;
 
-                    m_params.updt_params(m_p);
+                    m_best_param_state.updt_params(m_p);
                     ctx->updt_params(m_p);
                 };
             public:
                 param_generator(parallel& p);
-                void run();
+                lbool run_prefix_step();
+                void protocol_iteration();
+                void replay_proof_prefixes();
 
                 reslimit& limit() {
                     return m.limit();