Fix #10303: unsound sat in nla when the LP model carries infinitesimals (#10307)

Fixes #10303.

## Symptom

On the reported QF_NRA instance z3 answers `sat` for some values of
`smt.random_seed` and `unsat` for others, and every `sat` comes with a
model z3's own validator rejects. The correct answer is `unsat`.
`smt.arith.solver=2` is unaffected; `smt.arith.solver=6` (the default)
is not.

## Root cause

The simplex model is not rational — each column is a `numeric_pair<mpq>`
`(x, y)` denoting `x + δ·y`, where `δ` is a positive infinitesimal used
to represent *strict* bounds exactly (`v > 0` is stored as `(0, 1)`).
`δ` only becomes concrete at model-output time, in
`from_model_in_impq_to_mpq(v) = v.x + m_delta * v.y`.

But nla decides monomial consistency using **only the rational parts**:

```cpp
const rational& val(lpvar j) const { return lra.get_column_value(j).x; }   // nla_core.h:165
r *= lra.get_column_value(j).x;                                            // product_value
return product_value(m) == lra.get_column_value(m.var()).x;                // check_monic
```

That is sound only on a δ-free model, and it cannot be repaired by also
tracking `y`: a **product** `(x₁+δy₁)(x₂+δy₂)` has a `δ²` term, which a
`numeric_pair` cannot represent. The delta encoding is inherently
linear, so nla structurally cannot reason on a δ-carrying model.

The code relies on this: `core::check()` calls
`lra.get_rid_of_inf_eps()` as its very first action to instantiate δ
before any monomial is inspected. The invariant is:

> `m_to_refine` must only ever be computed on a δ-free model.

`core::optimize_nl_bounds()` breaks it. It calls
`lra.find_feasible_solution()` in the middle of the nla check; the
simplex re-runs, parks columns back onto strict bounds and
**re-introduces non-zero `y`**. It then calls `init_to_refine()` on that
model — one full LP re-solve after the scrub in `core::check()`.

A wrong `m_to_refine` turns directly into a wrong answer:

```
find_feasible_solution() re-introduces δ
  → init_to_refine() mis-measures monomials (compares only .x)
  → m_to_refine wrongly empty
  → horner.cpp:117  set_nla_satisfied()
  → core::check()   returns l_true
  → theory_lra      FC_DONE  →  sat
  → model output instantiates δ  (x + m_delta·y)
  → monomial equations violated → "an invalid model was generated"
```

Instrumenting model construction on the reported benchmark confirms it
exactly: `use_nra_model=0`, **87 columns still carrying infinitesimals,
44 monomials violated** once δ is instantiated — every one of them with
`to_refine = 0`.

## Fix

Enforce the invariant where it is actually depended upon, instead of
only at the entry to `core::check()`:

```cpp
void core::init_to_refine() {
    if (lra.is_feasible())
        lra.get_rid_of_inf_eps();
    m_to_refine.reset();
    ...
}
```

Every caller — including the ones inside `optimize_nl_bounds()` that
follow an LP re-solve — now measures monomials on a δ-free model.

A second commit closes a related hole: the
`arith.nl.optimize_bounds_lp_max_vars` throttle exit returns *after*
`find_feasible_solution()` has already moved the model, and was the only
exit that never called `init_to_refine()` at all — leaving `m_to_refine`
stale rather than merely δ-contaminated.

## Validation

Reported benchmark, `tactic.default_tactic=smt` (deterministic — the
default QF_NRA portfolio uses wall-clock `try_for` budgets, so it is
timing-dependent): master fails on **9 of 20** seeds; with the fix
**20/20** answer `unsat`. Under the default configuration, seeds 1–10
all answer `unsat` (was `sat` + invalid model on 1, 3, 4, 10), matching
`smt.arith.solver=2`.

The bug was much broader than the single reported instance. On the
`QF_NRA_small` corpus (1147 instances, `-T:10`):

| | sat | unsat | unknown | invalid model |
|---|---|---|---|---|
| master | 460 | 597 | 77 | **13** |
| this PR | 466 | 602 | 79 | **0** |

**Zero sat/unsat conflicts.** Of the 13 instances where master emitted
an invalid model, **7 are genuinely `unsat`** — the same unsoundness as
the reported one.

## Performance

Net **faster**, on the 1054 instances answered identically before and
after:

| | total |
|---|---|
| master | 229.7 s |
| this PR | 146.4 s (**−36.3 %**) |

133 instances faster by >200 ms vs. 13 slower by >200 ms.

The added `get_rid_of_inf_eps()` is asymptotically free —
`init_to_refine()` already costs Θ(Σ|monic|) arbitrary-precision
*multiplications*, so adding Θ(#columns) `mpq::is_zero()` tests (which
early-exit when no deltas are present) does not change its complexity
class. The expensive path is also moved rather than added: deltas left
by `optimize_nl_bounds()` previously survived until the next
`core::check()`, which paid the full `find_delta_for_strict_bounds` +
rewrite cost anyway.

The speedup itself comes from correctness — a truthful `m_to_refine`
points grobner / basic_lemma / order / monotonicity / tangent / nra at
the monomials that are genuinely violated, instead of letting them chase
a model that was never consistent.

`test-z3 /a`: 93/93 pass.

---------

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

src/math/lp/nla_core.cpp

@@ -634,6 +634,16 @@ void core::erase_from_to_refine(lpvar j) {
 
 void core::init_to_refine() {
     TRACE(nla_solver_details, tout << "emons:" << pp_emons(*this, m_emons););
+    // check_monic() compares only the rational parts of the column values, so
+    // m_to_refine has to be calibrated against a model without infinitesimal
+    // (delta) components. Otherwise a monomial whose factors still carry
+    // non-zero delta parts looks consistent here, while the model handed to the
+    // theory solver - where delta is instantiated by a positive rational -
+    // violates it. optimize_nl_bounds() re-solves the LP and re-introduces
+    // delta components, so they are dropped here rather than only on entry to
+    // check().
+    if (lra.is_feasible())
+        lra.get_rid_of_inf_eps();
     m_to_refine.reset();
     unsigned r = random(), sz = m_emons.number_of_monics();
     for (unsigned k = 0; k < sz; ++k) {
@@ -1596,8 +1606,12 @@ bool core::optimize_nl_bounds() {
     // problems this pass is expensive and rarely productive, so skip it when the
     // candidate set exceeds the threshold (0 = unlimited).
     unsigned const max_vars = params().arith_nl_optimize_bounds_lp_max_vars();
-    if (max_vars != 0 && cands.size() > max_vars)
+    if (max_vars != 0 && cands.size() > max_vars) {
+        // find_feasible_solution() above already moved the model, so m_to_refine
+        // is stale on this path too and has to be re-calibrated before returning.
+        init_to_refine();
         return false;
+    }
 
     // Collect improved bounds first (each find_improved_bound maximizes a term
     // over the *unchanged* constraint set, so all improvements are valid implied