From d1a85c4e811b27f540498cc5db66d48c4f44e5bb Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Sun, 5 Jul 2026 04:26:16 -0700
Subject: [PATCH] opt: preserve strict supremum/infimum optima with
 infinitesimal component

Maximizing a real objective under a strict inequality (e.g. `maximize r`
subject to `r < 1`) must yield the strict supremum `1 - epsilon`, but z3
was reporting a plain feasible model value (`0`).

Regression from commit fdc32d0e6 ("Fix inconsistent optimization result
with unvalidated LP bound", #10028), which stopped committing the LP
optimization hint to m_objective_values up front and instead defers the
commit until check_bound() validates it. That fix targets plain-rational
over-estimates produced by shared uninterpreted symbols (e.g. large
`distinct` encodings), which have a zero infinitesimal.

For a strict real supremum/infimum the hint has a non-zero infinitesimal
(`1 - epsilon`). check_bound() can never validate it because
opt_solver::mk_ge drops the negative infinitesimal, turning the bound
`r >= 1 - epsilon` into the unsatisfiable `r >= 1`. Validation therefore
fails, maximize_objective() returns false, and m_objective_values is left
holding the strictly smaller current model value, which callers such as
optsmt::geometric_lex report as the optimum.

Restore the pre-#10028 eager commit, scoped to finite values with a
non-zero infinitesimal. Such values are strict optima that no concrete
model can attain and that check_bound() cannot validate, so the arithmetic
hint is authoritative. Plain-rational (zero-infinitesimal) values,
including all integer objectives and the #10028 shared-symbol case, are
untouched and continue through the deferred-commit validation path.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/opt/opt_solver.cpp | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index eb8b4dd6cb..88e81184fd 100644
--- a/src/opt/opt_solver.cpp
+++ b/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.