diff --git a/src/ast/simplifiers/bound_manager.cpp b/src/ast/simplifiers/bound_manager.cpp index cb9df3e67..de26699b9 100644 --- a/src/ast/simplifiers/bound_manager.cpp +++ b/src/ast/simplifiers/bound_manager.cpp @@ -155,7 +155,8 @@ void bound_manager::operator()(expr * f, expr_dependency * d, proof* p) { void bound_manager::insert_upper(expr * v, bool strict, numeral const & n, expr_dependency * d) { limit old; if (m_uppers.find(v, old)) { - if (n < old.first || (n == old.first && strict && !old.second)) { + auto [old_bound, old_strict] = old; + if (n < old_bound || (n == old_bound && strict && !old_strict)) { // improved bound m_uppers.insert(v, limit(n, strict)); if (d) @@ -175,7 +176,8 @@ void bound_manager::insert_upper(expr * v, bool strict, numeral const & n, expr_ void bound_manager::insert_lower(expr * v, bool strict, numeral const & n, expr_dependency * d) { limit old; if (m_lowers.find(v, old)) { - if (n > old.first || (n == old.first && strict && !old.second)) { + auto [old_bound, old_strict] = old; + if (n > old_bound || (n == old_bound && strict && !old_strict)) { // improved bound m_lowers.insert(v, limit(n, strict)); if (d)