mirror of
https://github.com/Z3Prover/z3
synced 2026-07-27 17:32:45 +00:00
1d936e2384
When an objective's optimum is an open (strict) bound, the arithmetic
relaxation returns a value carrying a non-zero infinitesimal (e.g.
minimizing a real x subject to x > 0, whose infimum is the unattained 0,
reported as "epsilon"). opt_solver::maximize_objective validates such a
hint with check_bound(), which asserts the objective is >= val via mk_ge
and searches for a model reaching it. mk_ge cannot faithfully encode the
infinitesimal (it drops a negative infinitesimal and turns a positive one
into a strict bound), so this validation always fails spuriously for an
open optimum. Since #10028 (
|
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||