[snapshot-regression-fix] opt: preserve strict supremum/infimum optima with infinitesimal component (#10052)

## Summary

Fixes a Z3 optimization regression where maximizing a real objective
under a
**strict** inequality returned a plain feasible model value instead of
the
strict supremum.

Originating discussion:
https://github.com/Z3Prover/bench/discussions/3053
Benchmark: `iss-5720/bug-1.smt2` (in `Z3Prover/bench`)

```smt2
(declare-const r Real)
(assert (< r 1))
(maximize r)
(check-sat)
(get-objectives)
```

The optimum of `r` subject to `r < 1` is the strict supremum `1 -
epsilon`,
which the recorded oracle expects. Current z3 instead reports the
feasible
point `0`.

## Divergence

```diff
--- bug-1.expected.out (expected)
+++ produced (current z3)
@@ -1,4 +1,4 @@
 sat
 (objectives
- (r (+ 1.0 (* (- 1.0) epsilon)))
+ (r 0)
 )
```

## Root cause

Regression from commit `fdc32d0e6` ("Fix inconsistent optimization
result with
unvalidated LP bound", #10028). That change stopped committing the LP
optimization hint `val` to `m_objective_values` up front in
`opt_solver::maximize_objective`, deferring the commit until
`check_bound()`
validates it. Its goal is to reject **plain-rational** over-estimates
produced
when the objective shares symbols with other theories (e.g. the
auxiliary
uninterpreted function used to encode large `distinct` constraints);
those
over-estimates have a **zero** infinitesimal.

For a strict real supremum/infimum the hint has a **non-zero**
infinitesimal
(here `val = 1 - epsilon`). `check_bound()` can never validate it,
because
`opt_solver::mk_ge` drops the negative infinitesimal (mathematically,
`r >= 1 - epsilon` is equivalent over the reals to `r >= 1`), turning
the
validation bound into the unsatisfiable `r >= 1` given `r < 1`.
Validation
therefore fails, `maximize_objective` returns `false`, and
`m_objective_values`
is left holding the strictly smaller current **model** value (`0`),
which
`optsmt::geometric_lex` then reports as the optimum.

## Fix

`src/opt/opt_solver.cpp`, `maximize_objective`: restore the pre-#10028
eager
commit of the hint, **scoped to finite values with a non-zero
infinitesimal**:

```cpp
if (val.is_finite() && !val.get_infinitesimal().is_zero() && val > m_objective_values[i])
    m_objective_values[i] = val;
```

A finite value with a non-zero infinitesimal is a strict optimum that no
concrete model can attain and that `check_bound()` cannot validate, so
the
arithmetic hint is authoritative and must be preserved. Plain-rational
(zero-infinitesimal) values — including **all integer objectives** and
the
`#10028` shared-symbol over-estimates — do not enter this branch and
continue
through the deferred-commit validation path unchanged, so `#10028` is
structurally preserved. The change does not alter control flow or the
return
value, so the lex/box drivers behave as before.

## Validation

Built the patched `./z3` checkout (`./configure && make -C build
-j$(nproc)`)
and re-ran the benchmark with the same options the snapshot capture
uses:

```
$ ./build/z3 -T:20 inputs/issues/iss-5720/bug-1.smt2
sat
(objectives
 (r (+ 1.0 (* (- 1.0) epsilon)))
)
```

This is a **byte-exact match** with the recorded `bug-1.expected.out`
oracle.

Additional before/after checks on the rebuilt binary (baseline = current
nightly, unpatched):

| case | baseline | patched |
| --- | --- | --- |
| single strict-real max `r<1` | `r=0` ❌ | `r=1-eps` ✅ (target) |
| single strict-real min `r>1` | `r=0` ❌ | `r=1+eps` ✅ |
| non-strict real max `r<=1` | `r=1` ✅ | `r=1` ✅ |
| integer max `x<10` | `x=9` ✅ | `x=9` ✅ |
| bounded strict `2<r<5` | — | `r=5-eps` ✅ |
| box: two strict reals | — | both `-eps` ✅ |
| lex: nonstrict-real then int | `r=1,x=9` ✅ | `r=1,x=9` ✅ |
| lex: int then nonstrict-real | `x=9,r=5` ✅ | `x=9,r=5` ✅ |
| lex: all integer | `x=9,y=9` ✅ | `x=9,y=9` ✅ |
| lex: int then strict-real (final) | `x=9,r=0` ❌ | `x=9,r=1-eps` ✅ |

All well-defined lex/box cases are preserved, and a strict-real
objective as
the **final** lex objective is now also correct.

## Known limitation (pre-existing, honest disclosure)

Lexicographic optimization where a **non-final** objective is a strict
real
supremum (e.g. `maximize r` with `r<1`, *then* `maximize x`) remains
ill-defined: the supremum `1-epsilon` is not attained by any model, so
`optsmt::commit_assignment` asserting `r >= 1-epsilon` (which `mk_ge`
reduces to
`r >= 1`) contradicts `r < 1`. This corner is already mishandled by the
current
nightly (it returns `r=0`) and is not what discussion #3053 reports;
this patch
does not attempt to redefine that semantics. It changes only how that
corner
manifests, while fixing the reported single-objective divergence and all
well-defined cases above.

Draft for human review.




> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28733642068)
· 691.9 AIC · ⌖ 44.2 AIC · ⊞ 8.9K ·
[◷](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.63, model: claude-opus-4.8, id:
28733642068, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28733642068 -->

<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->

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

src/opt/opt_solver.cpp

@@ -342,6 +342,24 @@ namespace opt {
             return true;
         }
 
+        //
+        // A finite hint with a non-zero infinitesimal is a strict
+        // supremum/infimum (e.g. maximizing r subject to r < 1 yields
+        // 1 - epsilon).  No concrete model can attain such a value, and
+        // check_bound() below cannot validate it either: opt_solver::mk_ge
+        // drops the negative infinitesimal, turning the bound r >= 1 - epsilon
+        // into the unsatisfiable r >= 1.  Commit it eagerly here so that it is
+        // neither overwritten by the strictly smaller current model value in
+        // update_objective() nor lost when validation fails and this routine
+        // returns false (callers such as optsmt::geometric_lex then report
+        // m_objective_values as the optimum).  This restores the pre-#10028
+        // behavior for strict optima while leaving the plain-rational
+        // (zero-infinitesimal) over-estimates that #10028 fixed to the
+        // deferred-commit logic below.
+        //
+        if (val.is_finite() && !val.get_infinitesimal().is_zero() && val > m_objective_values[i])
+            m_objective_values[i] = val;
+
         //
         // retrieve value of objective from current model and update 
         // current optimal.