From 8cc75d444e5d4840adba1466ed29fbdef27e6c38 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 19 Mar 2026 13:16:27 -1000 Subject: [PATCH] fix box mode: reset bounds before each objective update_lower_lex updates m_lower for subsequent objectives with saved values from the current model. Reset m_lower[i] and m_upper[i] to their initial values before optimizing each objective so earlier objectives do not contaminate later ones. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/opt/optsmt.cpp | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 73a6f1c02..f3ed1aaf9 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -545,28 +545,20 @@ namespace opt { // m_optsmt_engine is "symba", because symba_opt and geometric_opt // optimize all objectives jointly, violating box mode semantics. // - // Save and restore m_lower/m_upper across iterations because - // geometric_lex's update_lower_lex updates m_lower for all - // subsequent objectives with saved values from the current model, - // which would contaminate later objectives' starting bounds. - vector saved_lower(m_lower); - vector saved_upper(m_upper); m_context.get_base_model(m_best_model); for (unsigned i = 0; i < m_vars.size() && m.inc(); ++i) { - m_lower = saved_lower; - m_upper = saved_upper; + // Reset bounds for objective i so that update_lower_lex + // contamination from earlier objectives does not affect it. + m_lower[i] = inf_eps(rational(-1), inf_rational(0)); + m_upper[i] = inf_eps(rational(1), inf_rational(0)); solver::scoped_push _push(*m_s); is_sat = geometric_lex(i, true, true); if (is_sat == l_undef) return l_undef; if (is_sat == l_false) return l_false; - saved_lower[i] = m_lower[i]; - saved_upper[i] = m_upper[i]; m_models.set(i, m_best_model.get()); } - m_lower = saved_lower; - m_upper = saved_upper; return l_true; }