diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 8b37fb802..cefe8bbbb 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -1749,7 +1749,9 @@ class QuantifierRef(BoolRef):
         return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
 
     def sort(self):
-        """Return the Boolean sort."""
+        """Return the Boolean sort or sort of Lambda."""
+        if self.is_lambda():
+            return _sort(self.ctx, self.as_ast())
         return BoolSort(self.ctx)
 
     def is_forall(self):
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index d872997c4..03cd3e1b2 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -339,6 +339,7 @@ namespace smt {
         SASSERT(v != null_theory_var);
         v = find(v);
         var_data* d = m_var_data[v];
+        TRACE("array", tout << "v" << v << "\n";);
         for (enode * store : d->m_stores) {
             SASSERT(is_store(store));
             instantiate_default_store_axiom(store);
@@ -383,13 +384,21 @@ namespace smt {
     void theory_array_full::relevant_eh(app* n) {
         TRACE("array", tout << mk_pp(n, get_manager()) << "\n";);
         theory_array::relevant_eh(n);
-        if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n)) {
+        if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n) && !is_store(n)) {
             return;
         }
         context & ctx = get_context();
         enode* node = ctx.get_enode(n);
-
-        if (is_select(n)) {
+        if (is_store(n)) {
+            enode * arg = ctx.get_enode(n->get_arg(0));
+            if (is_const(arg)) {
+                TRACE("array", tout << expr_ref(arg->get_owner(), get_manager()) << " " << is_const(arg) << "\n";);
+                theory_var v = arg->get_th_var(get_id());
+                set_prop_upward(v);
+                add_parent_default(v);
+            }
+        }
+        else if (is_select(n)) {
             enode * arg = ctx.get_enode(n->get_arg(0));
             theory_var v = arg->get_th_var(get_id());
             SASSERT(v != null_theory_var);