From a0ecf07672384f0e750d9883f31518950c61057f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 6 Jul 2026 12:51:14 -0700 Subject: [PATCH] Revert "[snapshot-regression-fix] opt: preserve strict supremum/infimum optima with infinitesimal component (#10052)" This reverts commit eccdffa78168015d5d21564c310c66ca2db0dd8e. --- 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.