From 7c7ffbc9a48eb20c401357d320bcf27dd30b4819 Mon Sep 17 00:00:00 2001
From: "z3prover-ci-bot[bot]"
<305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Date: Wed, 29 Jul 2026 14:02:50 -0700
Subject: [PATCH] [snapshot-regression-fix] qe_mbp: restrict array-var-in-index
fallback to nested indices (#10292)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
## 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]
>
> Firewall blocked 1 domain
>
> 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.
>
>
> 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)
---------
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
---
src/qe/qe_mbp.cpp | 20 ++++++++++++++------
1 file changed, 14 insertions(+), 6 deletions(-)
diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index 752f9006f0..15ce274b6e 100644
--- a/src/qe/qe_mbp.cpp
+++ b/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 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;
}