mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 12:11:23 +00:00
Code Activity

Fixed iterator invalidation bug in theory_arith_nl.

Browse source 
Indirectly relates to #740
This commit is contained in:
Christoph M. Wintersteiger 2016-10-18 17:17:19 +01:00
parent 9fef51553c
commit 4546915238
1 changed files with 13 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/smt/theory_arith_nl.h
View file

@ -965,10 +965,19 @@ namespace smt {
bool theory_arith<Ext>::propagate_linear_monomials() { bool theory_arith<Ext>::propagate_linear_monomials() {
TRACE("non_linear", tout << "propagating linear monomials...\n";); TRACE("non_linear", tout << "propagating linear monomials...\n";);
bool p = false; bool p = false;
svector<theory_var>::const_iterator it = m_nl_monomials.begin(); // CMW: m_nl_monomials is sometimes modified while executing
svector<theory_var>::const_iterator end = m_nl_monomials.end(); // propagate_linear_monomial(...), invalidating the iterator `it'.
for (; it != end; ++it) { // (Via the relevancy propagation that internalizes a new axiom
theory_var v = *it; // in mk_div_axiom and possibly others.) I'm replacing the iterator
// with an index `i'.
// Was previously:
// svector<theory_var>::const_iterator it = m_nl_monomials.begin();
// svector<theory_var>::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)) if (propagate_linear_monomial(v))
p = true; p = true;
} }