diff --git a/src/model/array_factory.cpp b/src/model/array_factory.cpp
index 40476e6d3..8350839b7 100644
--- a/src/model/array_factory.cpp
+++ b/src/model/array_factory.cpp
@@ -72,6 +72,7 @@ expr * array_factory::get_some_value(sort * s) {
 }
 
 bool array_factory::mk_two_diff_values_for(sort * s) {
+    TRACE("array_factory", tout << mk_pp(s, m_manager) << "\n";);
     DEBUG_CODE({
         value_set * set = 0;
         SASSERT(!m_sort2value_set.find(s, set) || set->size() <= 1);
@@ -112,6 +113,7 @@ bool array_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
     v1 = *it;
     ++it;
     v2 = *it;
+    TRACE("array_factory", tout << v1 << " " << v2 << "\n";);
     return true;    
 }
 
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index afe94c3c7..2d03336e5 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -509,26 +509,42 @@ 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();
+        }
+        while (r != n);
+        return false;
+    }
+
     void theory_array_base::collect_shared_vars(sbuffer<theory_var> & result) {
-        TRACE("array_shared", tout << "collecting shared vars...\n";);
+        TRACE("array", tout << "collecting shared vars...\n";);
         context & ctx = get_context();
         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)) {
+            enode * n = get_enode(i);
+            if (!ctx.is_relevant(n) || !is_array_sort(n)) {
+                continue;
+            }
             enode * r = n->get_root();
-        if (!r->is_marked()){
-            if(is_array_sort(r) && ctx.is_shared(r)) {
-              TRACE("array_shared", 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);
-              result.push_back(r_th_var);
+            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)) {
+                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);
+                result.push_back(r_th_var);
             }
             r->set_mark();
-            to_unmark.push_back(r);
-        }
-            }
+            to_unmark.push_back(r);            
         }
         unmark_enodes(to_unmark.size(), to_unmark.c_ptr());
     }
diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h
index ec47b9608..7e521750f 100644
--- a/src/smt/theory_array_base.h
+++ b/src/smt/theory_array_base.h
@@ -60,6 +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);
 
 
         app * mk_select(unsigned num_args, expr * const * args);