mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 09:22:41 +00:00
Code Activity

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

Browse source 
This reverts commit eccdffa781.
This commit is contained in:
Lev Nachmanson 2026-07-06 12:51:14 -07:00
parent f37b435923
commit a0ecf07672
1 changed files with 0 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/opt/opt_solver.cpp
View file

@ -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.