diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index 2e8a0603d..372e05c75 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -175,18 +175,14 @@ namespace array {
         ptr_buffer<expr> sel1_args, sel2_args;
         unsigned num_args = select->get_num_args();
 
-        if (select->get_arg(0) != store && expr2enode(select->get_arg(0))->get_root() == expr2enode(store)->get_root()) 
-            return false;
         bool has_diff = false;
         for (unsigned i = 1; i < num_args; i++) 
             has_diff |= expr2enode(select->get_arg(i))->get_root() != expr2enode(store->get_arg(i))->get_root();
         if (!has_diff)
             return false;
 
-
         sel1_args.push_back(store);
-        sel2_args.push_back(store->get_arg(0));
-        
+        sel2_args.push_back(store->get_arg(0));        
         
         for (unsigned i = 1; i < num_args; i++) {
             sel1_args.push_back(select->get_arg(i));
diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp
index b56f4efb1..47ccfcc62 100644
--- a/src/sat/smt/array_solver.cpp
+++ b/src/sat/smt/array_solver.cpp
@@ -228,11 +228,8 @@ namespace array {
         
         auto& d = get_var_data(v);
 
-        for (euf::enode* lambda : d.m_lambdas) {
-            expr* e = lambda->get_expr();
-            if (a.is_const(e) || a.is_map(e)) 
-                propagate_select_axioms(d, lambda);
-        }
+        for (euf::enode* lambda : d.m_lambdas) 
+            propagate_select_axioms(d, lambda);        
         
         for (euf::enode* lambda : d.m_parent_lambdas)
             propagate_select_axioms(d, lambda);