diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp
index e45d59bd9..5e285112d 100644
--- a/src/sat/smt/array_internalize.cpp
+++ b/src/sat/smt/array_internalize.cpp
@@ -99,7 +99,8 @@ namespace array {
 
     void solver::internalize_eh(euf::enode* n) {
         switch (n->get_decl()->get_decl_kind()) {
-        case OP_STORE:
+        case OP_STORE:          
+            ctx.push_vec(get_var_data(find(n)).m_lambdas, n);
             push_axiom(store_axiom(n));
             break;
         case OP_SELECT: