remove debug asserts

Z3Prover · Apr 6, 2022 · b0dce5b · b0dce5b
1 parent 2f63747
commit b0dce5b
Showing 1 changed file with 0 additions and 6 deletions.
diff --git 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;