From 01e47bfe263f8eabf2daa2da35c7b248ee33fff9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 15 Jun 2024 02:29:32 -0700 Subject: [PATCH] fix #7245 --- src/opt/opt_solver.cpp | 14 ++++---------- src/smt/smt_kernel.h | 2 +- 2 files changed, 5 insertions(+), 11 deletions(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 955025fd9..aff1301e0 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -259,8 +259,9 @@ namespace opt { if (!m_models[i]) m_models.set(i, m_last_model.get()); - if (val > m_objective_values[i]) - m_objective_values[i] = val; + if (val > m_objective_values[i]) { + m_objective_values[i] = val; + } if (!m_last_model) return true; @@ -284,14 +285,7 @@ namespace opt { // auto check_bound = [&]() { SASSERT(has_shared); - bool ok = bound_value(i, val); - if (l_true != m_context.check(0, nullptr)) - return false; - m_context.get_model(m_last_model); - if (!m_last_model) - return false; - update_objective(); - return ok; + return bound_value(i, val) && l_true == m_context.check(0, nullptr); }; if (!val.is_finite()) { diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index dacbb525e..eec74f8b1 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -258,7 +258,7 @@ namespace smt { expr_ref_vector get_trail(unsigned max_level); /** - \brief (For debubbing purposes) Prints the state of the kernel + \brief (For debugging purposes) Prints the state of the kernel */ std::ostream& display(std::ostream & out) const;