From 3c685d368b7ea8ab0e26fa37a3c9de23dd74eb47 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:19:25 -0700 Subject: [PATCH] [snapshot-regression-fix] Spacer: keep symbolic term_graph representatives to fix 'Stuck on a lemma' regression (#10237) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## 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] >
> 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/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) --------- 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> --- src/qe/mbp/mbp_term_graph.cpp | 43 +++++++++++++++++++---------------- 1 file changed, 24 insertions(+), 19 deletions(-) diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp index 3d02cd7f85..93bbd5ef28 100644 --- a/src/qe/mbp/mbp_term_graph.cpp +++ b/src/qe/mbp/mbp_term_graph.cpp @@ -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();