From cc5a2dae5e3efd42ffae50c694e2128b660c5495 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Fri, 3 Jul 2026 13:38:56 -0700 Subject: [PATCH] [snapshot-regression-fix] bv_rewriter: keep (= var concat) intact so DER can eliminate the bound variable (iss-4525/bug-7) (#10034) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Fixes the snapshot-regression divergence reported in Z3Prover/bench discussion **#2977** — https://github.com/Z3Prover/bench/discussions/2977 — for benchmark **`iss-4525/bug-7.smt2`**. ## Divergence The benchmark's second query `(check-sat-using (then simplify ctx-solver-simplify))` regressed from `sat` to `unknown`: ```diff --- bug-7.expected.out (expected) +++ produced (current z3) @@ -1,2 +1,2 @@ sat -sat +unknown ``` The input sets `:rewriter.split_concat_eq true` and `:smt.threads 3`, and its core assertion has the shape `(not (forall ((q11 (_ BitVec 21)) ...) (not (= q11 q9 q11 (concat #b01111000010 s)))))`. ## Root cause With `split_concat_eq` enabled, `bv_rewriter::mk_eq_concat` rewrites an equality `(= x (concat ...))` into per-slice **extract** equalities, e.g. `(= (extract 9 0 x) s) ∧ (= (extract 20 10 x) #b01111000010)`. When `x` is a **bound (de Bruijn) variable**, this is harmful: destructive equality resolution (`der.cpp`) only recognises the pattern `(= VAR t)` to eliminate a bound variable. After the split, the variable only appears under `extract`, so DER can no longer eliminate it and a **residual quantifier** survives `simplify`. Discharging that residual quantifier is then left to the solver invoked inside `ctx-solver-simplify`. That solver is where the observable regression actually lives: with `smt.threads ≥ 2` the parallel solver (`smt_parallel.cpp`) now returns `unknown` on the quantified cube instead of solving it (the older, oracle-era parallel solver kept splitting and proved it), so `ctx-solver-simplify` can no longer reduce `(not (forall ...))` to `true` and reports `unknown`. Reproduced with an A/B comparison of an oracle-era build (`sat` / correct) vs. current tip (`unknown`); the sequential path (`threads=1`) is unaffected. Rather than touch the parallel solver — whose current early-exit behaviour is a deliberate termination fix and is risky to revert — this change removes the condition that *creates* the residual quantifier in the first place, so the goal is solved by `simplify` alone and no longer depends on the parallel solver's completeness. ## Fix In `bv_rewriter::is_concat_split_target`, exclude a bare variable from being a split target: ```diff - m_split_concat_eq || + (m_split_concat_eq && !is_var(t)) || m_util.is_concat(t) || m_util.is_numeral(t) || m_util.is_bv_or(t); ``` `split_concat_eq` is only a bit-blasting heuristic, so skipping it for `(= var concat)` is sound and restores DER-based variable elimination. Ground terms are `app` nodes (never `var` nodes), so **default behaviour** (`split_concat_eq` is off by default) **and all ground uses are completely unchanged** — only the explicitly-enabled option with a bound-variable operand is affected. ## Validation - Rebuilt the checkout (`./configure && make -C build`) with the fix. - Re-ran the benchmark with the capture options (`z3 -T:20 inputs/issues/iss-4525/bug-7.smt2`): output is now `sat` / `sat`, an **exact match** to the recorded `bug-7.expected.out` oracle, deterministic across repeated runs. - Confirmed the mechanism: `(apply (then simplify))` with `split_concat_eq` enabled now empties the goal (DER eliminates the bound variable), whereas before it left a residual quantifier. - Confirmed `split_concat_eq` still splits **ground** `(= (concat a b) c)` equalities into extract-equalities (intended behaviour preserved). - Ran the relevant `test-z3` unit suites — all pass: `ast`, `bit_vector`, `fixed_bit_vector`, `simplifier`, `bit_blaster`, `var_subst`, `arith_rewriter`, `seq_rewriter`, `factor_rewriter`, `quant_solve`, `euf_bv_plugin`. Opened as a **draft** for human review. Note the transparency caveat above: the deeper behavioural regression is in the parallel solver's handling of quantified cubes; this patch resolves the reported divergence robustly at the rewriter/DER layer instead of altering that solver. > Generated by [Fix a Z3 snapshot-regression divergence](https://github.com/Z3Prover/bench/actions/runs/28646063005) · 989.2 AIC · ⌖ 40.3 AIC · ⊞ 8.9K · [◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/rewriter/bv_rewriter.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 6f6a121e48..b2ae76dd78 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -2678,8 +2678,15 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { } bool bv_rewriter::is_concat_split_target(expr * t) const { + // A bare (de Bruijn) variable is deliberately excluded as a split target: + // splitting (= x (concat ...)) into per-slice extract equalities rewrites + // an eliminable (= VAR t) equality into (= (extract .. VAR) t) fragments + // that destructive equality resolution (der) can no longer use to eliminate + // the bound variable, turning solvable quantified goals into residual + // quantifiers. Splitting is only a bit-blasting heuristic, so skipping it + // here is sound and preserves der-based variable elimination. return - m_split_concat_eq || + (m_split_concat_eq && !is_var(t)) || m_util.is_concat(t) || m_util.is_numeral(t) || m_util.is_bv_or(t);