mirror of
https://github.com/Z3Prover/z3
synced 2026-08-08 23:11:20 +00:00
c7b3b425e6
The nonlinear bound optimization can cross an unconditional bound such as x² >= 0. Such bounds legitimately have no dependency witness, but crossed-bound conflict construction asserted that a witness must exist.\n\nAllow the null witness to participate as an empty dependency and retain the asserted bound's explanation. This fixes the max_rev regression without falling back to unknown.\n\nThe max_rev regression and the full unit suite pass. Copilot-Session: a8f87ede-b718-4fe9-9839-cc9eaaf9c3a7 |
||
|---|---|---|
| .. | ||
| dd | ||
| grobner | ||
| hilbert | ||
| interval | ||
| lp | ||
| polynomial | ||
| realclosure | ||
| simplex | ||
| subpaving | ||