From b0dce5b27d063e954ef0ea506c4600a5ddcb6d25 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 6 Apr 2022 08:53:12 +0200
Subject: [PATCH] remove debug asserts

---
 src/sat/smt/array_model.cpp | 6 ------
 1 file changed, 6 deletions(-)

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;