mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

fix null parent bug by making a copy of n_eq_enode->m_parents in simplify_parent

Browse source
This commit is contained in:
Murphy Berzish 2016-05-19 16:57:01 -04:00
parent c8522c5b78
commit 2f494a9611
1 changed files with 11 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/smt/theory_str.cpp
View file

@ -838,9 +838,18 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) {
app * n_eqNode = n_eq_enode->get_owner();
TRACE("t_str_detail", tout << "considering all parents of " << mk_ismt2_pp(n_eqNode, m) << std::endl
<< "associated n_eq_enode has " << n_eq_enode->get_num_parents() << " parents" << std::endl;);
for (enode_vector::iterator parent_it = n_eq_enode->begin_parents(); parent_it != n_eq_enode->end_parents(); parent_it++) {
// the goal of this next bit is to avoid dereferencing a bogus e_parent in the following loop.
// what I image is causing this bug is that, for example, we examine some parent, we add an axiom that involves it,
// and the parent_it iterator becomes invalidated, because we indirectly modified the container that we're iterating over.
enode_vector current_parents;
for (enode_vector::const_iterator parent_it = n_eq_enode->begin_parents(); parent_it != n_eq_enode->end_parents(); parent_it++) {
current_parents.insert(*parent_it);
}
for (enode_vector::iterator parent_it = current_parents.begin(); parent_it != current_parents.end(); ++parent_it) {
enode * e_parent = *parent_it;
// TODO deeper bug hiding here
SASSERT(e_parent != NULL);
app * a_parent = e_parent->get_owner();