mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-02 20:23:27 +00:00
Code Activity

[snapshot-regression-fix] Spacer: keep symbolic term_graph representatives to fix 'Stuck on a lemma' regression (#10237)

Browse source 
## Summary

Fixes a Spacer regression where a satisfiable HORN benchmark that
previously returned `sat` now returns `unknown` with `(:reason-unknown
"Stuck on a lemma")`.

- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/3420
- **Benchmark:** `iss-5561/bug-2.smt2` (`inputs/issues/iss-5561/` in
`Z3Prover/bench`)
- **Kind:** `diff` (semantic answer changed)

### Divergence

```diff
--- bug-2.expected.out (expected)
+++ produced (current z3)
@@ -1,2 +1,2 @@
-sat
-(:reason-unknown "")
+unknown
+(:reason-unknown "Stuck on a lemma")
```

## Root cause

`git bisect` (clean per-commit builds, `-T:20`) identifies the first bad
commit as **df8d23960** — *"qe2: fix nonlinear term introduced by
term_graph representative selection in MBP (#10186)"* — which modified
`term_graph::term_lt` in `src/qe/mbp/mbp_term_graph.cpp`.

That change made concrete model **values** win over non-eliminated
uninterpreted **constants** when electing equivalence-class
representatives (previously the documented invariant was *"prefer
uninterpreted constants over values"*). It was intended to keep `qe2`'s
one-shot output linear (avoiding e.g. `(* 2 x)` becoming `(* x1 x)`).

Spacer, however, shares this same term_graph machinery for model-based
projection when generalizing lemmas. Preferring the value makes a
non-eliminated state constant get substituted by its concrete model
value everywhere in the projected lemma. This **over-grounds** the lemma
to the specific model, so Spacer keeps regenerating an over-specialized
lemma at infinity level; each regeneration bumps it until
`old_lemma->get_bumped() >= 100`, at which point `add_lemma_core` throws
`default_exception("Stuck on a lemma")`
(`src/muz/spacer/spacer_context.cpp`), surfacing as `unknown`.

`qe2`'s projection and Spacer's lemma generalization both funnel through
the same `spacer_qel`/`mbp_qel`/`qel` term_graph paths, so there is no
clean, separately-validatable client seam at which to gate the new
behavior without threading a new context flag through several layers.

## Fix

Revert the `term_lt` value-preference block, restoring the long-standing
invariant *"prefer uninterpreted constants over values"* that Spacer's
projection relies on. The change is confined to `term_lt` and adds an
explanatory comment referencing this regression.

## Validation

Built the patched `./z3` checkout (mk_make + `make`) and re-ran the
benchmark with the snapshot capture options (`-T:20`):

```
$ z3 -T:20 inputs/issues/iss-5561/bug-2.smt2
sat
(:reason-unknown "")
```

This matches the recorded `bug-2.expected.out` oracle exactly. The
sibling benchmark `iss-5561/bug-1.smt2` and basic solving were also
spot-checked and unaffected.

## Caveat for reviewers

This is a straight revert of the `term_lt` portion of #10186, so that
PR's cosmetic improvement — keeping `apply qe2` output in linear
`QF_LIA` form (avoiding logically-equivalent nonlinear terms) — is
reintroduced. #10186 added no regression test, so that behavior could
not be re-validated here. A non-regressing reimplementation should make
the representative preference **client-controlled** (as the `XXX`
comment above `term_lt` already suggests): enable value-preference only
for one-shot QE tactics (`qe2`) while keeping symbolic representatives
for Spacer's MBP generalization. Opened as a **draft** for human review.




> [!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/30191159770)
· 572.3 AIC · ⌖ 20.4 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:
30191159770, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/30191159770 -->

<!-- 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: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
z3prover-ci-bot[bot] 2026-07-29 14:19:25 -07:00 • committed by GitHub
parent 7c7ffbc9a4
commit 3c685d368b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 24 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

43
src/qe/mbp/mbp_term_graph.cpp
View file

@ -708,8 +708,18 @@ expr *term_graph::mk_app_core(expr *e) {
return e;
expr_ref_buffer kids(m);
app *a = ::to_app(e);
for (expr *arg : *a)
kids.push_back(mk_app(arg));
for (expr *arg : *a) {
// Keep literal values (e.g. the coefficient 2 in (* 2 x)) as-is.
// Replacing a value with its non-value class representative (e.g. x1
// when (= x1 2) was added to the graph) can turn a linear coefficient
// into a free variable, producing a nonlinear term such as (* x1 x).
// Values are canonical and never need to be expressed through a
// symbolic representative.
if (m.is_value(arg))
kids.push_back(arg);
else
kids.push_back(mk_app(arg));
}
app *res = m.mk_app(a->get_decl(), a->get_num_args(), kids.data());
m_pinned.push_back(res);
return res;
@ -813,28 +823,23 @@ bool term_graph::term_lt(term const &t1, term const &t2) {
// prefer applications over variables (for non-ground)
// prefer uninterpreted constants over values
// prefer smaller expressions over larger ones
//
// Keeping uninterpreted constants as representatives is required by
// model-based projection clients such as Spacer: substituting a
// non-eliminated state constant with its concrete model value over-grounds
// the projected lemma (see Z3Prover/bench discussion #3420, benchmark
// iss-5561/bug-2.smt2).
//
// The complementary concern — that a literal value used as a coefficient
// (e.g. the 2 in (* 2 x)) could be displaced by a free variable x1 when
// (= x1 2) is in scope, yielding a nonlinear term (* x1 x) — is addressed
// separately in mk_app_core, which keeps literal values as-is and never
// replaces them with a non-value representative.
if (t1.get_num_args() == 0 || t2.get_num_args() == 0) {
if (t1.get_num_args() == t2.get_num_args()) {
if (m.is_value(t1.get_expr()) == m.is_value(t2.get_expr()))
return t1.get_id() < t2.get_id();
// Prefer values over non-var uninterpreted constants to avoid
// substituting numeric literals with free variables. This prevents
// non-linear terms like (x * x1) when x1=2 is added as a model
// constraint and 2 appears as a coefficient in (2 * x).
// Exception: if the non-value is a variable to eliminate, keep the
// old preference (non-value wins) so refine_repr can replace it.
auto is_elim_var = [&](term const &t) {
expr *e = t.get_expr();
return is_app(e) && m_is_var.contains(to_app(e)->get_decl());
};
bool t1_is_val = m.is_value(t1.get_expr());
bool t2_is_val = m.is_value(t2.get_expr());
// If the non-value is NOT a variable to eliminate, prefer the value
if (t1_is_val && !t2_is_val && !is_elim_var(t2))
return true; // t1 (value) preferred
if (t2_is_val && !t1_is_val && !is_elim_var(t1))
return false; // t2 (value) preferred
return m.is_value(t2.get_expr());
}
return t1.get_num_args() < t2.get_num_args();