From 11997afb5d1c0dd816bcd43dfa8298031e4ee743 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 19 Oct 2016 12:00:34 +0100 Subject: [PATCH] Fixed potential problems with invalidated iterators. --- src/smt/theory_arith_nl.h | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 04b974d6e..df9a71aaa 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -589,10 +589,8 @@ namespace smt { m_dep_manager.reset(); bool propagated = false; context & ctx = get_context(); - svector::const_iterator it = m_nl_monomials.begin(); - svector::const_iterator end = m_nl_monomials.end(); - for (; it != end; ++it) { - theory_var v = *it; + for (unsigned i = 0; i < m_nl_monomials.size(); i++) { + theory_var v = m_nl_monomials.size(); expr * m = var2expr(v); if (!ctx.is_relevant(m)) continue; @@ -706,10 +704,8 @@ namespace smt { bool bounded = false; unsigned n = 0; numeral range; - svector::const_iterator it = m_nl_monomials.begin(); - svector::const_iterator end = m_nl_monomials.end(); - for (; it != end; ++it) { - theory_var v = *it; + for (unsigned i = 0; i < m_nl_monomials.size(); i++) { + theory_var v = m_nl_monomials.size(); if (is_real(v)) continue; bool computed_epsilon = false; @@ -2340,10 +2336,8 @@ namespace smt { bool theory_arith::max_min_nl_vars() { var_set already_found; svector vars; - svector::const_iterator it = m_nl_monomials.begin(); - svector::const_iterator end = m_nl_monomials.end(); - for (; it != end; ++it) { - theory_var v = *it; + for (unsigned i = 0; i < m_nl_monomials.size(); i++) { + theory_var v = m_nl_monomials.size(); mark_var(v, vars, already_found); expr * n = var2expr(v); SASSERT(is_pure_monomial(n));