mirror of
https://github.com/Z3Prover/z3
synced 2026-07-27 17:32:45 +00:00
475af3e5c5
The nonlinear optimization path (max_with_nl) returned the linear-relaxation optimum lp_val including its infinitesimal. That infinitesimal is an artifact of the strict bounds introduced by the linearization, not a genuine strict optimum of the nonlinear problem. Threading it into opt_solver::mk_ge made theory_lra assert a delta-rational lower bound (r, -1) that coincides with the column's existing strict upper bound (r, -1), fixing the objective column at a delta value the LP core never snapped, tripping the non_basic_columns_are_set_correctly assertion in a debug build (unit tests max_reg / max_rev). Project the infinitesimal away in both NLA branches (FC_DONE and FC_CONTINUE); the rational part remains a sound bound for check_bound to validate. The genuinely-strict, NLA-free path (e.g. pure LP suprema and shared-symbol/EUF objectives) is unaffected, so faithful validation of strict optima is preserved. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||