From 34964402b4986801c6a94ab51e5c7cc076565909 Mon Sep 17 00:00:00 2001
From: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Date: Sun, 12 Jul 2026 22:07:05 -0700
Subject: [PATCH] bugfix about child threads setting force_enable=false for
 parallel

---
 src/smt/smt_context.cpp  |  2 +-
 src/smt/smt_parallel.cpp | 18 +++++++++++++-----
 2 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 89326fa7ac..1bec94df1f 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3617,7 +3617,7 @@ namespace smt {
     }
 
     bool context::use_parallel_solver() const {
-        if (m.has_trace_stream() || m_par)
+        if (m.has_trace_stream())
             return false;
         smt_parallel_params pp(m_params);
         return m_fparams.m_threads > 1 || pp.force_enable();
diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 6b965c5e48..76c39b0c03 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -629,7 +629,9 @@ namespace smt {
         for (expr* e : _asms)
             asms.push_back(m_g2l(e));
         IF_VERBOSE(1, verbose_stream() << "Initialized core minimizer thread\n");
-        ctx = alloc(context, m, m_smt_params, p.ctx.get_params());
+        params_ref child_params(p.ctx.get_params());
+        child_params.set_bool("force_enable", false);
+        ctx = alloc(context, m, m_smt_params, child_params);
         ctx->set_logic(p.ctx.m_setup.get_logic());
         context::copy(p.ctx, *ctx, true);
         ctx->pop_to_base_lvl();
@@ -853,8 +855,9 @@ namespace smt {
             asms.push_back(m_g2l(e));
         LOG_WORKER(1, " created with " << asms.size() << " assumptions\n");
         m_smt_params.m_random_seed += id;  // ensure different random seed for each worker
-        ctx = alloc(context, m, m_smt_params, p.ctx.get_params());
-        ctx->m_par = &p;
+        params_ref child_params(p.ctx.get_params());
+        child_params.set_bool("force_enable", false);
+        ctx = alloc(context, m, m_smt_params, child_params);
         ctx->set_logic(p.ctx.m_setup.get_logic());
         context::copy(p.ctx, *ctx, true);
         // don't share initial units
@@ -880,6 +883,7 @@ namespace smt {
         : p(p), b(p.m_batch_manager), m(), m_g2l(p.ctx.m, m), m_l2g(m, p.ctx.m) {
         IF_VERBOSE(1, verbose_stream() << "Initialized SLS portfolio thread\n");
         m_params.append(p.ctx.m_params);
+        m_params.set_bool("force_enable", false);
         m_sls = alloc(sls::smt_solver, m, m_params);
     }
 
@@ -889,7 +893,9 @@ namespace smt {
             asms.push_back(m_g2l(e));
         IF_VERBOSE(1, verbose_stream() << "Initialized backbones thread " << id << "\n");
         m_mode = id == 0 ? bb_mode::bb_negated : bb_mode::bb_positive;
-        ctx = alloc(context, m, m_smt_params, p.ctx.get_params());
+        params_ref child_params(p.ctx.get_params());
+        child_params.set_bool("force_enable", false);
+        ctx = alloc(context, m, m_smt_params, child_params);
         ctx->set_logic(p.ctx.m_setup.get_logic());
         ctx->get_fparams().m_max_conflicts = m_bb_conflicts_per_chunk;
         context::copy(p.ctx, *ctx, true);
@@ -1060,7 +1066,9 @@ namespace smt {
         // run in-processing on the assertions
         s->reduce();
 
-        scoped_ptr<context> new_ctx = alloc(context, m, m_smt_params, p.ctx.get_params());
+        params_ref child_params(p.ctx.get_params());
+        child_params.set_bool("force_enable", false);
+        scoped_ptr<context> new_ctx = alloc(context, m, m_smt_params, child_params);
         // extract simplified assertions from the simplifier
         // create a new context with the simplified assertions
         // update ctx with the new context.