diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp index b295ce282..c437629f5 100644 --- a/src/sat/smt/array_model.cpp +++ b/src/sat/smt/array_model.cpp @@ -42,7 +42,6 @@ namespace array { dep.add(n, p); for (euf::enode* p : *get_select_set(n)) { - SASSERT(n != p); dep.add(n, p); for (unsigned i = 1; i < p->num_args(); ++i) dep.add(n, p->get_arg(i)); @@ -51,15 +50,10 @@ namespace array { for (euf::enode* k : euf::enode_class(n)) if (a.is_const(k->get_expr())) dep.add(n, k->get_arg(0)); - for (euf::enode* k : euf::enode_class(n)) - if (a.is_const(k->get_expr())) { - SASSERT(n != k->get_arg(0)); - } theory_var v = get_th_var(n); euf::enode* d = get_default(v); if (d) dep.add(n, d); - SASSERT(n != d); if (!dep.deps().contains(n)) dep.insert(n, nullptr); return true;