mirror of
https://github.com/Z3Prover/z3
synced 2026-07-27 01:12:40 +00:00
ae190b8b88
Under `parallel.enable=true`, QF_BV workers that exhaust their per-cube
conflict budget (1000) are misclassified as unrecoverably incomplete,
causing the portfolio to return `unknown` in ~1 second instead of
escalating the budget and continuing.
## Root cause
`parallel_tactical.cpp` only recognizes `"max-conflicts-reached"` (the
`smt::context` spelling) as a signal to escalate the conflict budget.
SAT-core-backed solvers — which QF_BV workers use — report the same
condition as `"sat.max.conflicts"` (from
`sat_solver::reached_max_conflicts()`). The mismatch causes every QF_BV
cube attempt to fall through to `b.set_unknown()` instead of
`update_max_thread_conflicts()`.
## Fix
```diff
- if (reason != "max-conflicts-reached") {
+ if (reason != "max-conflicts-reached" && reason != "sat.max.conflicts") {
```
Both spellings now correctly route to the budget-escalation path. The
parallel `smt_parallel.cpp` path is unaffected — it owns `smt::context`
workers, which can only produce `"max-conflicts-reached"`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
|
||
|---|---|---|
| .. | ||
| assertions | ||
| check_logic.cpp | ||
| check_logic.h | ||
| check_sat_result.cpp | ||
| check_sat_result.h | ||
| CMakeLists.txt | ||
| combined_solver.cpp | ||
| combined_solver.h | ||
| combined_solver_params.pyg | ||
| mus.cpp | ||
| mus.h | ||
| parallel_params.pyg | ||
| parallel_tactical.cpp | ||
| parallel_tactical.h | ||
| preferred_value_propagator.h | ||
| progress_callback.h | ||
| simplifier_solver.cpp | ||
| simplifier_solver.h | ||
| slice_solver.cpp | ||
| slice_solver.h | ||
| smt_logics.cpp | ||
| smt_logics.h | ||
| solver.cpp | ||
| solver.h | ||
| solver2tactic.cpp | ||
| solver2tactic.h | ||
| solver_na2as.cpp | ||
| solver_na2as.h | ||
| solver_pool.cpp | ||
| solver_pool.h | ||
| solver_preprocess.cpp | ||
| solver_preprocess.h | ||
| tactic2solver.cpp | ||
| tactic2solver.h | ||