diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index ecd5f8190..015c4a0c1 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -532,19 +532,22 @@ namespace array {
         if (!get_config().m_array_delay_exp_axiom)
             return false;
         unsigned num_vars = get_num_vars();
+        bool change = false;
         for (unsigned v = 0; v < num_vars; v++) {
             propagate_parent_select_axioms(v);
             auto& d = get_var_data(v);
             if (!d.m_prop_upward)
                 continue;
             euf::enode* n = var2enode(v);
+            if (add_as_array_eqs(n))
+                change = true;
             bool has_default = false;
             for (euf::enode* p : euf::enode_parents(n))
                 has_default |= a.is_default(p->get_expr());
             if (has_default)
                 propagate_parent_default(v);      
         }
-        bool change = false;
+
         unsigned sz = m_axiom_trail.size();
         m_delay_qhead = 0;
         
@@ -557,6 +560,27 @@ namespace array {
         return change;
     }
 
+    bool solver::add_as_array_eqs(euf::enode* n) {
+        func_decl* f = nullptr;
+        bool change = false;
+        if (!a.is_as_array(n->get_expr(), f))
+            return false;
+        for (unsigned i = 0; i < ctx.get_egraph().enodes_of(f).size(); ++i) {
+            euf::enode* p = ctx.get_egraph().enodes_of(f)[i];
+            expr_ref_vector select(m);
+            select.push_back(n->get_expr());
+            for (expr* arg : *to_app(p->get_expr()))
+                select.push_back(arg);
+            expr_ref _e(a.mk_select(select.size(), select.data()), m);
+            euf::enode* e = e_internalize(_e);
+            if (e->get_root() != p->get_root()) {
+                add_unit(eq_internalize(_e, p->get_expr()));
+                change = true;
+            }
+        }
+        return change;
+    }
+
     bool solver::add_interface_equalities() {
         sbuffer<theory_var> roots;
         collect_defaults();
diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h
index 133c17044..0c0fc82d6 100644
--- a/src/sat/smt/array_solver.h
+++ b/src/sat/smt/array_solver.h
@@ -184,6 +184,7 @@ namespace array {
         bool assert_default_store_axiom(app* store);
         bool assert_congruent_axiom(expr* e1, expr* e2);
         bool add_delayed_axioms();
+        bool add_as_array_eqs(euf::enode* n);
         
         bool has_unitary_domain(app* array_term);
         bool has_large_domain(expr* array_term);
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 56e3b93b6..e10225c9c 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -869,7 +869,7 @@ namespace euf {
             if (b != sat::null_bool_var) {
                 m_bool_var2expr.setx(b, n->get_expr(), nullptr);
                 SASSERT(r->m.is_bool(n->get_sort()));
-                IF_VERBOSE(1, verbose_stream() << "set bool_var " << r->bpp(n) << "\n");
+                IF_VERBOSE(11, verbose_stream() << "set bool_var " << r->bpp(n) << "\n");
             }
         }
         for (auto* s_orig : m_id2solver) {