From 8e2f09b517ae84b2f70d0e4af74df95c8ecf38b2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 25 Apr 2022 17:17:59 +0100
Subject: [PATCH] #5778 - ensure arrays used inside of extensionality function
 are treated as shared

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/array_axioms.cpp  |  6 +++++-
 src/smt/theory_array_base.cpp | 36 ++++-------------------------------
 2 files changed, 9 insertions(+), 33 deletions(-)

diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index c0f0e9a72..84b12cf7d 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -629,12 +629,14 @@ namespace array {
             euf::enode * n = var2enode(i);            
             if (!is_array(n)) 
                 continue;
+            CTRACE("array", !ctx.is_relevant(n), tout << "not relevant: " << ctx.bpp(n) << "\n");
             if (!ctx.is_relevant(n))
                 continue;
             euf::enode * r = n->get_root();
             if (r->is_marked1()) 
                 continue;            
-            // arrays used as indices in other arrays have to be treated as shared issue #3532, #3529            
+            // arrays used as indices in other arrays have to be treated as shared issue #3532, #3529
+            CTRACE("array", !ctx.is_shared(r) && !is_shared_arg(r), tout << "not shared: " << ctx.bpp(r) << "\n");
             if (ctx.is_shared(r) || is_shared_arg(r)) 
                 roots.push_back(r->get_th_var(get_id()));           
             r->mark1();
@@ -655,6 +657,8 @@ namespace array {
                         return true;
             if (a.is_const(e))
                 return true;
+            if (a.is_ext(e))
+                return true;
         }
             
         return false;
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index 9bc0b733f..33944c96c 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -473,39 +473,12 @@ namespace smt {
         return false;
     }
 
-#if 0
-    void theory_array_base::collect_shared_vars(sbuffer<theory_var> & result) {
-        TRACE("array_shared", tout << "collecting shared vars...\n";);
-        ptr_buffer<enode> to_unmark;
-        unsigned num_vars = get_num_vars();
-        for (unsigned i = 0; i < num_vars; i++) {
-            enode * n = get_enode(i);
-            if (ctx.is_relevant(n) && ctx.is_shared(n)) {
-                enode * r = n->get_root();
-                if (!r->is_marked() && is_array_sort(r)) {
-                    TRACE("array_shared", tout << "new shared var: #" << r->get_expr_id() << "\n";);
-                    r->set_mark();
-                    to_unmark.push_back(r);
-                    theory_var r_th_var = r->get_var(get_id());
-                    SASSERT(r_th_var != null_theory_var);
-                    result.push_back(r_th_var);
-                }
-            }
-        }
-        unmark_enodes(to_unmark.size(), to_unmark.c_ptr());
-    }
-#else
-
     bool theory_array_base::is_select_arg(enode* r) {
-        for (enode* n : r->get_parents()) {
-            if (is_select(n)) {
-                for (unsigned i = 1; i < n->get_num_args(); ++i) {
-                    if (r == n->get_arg(i)->get_root()) {
+        for (enode* n : r->get_parents()) 
+            if (is_select(n)) 
+                for (unsigned i = 1; i < n->get_num_args(); ++i) 
+                    if (r == n->get_arg(i)->get_root()) 
                         return true;
-                    }
-                }
-            }
-        }
         return false;
     }
 
@@ -536,7 +509,6 @@ namespace smt {
         TRACE("array", tout << "collecting shared vars...\n" << unsigned_vector(result.size(), (unsigned*)result.data())  << "\n";);
         unmark_enodes(to_unmark.size(), to_unmark.data());
     }
-#endif
 
     /**
        \brief Create interface variables for shared array variables.