From 28e9610a1f8a3e2dee74a9286c196767c2ef93b5 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Sun, 5 Jul 2026 00:41:18 -0700
Subject: [PATCH] opt: preserve strict-inequality (infinitesimal) optima in
 maximize_objective

Box/lex optimization over an open interval (e.g. minimize/maximize a Real
x under `x > 16/5 && x < 127/10`) regressed to reporting arbitrary feasible
interior points (37/10, 117/10) instead of the true infimum/supremum with
infinitesimals (16/5 + epsilon, 127/10 - epsilon).

Root cause: commit fdc32d0e6 (#10028/#10040) stopped committing the
arithmetic optimization hint `val` unless it is re-validated by
check_bound(). That fix is correct for objectives that share symbols with
other theories, where the LP hint can over-estimate an unachievable
optimum. But check_bound() cannot validate a strict/open optimum: such a
value carries a non-zero infinitesimal, and mk_ge() drops the infinitesimal
when building the bound literal (it is not expressible as an arithmetic
atom). So `x >= c - epsilon` becomes the strictly stronger `x >= c`, which
is unsatisfiable together with the original `x < c`; the check fails and the
correct optimum is discarded in favour of an interior model point.

Fix: in check_bound(), trust `val` when it has a non-zero infinitesimal --
it is the exact optimum of the arithmetic relaxation and cannot be
re-validated by re-asserting a (necessarily weaker) rational bound. The
zero-infinitesimal path (integer/rational objectives, including the #10028
shared-symbol case) is unchanged.

Validated by rebuilding z3 and re-running the benchmark: output now matches
the recorded oracle. Closed-interval, integer-strict, unbounded, and lex
cases were also checked and the #10028 distinct-minimize case remains
consistent.

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

diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index eb8b4dd6cb..4015cb5b91 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -361,6 +361,21 @@ namespace opt {
         // 
         auto check_bound = [&]() {
             SASSERT(has_shared);
+            //
+            // A strict (open) optimum is represented with a non-zero
+            // infinitesimal, e.g. the supremum of 'x' subject to 'x < c' is
+            // 'c - epsilon'.  Such a bound cannot be re-validated here:
+            // mk_ge() drops the infinitesimal when constructing the bound
+            // literal (an infinitesimal is not expressible as an arithmetic
+            // atom), so 'x >= c - epsilon' is turned into the strictly
+            // stronger 'x >= c', which is unsatisfiable together with the
+            // original 'x < c' and makes this check spuriously fail.  The
+            // infinitesimal value is the exact optimum of the arithmetic
+            // relaxation, so trust it rather than discarding it in favour of
+            // an arbitrary interior model point.
+            //
+            if (!val.get_infinitesimal().is_zero())
+                return true;
             return bound_value(i, val) && l_true == m_context.check(0, nullptr);
         };