From 5df80705aaf5eeeb8c64b5860c82d22bf535b194 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 15 Mar 2026 07:02:13 -1000 Subject: [PATCH] Fix inconsistent optimization with scaled objectives (#8998) When the LP optimizer returns the same blocker expression in successive iterations of geometric_lex (e.g., due to nonlinear constraints like mod/to_int preventing the LP from exploring the full feasible region), the loop now falls back to using the model-based lower bound to push harder instead of breaking immediately. This fixes the case where minimize(3*a) incorrectly returned -162 while minimize(a) correctly returned -infinity with the same constraints. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/opt/optsmt.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index cc4b5a3d4..8a321d28a 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -253,7 +253,14 @@ namespace opt { } last_objective = obj; if (bound == last_bound) { - break; + // LP didn't produce a new blocker. If the model-based lower bound + // is strictly better than what the LP found, use it to push the LP + // further. This handles cases where nonlinear constraints, mod, + // to_int, prevent the LP from seeing the full feasible region. + if (m_lower[obj_index].is_finite() && m_lower[obj_index] > obj) + bound = m_s->mk_ge(obj_index, m_lower[obj_index]); + if (bound == last_bound) + break; } m_s->assert_expr(bound); last_bound = bound;