From f74079de0196193d65a740fb8e9ffb089e5f5c4e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 29 Mar 2020 12:48:14 -0700
Subject: [PATCH] fix #3529

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_array_base.cpp | 25 ++++++++++++++-----------
 src/smt/theory_array_base.h   |  3 +--
 2 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index 2d03336e5..34539d5fa 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -509,14 +509,17 @@ namespace smt {
         unmark_enodes(to_unmark.size(), to_unmark.c_ptr());
     }
 #else
-    bool theory_array_base::has_array_ext(enode* n) {
-        enode* r = n;
-        do {
-            if (is_array_ext(n->get_owner()))
-                return true;
-            n = n->get_next();
+
+    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()) {
+                        return true;
+                    }
+                }
+            }
         }
-        while (r != n);
         return false;
     }
 
@@ -534,10 +537,10 @@ namespace smt {
             if (r->is_marked()) {
                 continue;
             }
-            // array extensionality terms may be produced in nested arrays.
-            // they have to be treated as shared to resolve equalities.
-            // issue #3532
-            if (ctx.is_shared(r) || has_array_ext(r)) {
+            // arrays used as indices in other arrays have to be treated as shared.
+            // issue #3532, #3529
+            // 
+            if (ctx.is_shared(r) || is_select_arg(r)) {
                 TRACE("array", tout << "new shared var: #" << r->get_owner_id() << "\n";);
                 theory_var r_th_var = r->get_th_var(get_id());
                 SASSERT(r_th_var != null_theory_var);
diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h
index 7e521750f..6da19b95c 100644
--- a/src/smt/theory_array_base.h
+++ b/src/smt/theory_array_base.h
@@ -60,8 +60,7 @@ namespace smt {
         bool is_array_sort(enode const* n) const { return is_array_sort(n->get_owner()); }
         bool is_set_has_size(enode const* n) const { return is_set_has_size(n->get_owner()); }
         bool is_set_carde(enode const* n) const { return is_set_card(n->get_owner()); }
-        bool has_array_ext(enode* n);
-
+        bool is_select_arg(enode* r);
 
         app * mk_select(unsigned num_args, expr * const * args);
         app * mk_store(unsigned num_args, expr * const * args);