[snapshot-regression-fix] bv_rewriter: keep (= var concat) intact so DER can eliminate the bound variable (iss-4525/bug-7) (#10034)

## 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)

<!-- gh-aw-agentic-workflow: Fix a Z3 snapshot-regression divergence,
engine: copilot, version: 1.0.63, model: claude-opus-4.8, id:
28646063005, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28646063005 -->

<!-- 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>

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