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

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