From fadcac8f6d0f119523e70cd893933466a2342298 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Feb 2018 12:39:08 -0800 Subject: [PATCH] fix #1491 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 2f6bad9e8..1950a199d 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -402,8 +402,8 @@ namespace opt { */ bool context::scoped_lex() { if (m_maxsat_engine == symbol("maxres")) { - for (unsigned i = 0; i < m_objectives.size(); ++i) { - if (m_objectives[i].m_type != O_MAXSMT) return true; + for (auto const& o : m_objectives) { + if (o.m_type != O_MAXSMT) return true; } return false; } @@ -413,14 +413,16 @@ namespace opt { lbool context::execute_lex() { lbool r = l_true; bool sc = scoped_lex(); - IF_VERBOSE(1, verbose_stream() << "(optsmt:lex)\n";); - for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) { - bool is_last = i + 1 == m_objectives.size(); - r = execute(m_objectives[i], i + 1 < m_objectives.size(), sc && !is_last); + IF_VERBOSE(1, verbose_stream() << "(opt :lex)\n";); + unsigned sz = m_objectives.size(); + for (unsigned i = 0; r == l_true && i < sz; ++i) { + objective const& o = m_objectives[i]; + bool is_last = i + 1 == sz; + r = execute(o, i + 1 < sz, sc && !is_last && o.m_type != O_MAXSMT); if (r == l_true && !get_lower_as_num(i).is_finite()) { return r; } - if (r == l_true && i + 1 < m_objectives.size()) { + if (r == l_true && i + 1 < sz) { update_lower(); } }