From efe5e946f16ec223a91d15101cefc49fb197534d Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Fri, 10 Jul 2026 15:25:57 -0700
Subject: [PATCH] Fix unsigned overflow in parallel solver conflict budget
 escalation (#10076)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Z3 4.16.0 introduced a cube-and-conquer parallel solver that regressed
easy QF_LIRA problems from <1s to hanging indefinitely. Workers start
with a 1000-conflict budget and multiply by 1.5× on each timeout, but
after ~38 escalations the `unsigned` cast overflows, causing the budget
to oscillate chaotically (e.g. 3.27B → 618M → 927M → … never reaching a
stable large value). For sub-cubes that require more conflicts than any
value in the oscillation window, the worker loops forever.

## Changes

- **`src/smt/smt_parallel.h`** – `update_max_thread_conflicts()`:
replace raw `(unsigned)(mul * val)` cast with saturating arithmetic that
caps at `UINT_MAX`, eliminating the UB and the oscillation:
  ```cpp
// Before – UB when product > UINT_MAX, budget oscillates after ~38
escalations
  m_config.m_threads_max_conflicts =
(unsigned)(m_config.m_max_conflict_mul *
m_config.m_threads_max_conflicts);

  // After – saturates at UINT_MAX
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;
  ```

- **`src/solver/parallel_tactical.cpp`** – Identical
saturating-arithmetic fix in the `parallel_tactical2` worker's
`update_max_thread_conflicts()`, which is the code path actually
exercised for QF_LIRA problems.

- **`src/smt/smt_parallel.cpp`** – Worker's initial per-cube conflict
budget is now sourced from `m_smt_params.m_threads_max_conflicts` (the
user-visible `smt.threads.max_conflicts` parameter) instead of being
hardcoded to 1000, so users who leave the parameter at its default get
an unlimited initial budget matching Z3 4.12.x portfolio behaviour.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_parallel.cpp         | 2 ++
 src/smt/smt_parallel.h           | 4 +++-
 src/solver/parallel_tactical.cpp | 5 +++--
 3 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 5096d23144..d1df20a508 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -879,6 +879,8 @@ namespace smt {
         if (m_config.m_ablate_backtracking) {
             m_config.m_core_minimize = false;
         }
+
+        m_config.m_threads_max_conflicts = m_smt_params.m_threads_max_conflicts;
     }
 
     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) {