mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

remove debug asserts

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-06 08:53:12 +02:00
parent 2f63747c7b
commit b0dce5b27d
1 changed files with 0 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/array_model.cpp
View file

@ -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;