diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 6325a2a99..b2c17b4e0 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -433,14 +433,16 @@ namespace smt { enode * n = get_enode(i); if (ctx.is_relevant(n)) { enode * r = n->get_root(); - if (!r->is_marked() && is_array_sort(r) && ctx.is_shared(r)) { - TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";); - theory_var r_th_var = r->get_th_var(get_id()); - SASSERT(r_th_var != null_theory_var); - result.push_back(r_th_var); + if (!r->is_marked()){ + if(is_array_sort(r) && ctx.is_shared(r)) { + TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";); + theory_var r_th_var = r->get_th_var(get_id()); + 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());