From c5f17df310405b2f7718f1eaa93242cfa25e54de Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 1 Oct 2014 18:15:33 -0700 Subject: [PATCH] fixing an assert caused by previous change in theory_array_base.cpp --- src/smt/theory_array_base.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) 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());