mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

fix #3740

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-04 11:31:29 -07:00
parent df1c6c8a21
commit c26d3f5437
1 changed files with 5 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/smt/theory_arith_nl.h
View file

@ -1002,22 +1002,14 @@ bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
*/ */
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::propagate_linear_monomials() { bool theory_arith<Ext>::propagate_linear_monomials() {
if (!reflection_enabled())
return false;
TRACE("non_linear", tout << "propagating linear monomials...\n";); TRACE("non_linear", tout << "propagating linear monomials...\n";);
bool p = false; bool p = false;
// CMW: m_nl_monomials is sometimes modified while executing // CMW: m_nl_monomials can grow during this loop, so
// propagate_linear_monomial(...), invalidating the iterator `it'. // don't use iterators.
// (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<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++) { for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
theory_var v = m_nl_monomials[i]; if (propagate_linear_monomial(m_nl_monomials[i]))
if (propagate_linear_monomial(v))
p = true; p = true;
} }
CTRACE("non_linear", p, display(tout);); CTRACE("non_linear", p, display(tout););