[snapshot-regression-fix] qe_mbp: restrict array-var-in-index fallback to nested indices (#10292)

## Summary

Fixes a **completeness regression** in `qe_mbp` uncovered by the
snapshot-regression corpus.

- Originating discussion:
https://github.com/Z3Prover/bench/discussions/3445
- Benchmark ref: `iss-5925/small.smt2` (`Z3Prover/bench`,
`inputs/issues/iss-5925/`)

### Divergence

```diff
--- small.expected.out (expected)
+++ produced (current z3)
@@ -1 +1 @@
-unsat
+unknown
```

The benchmark is `(check-sat-using qe2)` over a formula that eliminates
an array variable `r` used **directly** as a store index: `(store (store
a v true) r true)`.

### Root cause

Commit 5bd9e6a00 ("Fix #7259, #7036: unsound MBP array projection with
array var in select/store index") added `has_array_var_in_index`, which
routes `spacer_qel` to the classic model-based projection
(`spacer_qe_lite`) whenever an eliminated array variable occurs anywhere
in a select/store index position. That guard is **too broad**: it also
fires when the array variable is used *directly* as an index (e.g. `r`
in `(store base r val)`). For `iss-5925/small.smt2` the fallback path
cannot decide the goal and returns `unknown` instead of the correct
`unsat`.

Using an array variable *directly* as an index is sound under `mbp_qel`:
the index is exactly that variable, and its model value is substituted
soundly. The genuine unsoundness of #7259/#7036 arises only when the
variable is **nested inside a compound index term** that the
partial-array-equality class-merge can silently rewrite (e.g. `(select
va (= v va))` becoming `(select v true)`).

### Fix

Restrict `has_array_var_in_index` to the dangerous nested case by
skipping index arguments that are *exactly* the array variable (`v !=
idx && occurs(v, idx)`). This keeps the #7259/#7036 soundness fallback
intact while restoring `qe2` completeness for direct-index benchmarks.

### Validation

Built z3 from this checkout (`make -j`, Release) and re-ran with
`-T:20`:

- `inputs/issues/iss-5925/small.smt2`: `unknown` (before) -> **`unsat`**
(after), matching the recorded oracle.
- `inputs/issues/iss-5925/delta.smt2`: still `unknown`, matching its
oracle.
- Reconstructed #7259 case `(select va (= v va))` under `qe2`: still
**`unsat`** (fallback still triggers for the nested-index case) -
soundness preserved.
- Unit tests `test-z3 mbp_qel` and `test-z3 qe_arith`: **PASS**.

Opened as a draft for human review. Please double-check the soundness
argument against the exact #7036 reproducer, which was not available in
the checkout.




> [!WARNING]
> <details>
> <summary>Firewall blocked 1 domain</summary>
>
> The following domain was blocked by the firewall during workflow
execution:
>
> - `pypi.org`
>> To allow these domains, add them to the `network.allowed` list in
your workflow frontmatter:
>
> ```yaml
> network:
>   allowed:
>     - defaults
>     - "pypi.org"
> ```
>
> See [Network
Configuration](https://github.github.com/gh-aw/reference/network/) for
more information.
>
> </details>


> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/30425630832)
· 287.3 AIC · ⌖ 20.1 AIC · ⊞ 10.7K ·
[◷](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.65, model: claude-opus-4.8, id:
30425630832, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/30425630832 -->

<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->

---------

Co-authored-by: z3prover-ci-bot[bot] <305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>

src/qe/qe_mbp.cpp

@@ -424,10 +424,16 @@ public:
     // The array term-graph projection (mbp_qel) treats an array equality
     // (= a b) as an implicit partial array equality and eliminates it via
     // class-merging. That rewrite is unsound when such an equality (or an
-    // array variable being eliminated) occurs inside a select/store *index*
-    // position, because the index is a first-class term whose value must be
-    // preserved. Detect that situation so we can fall back to the classic,
-    // model-based projection which handles it correctly (issues #7259, #7036).
+    // array variable being eliminated) occurs *nested inside* a select/store
+    // *index* position, because the index is a first-class term whose value
+    // must be preserved and the merge can silently change it (for example
+    // (select va (= v va)) becomes (select v true), issues #7259, #7036).
+    //
+    // An array variable that appears *directly* as an index (e.g. the store
+    // index r in (store base r val)) is not affected by this rewrite: the
+    // index is exactly that variable and mbp_qel substitutes its model value
+    // soundly. Only flag the dangerous case where the variable occurs as a
+    // proper subterm of a compound index term.
     bool has_array_var_in_index(app_ref_vector const& vars, expr* fml) {
         array_util au(m);
         ptr_vector<app> arr_vars;
@@ -448,9 +454,11 @@ public:
             // value; everything in between is an index argument.
             unsigned n = a->get_num_args();
             unsigned last = is_st ? n - 1 : n;
-            for (unsigned i = 1; i < last; ++i)
-                if (any_of(arr_vars, [&](app* v) { return occurs(v, a->get_arg(i)); }))
+            for (unsigned i = 1; i < last; ++i) {
+                auto idx = a->get_arg(i);
+                if (any_of(arr_vars, [&](app* v) { return idx != v && occurs(v, idx); }))
                     return true;
+            }
         }
         return false;
     }