From 45469152387b8f89ba386c770bd8a7028fc152af Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 18 Oct 2016 17:17:19 +0100 Subject: [PATCH] Fixed iterator invalidation bug in theory_arith_nl. Indirectly relates to #740 --- src/smt/theory_arith_nl.h | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index c3ae8c99b..04b974d6e 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -965,10 +965,19 @@ namespace smt { bool theory_arith::propagate_linear_monomials() { TRACE("non_linear", tout << "propagating linear monomials...\n";); bool p = false; - svector::const_iterator it = m_nl_monomials.begin(); - svector::const_iterator end = m_nl_monomials.end(); - for (; it != end; ++it) { - theory_var v = *it; + // CMW: m_nl_monomials is sometimes modified while executing + // propagate_linear_monomial(...), invalidating the iterator `it'. + // (Via the relevancy propagation that internalizes a new axiom + // in mk_div_axiom and possibly others.) I'm replacing the iterator + // with an index `i'. + + // Was previously: + // 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[i]; if (propagate_linear_monomial(v)) p = true; }