[snapshot-regression-fix] Fix nra_solver abort/output-leak on benign non-COI constraint violation (#10230)

## 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:👿: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]
> <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/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)

<!-- gh-aw-agentic-workflow: Fix a Z3 snapshot-regression divergence,
engine: copilot, version: 1.0.65, model: claude-opus-4.8, id:
30150856651, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/30150856651 -->

<!-- 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>

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;
                 }
             }