From c002c77e5afb4a813f5c6d5c9f7b9d0e33c359b7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 7 Mar 2025 11:52:49 -0800 Subject: [PATCH] fix #7569 Signed-off-by: Nikolaj Bjorner --- src/opt/optsmt.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 1cfc72185..d92bc0b06 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -133,9 +133,11 @@ namespace opt { // only try to improve delta_index. bound = m_s->mk_ge(delta_index, m_lower[delta_index] + inf_eps(delta_per_step)); } - TRACE("opt", tout << "index: " << delta_index << " delta: " << delta_per_step << " : " << bound << "\n";); + TRACE("opt", tout << mk_pp(m_objs.get(delta_index), m) << " index: " << delta_index << " delta: " << delta_per_step << " : " << bound << "\n";); if (bound == last_bound) { is_sat = l_false; + if (!m_lower[delta_index].is_finite() && !m_upper[delta_index].is_finite()) + m_lower[delta_index] = m_upper[delta_index]; } else { m_s->assert_expr(bound); @@ -155,7 +157,8 @@ namespace opt { else if (is_sat == l_false) { // we are done with this delta_index. m_upper[delta_index] = m_lower[delta_index]; - if (num_scopes > 0) m_s->pop(num_scopes); + if (num_scopes > 0) + m_s->pop(num_scopes); num_scopes = 0; last_bound = nullptr; bool all_tight = true;