From 912820338cf6bdad7744f9a5b421ae19dd2b230c Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 9 Jul 2026 15:48:15 +0000
Subject: [PATCH 1/2] Initial plan


From 2a26a5662c6e4101e0016ff78a9604f6f5d4d280 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 9 Jul 2026 16:39:52 +0000
Subject: [PATCH 2/2] Fix unsigned overflow in parallel solver conflict budget
 escalation

---
 src/smt/smt_parallel.cpp         | 11 +++++++++++
 src/smt/smt_parallel.h           |  4 +++-
 src/solver/parallel_tactical.cpp |  5 +++--
 3 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 5096d23144..1124a6d2c6 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -879,6 +879,17 @@ namespace smt {
         if (m_config.m_ablate_backtracking) {
             m_config.m_core_minimize = false;
         }
+
+        // Honour the user-visible smt.threads_max_conflicts parameter as the initial
+        // per-cube conflict budget.  The default value of that parameter is UINT_MAX,
+        // which means "no limit": workers run without a conflict ceiling and the
+        // cube-splitting machinery stays idle, giving behaviour consistent with
+        // Z3 4.12.x (portfolio of solvers, first to finish wins).  Users who
+        // explicitly set smt.threads_max_conflicts to a finite value opt into the
+        // cube-and-conquer regime and get splitting at that budget.
+        m_config.m_threads_max_conflicts = m_smt_params.m_threads_max_conflicts;
+        IF_VERBOSE(1, verbose_stream() << "Worker " << id << " m_threads_max_conflicts=" << m_config.m_threads_max_conflicts 
+                                       << " (from smt_params=" << m_smt_params.m_threads_max_conflicts << ")\n");
     }
 
     parallel::sls_worker::sls_worker(parallel& p)
diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h
index 4af58efbc9..8e5ebcf8f8 100644
--- a/src/smt/smt_parallel.h
+++ b/src/smt/smt_parallel.h
@@ -304,7 +304,9 @@ namespace smt {
 
             void update_max_thread_conflicts() {
                 // allow for backoff scheme of conflicts within the thread for cube timeouts.
-                m_config.m_threads_max_conflicts = (unsigned)(m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts);
+                // Use saturating arithmetic to avoid unsigned overflow / undefined behaviour.
+                double next = m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts;
+                m_config.m_threads_max_conflicts = (next >= (double)UINT_MAX) ? UINT_MAX : (unsigned)next;
             }
 
             void simplify();
diff --git a/src/solver/parallel_tactical.cpp b/src/solver/parallel_tactical.cpp
index 972379ea7c..803f54eb74 100644
--- a/src/solver/parallel_tactical.cpp
+++ b/src/solver/parallel_tactical.cpp
@@ -1025,8 +1025,9 @@ class parallel_solver {
         unsigned         m_num_initial_atoms = 0;
 
         void update_max_thread_conflicts() {
-            m_config.m_threads_max_conflicts = static_cast<unsigned>(
-                m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts);
+            // Use saturating arithmetic to avoid unsigned overflow / undefined behaviour.
+            double next = m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts;
+            m_config.m_threads_max_conflicts = (next >= (double)UINT_MAX) ? UINT_MAX : static_cast<unsigned>(next);
         }
 
         lbool check_cube(expr_ref_vector const& cube) {