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

fixing an assert caused by previous change in theory_array_base.cpp

Browse source
This commit is contained in:
Ken McMillan 2014-10-01 18:15:33 -07:00
parent 301cb51bbb
commit c5f17df310
1 changed files with 9 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/smt/theory_array_base.cpp
View file

@ -433,14 +433,16 @@ namespace smt {
enode * n = get_enode(i); enode * n = get_enode(i);
if (ctx.is_relevant(n)) { if (ctx.is_relevant(n)) {
enode * r = n->get_root(); enode * r = n->get_root();
if (!r->is_marked() && is_array_sort(r) && ctx.is_shared(r)) { if (!r->is_marked()){
TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";); if(is_array_sort(r) && ctx.is_shared(r)) {
theory_var r_th_var = r->get_th_var(get_id()); TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";);
SASSERT(r_th_var != null_theory_var); theory_var r_th_var = r->get_th_var(get_id());
result.push_back(r_th_var); SASSERT(r_th_var != null_theory_var);
result.push_back(r_th_var);
}
r->set_mark();
to_unmark.push_back(r);
} }
r->set_mark();
to_unmark.push_back(r);
} }
} }
unmark_enodes(to_unmark.size(), to_unmark.c_ptr()); unmark_enodes(to_unmark.size(), to_unmark.c_ptr());