From 88448d4afd3cc9a5f9637949c31e827811ffec78 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Jul 2026 11:47:07 -0700 Subject: [PATCH] Fix unsound model from parallel QF_BV solving (#10133) (#10142) ## Problem Fixes #10133. For `QF_BV` with `parallel.enable=true`, the solver could return `sat` with a model that violates its own assertions. `mk_qfbv_tactic` routes SAT solving to `mk_psat_tactic`, which built the solver via `mk_inc_sat_solver(m, p, false)` (non-incremental). The parallel cube-and-conquer engine **reuses this single solver** across many `check_sat(cube)` calls, but SAT variable/blocked-clause elimination ran because the simplifier's incremental gate was disabled. Elimination model reconstruction is only sound for a single one-shot solve; under repeated cube assumptions it produces models where eliminated Tseitin variables get values contradicting the original clauses. ## Root cause (two coupled defects) 1. **Stale simplifier cache.** `inc_sat_solver`'s constructor called `m_solver.set_incremental()` *after* `updt_params()`. The SAT simplifier caches `m_incremental_mode` from the SAT config *during* `updt_params`, so setting the incremental flag afterwards left a stale non-incremental mode and elimination stayed enabled. (This is why simply passing `incremental_mode=true` had no effect on its own.) 2. **Non-incremental parallel solver.** `mk_psat_tactic` created the reused solver as non-incremental. ## Fix - Move `set_incremental()` **before** `updt_params()` in the `inc_sat_solver` constructor so the simplifier caches the correct mode. - Create the parallel solver with `incremental_mode=true` in `mk_psat_tactic`. ## Validation - Variable elimination on the QF_BV parallel path drops to zero (`sat-elim-bool-vars-res` 21664 -> 0); remaining `elim-clauses/literals` are sound cleaner/subsumption steps. - Consistent with ground truth: on 4.16.0, `sat.elim_vars=false` removed all 7 `failed to verify` errors; this change disables exactly that unsound elimination, scoped to the reused/parallel solver. - A solvable QF_BV instance returns a **valid** model under `parallel.enable=true model_validate=true`. - All 92 unit tests pass (`test-z3 /a`). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/sat/sat_solver/inc_sat_solver.cpp | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index c12984193..42b2d310e 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -100,10 +100,17 @@ public: m_unknown("no reason given"), m_internalized_converted(false), m_internalized_fmls(m) { + // Establish the incremental flag on the SAT core *before* updt_params + // propagates parameters to the simplifier. The simplifier caches + // m_incremental_mode from the SAT config during its own updt_params, so + // the incremental flag must already be set; otherwise the simplifier + // keeps a stale non-incremental mode and applies variable/blocked-clause + // elimination even when the solver is meant to be reused incrementally + // (unsound model reconstruction, issue #10133). + m_solver.set_incremental(incremental_mode && !override_incremental()); updt_params(p); m_mcs.push_back(nullptr); init_preprocess(); - m_solver.set_incremental(incremental_mode && !override_incremental()); } bool override_incremental() const { @@ -1297,6 +1304,12 @@ void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* sof tactic * mk_psat_tactic(ast_manager& m, params_ref const& p) { parallel_params pp(p); if (pp.enable()) - return mk_parallel_tactic(mk_inc_sat_solver(m, p, false), p); + // The parallel (cube-and-conquer) tactic reuses this solver across many + // check_sat calls with different cube assumptions. Create it in incremental + // mode so the SAT simplifier does not apply variable/blocked-clause + // elimination: those in-processing steps are only model-sound for a single + // one-shot solve, and reusing an eliminated solver under new cube + // assumptions produces models that violate the original clauses (issue #10133). + return mk_parallel_tactic(mk_inc_sat_solver(m, p, true), p); return mk_sat_tactic(m); }