From 2d48fd119ce5074b880944c2b1c59e537c99cd46 Mon Sep 17 00:00:00 2001 From: "z3prover-ci-bot[bot]" <305651407+z3prover-ci-bot[bot]@users.noreply.github.com> Date: Sat, 25 Jul 2026 10:56:56 -0700 Subject: [PATCH] [snapshot-regression-fix] Fix nra_solver abort/output-leak on benign non-COI constraint violation (#10230) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Fixes a snapshot-regression divergence reported in [Z3Prover/bench discussion #3421](https://github.com/Z3Prover/bench/discussions/3421). - **Benchmark:** `iss-6061/delta.smt2` (from https://github.com/Z3Prover/z3/issues/6061) - **Recorded oracle:** `sat` - **Current (buggy) z3 output:** a large `constraint 19 violated` / `number of constraints = 602` diagnostic dump (and, in an assertion-enabled build, an `UNEXPECTED CODE WAS REACHED` abort at `nra_solver.cpp:245`). ### Divergence diff ```diff --- delta.expected.out (expected) +++ produced (current z3) @@ -1 +1,334 @@ -sat +constraint 19 violated +number of constraints = 602 +(0) j0 >= 1 +(1) j0 <= 1 ... +(19) j8 + j10 > 0 +(20) j8 + j10 >= 0 ... (160 more diff line(s)) ``` ## Root cause `nra_solver::imp::check()` runs nlsat over only the **cone-of-influence (COI)** subset of the LRA constraints. When nlsat returns `l_true`, the resulting model is validated against **all** LRA constraints/monics. Constraints outside the COI can be *legitimately* violated by that partial model — nlsat never assigned the variables that only occur outside the COI. This was previously handled by commit `8a146a92e` ("replace UNREACHABLE with VERIFY for non-COI constraint/monic violations", fixes #8883). The Nl2lin rewrite (`6fb68ac01`) reintroduced an **unconditional** `UNREACHABLE()` plus an `IF_VERBOSE(0, ...)` diagnostic dump for *any* violated constraint/monic, reverting that fix. For `delta.smt2`, constraint 19 (`j8 + j10 > 0`) is **not** in the COI (confirmed by instrumentation: `in_coi=0`). In a release build the reintroduced `UNREACHABLE()` is a no-op, so z3 correctly falls back to `l_undef` and ultimately answers `sat` — but the `IF_VERBOSE(0, ...)` dump still leaks to stderr, and the snapshot capture merges stderr into stdout, breaking the recorded oracle. In an assertion-enabled build the `UNREACHABLE()` aborts outright. ## Fix Only treat a violated constraint/monic as a genuine nlsat bug (verbose dump + `UNREACHABLE()`) when it is actually in the COI. A non-COI violation is benign, so return `l_undef` quietly without emitting any diagnostics. This restores the intent of `8a146a92e` and additionally stops the verbose dump from leaking for the benign case. ```cpp if (!check_constraint(ci)) { if (m_coi.constraints().contains(ci)) { IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n"; lra.constraints().display(verbose_stream())); UNREACHABLE(); } return l_undef; } ``` (analogous change for the monic check). ## Validation Rebuilt z3 from this branch (`make -j`) and re-ran the benchmark exactly as the snapshot capture does (combined stdout+stderr, `-T:20`): ``` $ z3 -T:20 inputs/issues/iss-6061/delta.smt2 2>&1 sat ``` The combined output is now exactly `sat`, byte-for-byte matching the recorded `delta.expected.out` oracle. Basic SMT solving sanity-checked and unaffected. Closes the divergence in Z3Prover/bench discussion #3421. > [!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/30150856651) · 239.4 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> --- src/math/lp/nra_solver.cpp | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index f5cc61ba9e..8fb383d475 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -240,16 +240,26 @@ struct solver::imp { lra.init_model(); for (lp::constraint_index ci : lra.constraints().indices()) if (!check_constraint(ci)) { - IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n"; - lra.constraints().display(verbose_stream())); - UNREACHABLE(); + // nlsat only solves over the cone-of-influence (COI) subset + // of constraints, so constraints outside the COI may be + // legitimately violated by the nlsat model. Only a violation + // of a COI constraint indicates a genuine nlsat bug; a + // non-COI violation is benign, so fall back to l_undef + // quietly without emitting diagnostics. + if (m_coi.constraints().contains(ci)) { + IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n"; + lra.constraints().display(verbose_stream())); + UNREACHABLE(); + } return l_undef; } for (auto const &m : m_nla_core.emons()) { if (!check_monic(m)) { - IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n"; - lra.constraints().display(verbose_stream())); - UNREACHABLE(); + if (m_coi.mons().contains(m.var())) { + IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n"; + lra.constraints().display(verbose_stream())); + UNREACHABLE(); + } return l_undef; } }