From 835679b27d2d6db72a7ecd0e8ff08037aea1dd63 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Mon, 6 Jul 2026 12:56:13 -0700
Subject: [PATCH] Revert #10052: eager-commit of infinitesimal LP hint is
 unsound for shared-symbol objectives (#10057)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

## Summary

Reverts #10052, whose eager-commit of infinitesimal LP hints is
**unsound** for shared-symbol objectives.

#10052 added, in `opt_solver::maximize_objective`:

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

on the premise that *"a non-zero infinitesimal ⇒ an exact, unattainable
strict optimum, so the LP hint is authoritative."* That holds for a
**pure LP**, but is **false when the objective is a shared symbol** with
another theory (e.g. the auxiliary uninterpreted function used to encode
a `distinct` with > 32 arguments). There the LP relaxation only yields a
*hint* that can be a strict **over-estimate**, and #10052 commits it
without validation — exactly the class of bound that #10028's
`check_bound` exists to reject.

## Counterexample

A 6-mark Golomb ruler over integers `x0..x5`, with the `distinct` padded
to > 32 arguments so `x5` becomes a shared symbol; objective is a real
`obj` with `obj > x5` (full file attached to #5720):

- Ground truth: `minimize x5` (integer) ⇒ **17**; since `obj > x5`, the
true optimum is **`17 + ε`**.
- With #10052, z3 reports **`(obj (+ 5.0 epsilon))`** — wrong and
**infeasible** (`obj < 6` is `unsat`; the returned model itself has `x5
= 35, obj = 49.5`).

| benchmark | with #10052 (master) | after this revert |
| --- | --- | --- |
| Golomb `bug.smt2` (shared symbol) | `(obj (+ 5.0 epsilon))` ❌
infeasible | `(obj 18)` ✅ consistent |
| #5720 (`max r < 1`) | `1 - epsilon` ✅ | `0` ❌ (regression returns) |

## Tradeoff / follow-up

This revert restores soundness on the shared-symbol case but
**reintroduces the #5720 regression** (`max r<1` ⇒ `0`), which is why
**#5720 has been reopened**. A correct fix should preserve the strict
single-objective supremum **without** trusting an unvalidated
shared-symbol hint — e.g. gate the eager commit on `!has_shared` (pure
LP only), or validate the rational part of the hint while keeping the
infinitesimal. The same blind spot affects the alternative `check_bound`
guard proposed in #10051.

Re: #5720

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

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