mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 09:22:41 +00:00
Code Activity

Fix unsigned overflow in parallel solver conflict budget escalation

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-09 16:39:52 +00:00 • committed by GitHub
parent 912820338c
commit 2a26a5662c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 17 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/smt_parallel.cpp
View file

@ -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)

4
src/smt/smt_parallel.h
View file

@ -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();

5
src/solver/parallel_tactical.cpp
View file

@ -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) {