From eccdffa78168015d5d21564c310c66ca2db0dd8e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sun, 5 Jul 2026 09:15:19 -0700 Subject: [PATCH] [snapshot-regression-fix] opt: preserve strict supremum/infimum optima with infinitesimal component (#10052) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Fixes a Z3 optimization regression where maximizing a real objective under a **strict** inequality returned a plain feasible model value instead of the strict supremum. Originating discussion: https://github.com/Z3Prover/bench/discussions/3053 Benchmark: `iss-5720/bug-1.smt2` (in `Z3Prover/bench`) ```smt2 (declare-const r Real) (assert (< r 1)) (maximize r) (check-sat) (get-objectives) ``` The optimum of `r` subject to `r < 1` is the strict supremum `1 - epsilon`, which the recorded oracle expects. Current z3 instead reports the feasible point `0`. ## Divergence ```diff --- bug-1.expected.out (expected) +++ produced (current z3) @@ -1,4 +1,4 @@ sat (objectives - (r (+ 1.0 (* (- 1.0) epsilon))) + (r 0) ) ``` ## Root cause Regression from commit `fdc32d0e6` ("Fix inconsistent optimization result with unvalidated LP bound", #10028). That change stopped committing the LP optimization hint `val` to `m_objective_values` up front in `opt_solver::maximize_objective`, deferring the commit until `check_bound()` validates it. Its goal is to reject **plain-rational** over-estimates produced when the objective shares symbols with other theories (e.g. the auxiliary uninterpreted function used to encode large `distinct` constraints); those over-estimates have a **zero** infinitesimal. For a strict real supremum/infimum the hint has a **non-zero** infinitesimal (here `val = 1 - epsilon`). `check_bound()` can never validate it, because `opt_solver::mk_ge` drops the negative infinitesimal (mathematically, `r >= 1 - epsilon` is equivalent over the reals to `r >= 1`), turning the validation bound into the unsatisfiable `r >= 1` given `r < 1`. Validation therefore fails, `maximize_objective` returns `false`, and `m_objective_values` is left holding the strictly smaller current **model** value (`0`), which `optsmt::geometric_lex` then reports as the optimum. ## Fix `src/opt/opt_solver.cpp`, `maximize_objective`: restore the pre-#10028 eager commit of the hint, **scoped to finite values with a non-zero infinitesimal**: ```cpp if (val.is_finite() && !val.get_infinitesimal().is_zero() && val > m_objective_values[i]) m_objective_values[i] = val; ``` A finite value with a non-zero infinitesimal is a strict optimum that no concrete model can attain and that `check_bound()` cannot validate, so the arithmetic hint is authoritative and must be preserved. Plain-rational (zero-infinitesimal) values — including **all integer objectives** and the `#10028` shared-symbol over-estimates — do not enter this branch and continue through the deferred-commit validation path unchanged, so `#10028` is structurally preserved. The change does not alter control flow or the return value, so the lex/box drivers behave as before. ## Validation Built the patched `./z3` checkout (`./configure && make -C build -j$(nproc)`) and re-ran the benchmark with the same options the snapshot capture uses: ``` $ ./build/z3 -T:20 inputs/issues/iss-5720/bug-1.smt2 sat (objectives (r (+ 1.0 (* (- 1.0) epsilon))) ) ``` This is a **byte-exact match** with the recorded `bug-1.expected.out` oracle. Additional before/after checks on the rebuilt binary (baseline = current nightly, unpatched): | case | baseline | patched | | --- | --- | --- | | single strict-real max `r<1` | `r=0` ❌ | `r=1-eps` ✅ (target) | | single strict-real min `r>1` | `r=0` ❌ | `r=1+eps` ✅ | | non-strict real max `r<=1` | `r=1` ✅ | `r=1` ✅ | | integer max `x<10` | `x=9` ✅ | `x=9` ✅ | | bounded strict `2= 1-epsilon` (which `mk_ge` reduces to `r >= 1`) contradicts `r < 1`. This corner is already mishandled by the current nightly (it returns `r=0`) and is not what discussion #3053 reports; this patch does not attempt to redefine that semantics. It changes only how that corner manifests, while fixing the reported single-objective divergence and all well-defined cases above. Draft for human review. > Generated by [Fix a Z3 snapshot-regression divergence](https://github.com/Z3Prover/bench/actions/runs/28733642068) · 691.9 AIC · ⌖ 44.2 AIC · ⊞ 8.9K · [◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/opt/opt_solver.cpp | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index eb8b4dd6cb..88e81184fd 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -342,6 +342,24 @@ 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.