mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-30 09:58:46 +00:00
Code Activity

Fixed potential problems with invalidated iterators.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-19 12:00:34 +01:00
parent 3aa7eab3e2
commit 11997afb5d
1 changed files with 6 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/smt/theory_arith_nl.h
View file

@ -589,10 +589,8 @@ namespace smt {
m_dep_manager.reset(); m_dep_manager.reset();
bool propagated = false; bool propagated = false;
context & ctx = get_context(); context & ctx = get_context();
svector<theory_var>::const_iterator it = m_nl_monomials.begin(); for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
svector<theory_var>::const_iterator end = m_nl_monomials.end(); theory_var v = m_nl_monomials.size();
for (; it != end; ++it) {
theory_var v = *it;
expr * m = var2expr(v); expr * m = var2expr(v);
if (!ctx.is_relevant(m)) if (!ctx.is_relevant(m))
continue; continue;
@ -706,10 +704,8 @@ namespace smt {
bool bounded = false; bool bounded = false;
unsigned n = 0; unsigned n = 0;
numeral range; numeral range;
svector<theory_var>::const_iterator it = m_nl_monomials.begin(); for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
svector<theory_var>::const_iterator end = m_nl_monomials.end(); theory_var v = m_nl_monomials.size();
for (; it != end; ++it) {
theory_var v = *it;
if (is_real(v)) if (is_real(v))
continue; continue;
bool computed_epsilon = false; bool computed_epsilon = false;
@ -2340,10 +2336,8 @@ namespace smt {
bool theory_arith<Ext>::max_min_nl_vars() { bool theory_arith<Ext>::max_min_nl_vars() {
var_set already_found; var_set already_found;
svector<theory_var> vars; svector<theory_var> vars;
svector<theory_var>::const_iterator it = m_nl_monomials.begin(); for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
svector<theory_var>::const_iterator end = m_nl_monomials.end(); theory_var v = m_nl_monomials.size();
for (; it != end; ++it) {
theory_var v = *it;
mark_var(v, vars, already_found); mark_var(v, vars, already_found);
expr * n = var2expr(v); expr * n = var2expr(v);
SASSERT(is_pure_monomial(n)); SASSERT(is_pure_monomial(n));