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>
`batch_manager::set_unknown()` in the parallel SMT tactic changed
`m_state` to `is_unknown` but never notified backbone workers or the
core-minimizer worker waiting on `m_bb_cv` / `m_core_min_cv`. Those
threads blocked indefinitely, deadlocking `solve()` at `t.join()`.
### Root cause
```
(declare-fun a (Int) Bool)
(declare-fun b (Int) Bool)
(assert (distinct a b))
(check-sat-using psmt)
```
Every CDCL worker returns `l_undef` with reason `(incomplete (theory
array))`. The first worker calls `set_unknown()` (a soft verdict — other
workers may still find sat/unsat) and exits. Other CDCL workers exit
when `get_cube()` checks `m_state != is_running`. Meanwhile, backbone
workers and the core minimizer are already blocked in
`wait_for_backbone_job()` / `wait_for_core_min_job()`, both of which
condition-wait on CVs that `set_unknown()` never signals. Their
predicates check `m_state != is_running`, but a CV predicate only
re-evaluates on notification or spurious wakeup.
### Fix
- **`src/solver/parallel_tactical.cpp`** — `set_unknown()` now calls
`m_bb_cv.notify_all()` and `m_core_min_cv.notify_all()` after setting
the terminal state, so waiting helper threads observe the change and
exit via the existing `m_state != is_running` guard in their wait
predicates.
### Test
- **`src/test/psmt.cpp`** — new regression covering SAT, UNSAT, and the
theory-incomplete (deadlock) path using `(as-array f)` terms to
reproduce the exact array-theory incompleteness that triggers
`set_unknown()`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Summary
Fixes a `psmt` (parallel SMT tactic) regression where the solver hangs
to a wall-clock timeout instead of returning `unknown` on formulas whose
root cube is genuinely undetermined by an incomplete theory.
- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/2735
- **Benchmark:** `iss-3044/bug-1.smt2` (from [Z3 issue
#3044](https://github.com/Z3Prover/z3/issues/3044))
```smt2
(declare-fun a (Int) Bool)
(declare-fun b (Int) Bool)
(assert (distinct a b))
(check-sat-using psmt)
```
## Divergence
The recorded oracle (expected) vs. current z3 (combined stdout+stderr,
`-T:20`):
```diff
-(incomplete (theory array))
-unknown
+timeout
```
## Root cause
The rewritten parallel tactic (`src/solver/parallel_tactical.cpp`,
introduced in #9824/#9825) hangs on this input.
In the worker `run()` loop, every `l_undef` cube result was treated as
if the per-cube **conflict limit** had been reached: the worker
escalated the per-thread conflict budget (`update_max_thread_conflicts`)
and re-checked / re-split the same cube. When the `l_undef` actually
comes from **theory incompleteness** (here, the array theory cannot
decide `(distinct a b)` over `Int -> Bool`) rather than the conflict
limit, the verdict never changes, so the worker re-checks the same cube
forever.
Compounding this, the `batch_manager` state machine had **no terminal
`unknown` state** — the only way to finish was for some worker to prove
`sat`/`unsat`, which is impossible for a root-level theory-incomplete
formula. The combination produced an infinite loop and a wall-clock
timeout.
The pre-rewrite parallel tactic avoided this: its `giveup()` detected
reasons starting with `(incomplete` / `(sat.giveup`, reported a soft
undef, and echoed the reason to `verbose_stream()`.
## Fix
All changes are confined to `src/solver/parallel_tactical.cpp` (47
insertions, 4 deletions):
1. **Distinguish genuine incompleteness from conflict-limit
exhaustion.** In the worker `l_undef` case, only `reason_unknown() ==
"max-conflicts-reached"` benefits from escalating the budget /
splitting. For any other reason (incomplete theory, quantifiers,
lambdas, resource limits, ...) re-checking is futile, so the worker
records a sound `unknown` and stops working the branch.
2. **Add a terminal `is_unknown` batch-manager state** (`set_unknown`,
`get_result() -> l_undef`, reason storage). It is a *soft* result: it
does not cancel the other workers, and a definitive `sat`/`unsat`
verdict from another branch may still override it (the
`set_sat`/`set_unsat` guards now permit overriding `is_unknown`). All
`set_unsat` call sites are global formula-unsat (core ⊆ assumptions, or
independent of the tested backbone literal), so the override is sound;
tree-closure unsat remains guarded by `is_running` and cannot fire
because the undef leaf stays open.
3. **Restore the reason output.** The captured `reason_unknown` is
propagated to the result goal and echoed to `verbose_stream()`,
reproducing the `(incomplete (theory array))` line that the sequential
path / old parallel tactic emitted.
## Validation
Rebuilt the `./z3` checkout (`./configure && make -C build -j16`) and
re-ran the benchmark with the freshly built binary using the same
options the snapshot capture uses (`-T:20`, combined stdout+stderr):
```
$ z3 inputs/issues/iss-3044/bug-1.smt2 -T:20
(incomplete (theory array))
unknown
```
This matches the recorded `bug-1.expected.out` oracle **byte-for-byte**,
and the benchmark now completes in ~0.5s (was: timeout). Verified stable
across 8 consecutive runs. Basic `psmt` `sat`/`unsat` checks continue to
produce correct results.
Opened as a **draft** for human review.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28313246856)
· 5.7K AIC · ⌖ 85.8 AIC · ⊞ 41.2K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests)
<!-- gh-aw-agentic-workflow: Fix a Z3 snapshot-regression divergence,
engine: copilot, version: 1.0.60, model: claude-opus-4.8, id:
28313246856, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28313246856 -->
<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Problem
The [master WebAssembly
Build](https://github.com/Z3Prover/z3/actions/runs/28306680131) fails
with:
```
../src/solver/parallel_tactical.cpp:59:9: error: redefinition of 'mk_parallel_tactic'
59 | tactic* mk_parallel_tactic(solver* s, params_ref const& /* p */) {
../src/solver/parallel_tactical.cpp:55:9: note: previous definition is here
```
## Cause
Commit 7564ccc3f (an unrelated lar_solver change) accidentally renamed
the dead `mk_parallel_tactic2` stub to `mk_parallel_tactic`, leaving two
identical definitions inside the `#ifdef SINGLE_THREAD` block. The WASM
build defines `SINGLE_THREAD`, so it hits the redefinition.
## Fix
`mk_parallel_tactic2` and its `non_parallel_tactic2` class were never
referenced anywhere. This removes the dead stub and orphaned class,
keeping the single `mk_parallel_tactic` that degrades to
`mk_solver2tactic(s)` in single-threaded mode (added in #9977).
Verified both `SINGLE_THREAD` and multi-threaded paths pass
`-fsyntax-only`.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Capture row as a pointer as lambda strips the reference and the vector was copied by value in lar_solver!
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add new parallel algorithm as a tactic (parallel_tactical2.cpp)
Don't port over old experiments from smt_parallel that we aren't using
(sls, inprocessing, failed_literal_mode for bb detection)
Fix bugs: lease cancellation/reslimit race condition, involves changing
lease epoch to simple boolean flag
Also, now there is a single shared set of params for the tactic and
smt_parallel
**Test runs for the parallel_tactical2 vs old smt_parallel version:**
run-2747-Z3-threads-4-qflia-30s-stats.md
run-2746-Z3-threads-4-qflia-30s-parallel_tactic-stats.md
run-2745-Z3-threads-1-qfbv-30s-stats.md
run-3013-Z3-threads-4-qfbv-30s-parallel_tactic-stats.md --> note this is
indeed run-3013, I reran after a bugfix in inc_sat_solver
run-2743-Z3-threads-4-qfnia-30s-stats.md
run-2742-Z3-threads-4-qfnia-30s-parallel_tactic-stats.md
**Test runs for the new smt_parallel with bugfixes:**
run-2801-Z3-threads-4-qflia-30s-smtparallel-bugfixes-stats.md,
run-2800-Z3-threads-4-qflia-30s-smtparallel-bugfixes-stats.md
run-2797-Z3-threads-4-qfnia-30s-smtparallel-bugfixes-stats.md
compare to old smt_parallel:
run-2747-Z3-threads-4-qflia-30s-stats.md
run-2743-Z3-threads-4-qfnia-30s-stats.md
Note that there is a slight regression on lia in run-2800. The source of
this appears to be the new new LP largest-cube LIA heuristic param,
which is enabled by default. disabling this param in run-2801 restored
performance (I didn't change this in this PR though, just something to
note)
http://mtzguido.tplinkdns.com:8081/z3/compare_stats.html
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.localdomain>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
