diff --git a/src/smt/theory_array.h b/src/smt/theory_array.h
index 67ae8a8a5..46922e049 100644
--- a/src/smt/theory_array.h
+++ b/src/smt/theory_array.h
@@ -28,7 +28,7 @@ namespace smt {
         unsigned   m_num_axiom1, m_num_axiom2a, m_num_axiom2b, m_num_extensionality, m_num_eq_splits;
         unsigned   m_num_map_axiom, m_num_default_map_axiom;
         unsigned   m_num_select_const_axiom, m_num_default_store_axiom, m_num_default_const_axiom, m_num_default_as_array_axiom;
-        unsigned   m_num_select_as_array_axiom;
+        unsigned   m_num_select_as_array_axiom, m_num_default_lambda_axiom;
         void reset() { memset(this, 0, sizeof(theory_array_stats)); }
         theory_array_stats() { reset(); }
     };
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index 6e7403737..1dd607f59 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -181,6 +181,17 @@ namespace smt {
         }
     }
 
+    void theory_array_full::add_lambda(theory_var v, enode* lam) {
+        var_data * d  = m_var_data[v];
+        unsigned lambda_equiv_class_size = get_lambda_equiv_size(v, d);
+        if (m_params.m_array_always_prop_upward || lambda_equiv_class_size >= 1) 
+            set_prop_upward(v, d);
+        ptr_vector<enode> & lambdas = m_var_data_full[v]->m_lambdas;
+        m_trail_stack.push(push_back_trail<enode *, false>(lambdas));
+        lambdas.push_back(lam);
+        instantiate_default_lambda_def_axiom(lam);        
+    }
+
     void theory_array_full::add_as_array(theory_var v, enode* arr) {
         var_data * d  = m_var_data[v];
         unsigned lambda_equiv_class_size = get_lambda_equiv_size(v, d);
@@ -238,6 +249,10 @@ namespace smt {
             instantiate_default_as_array_axiom(n);
             d->m_as_arrays.push_back(n);
         }
+        else if (m.is_lambda_def(n->get_decl())) {
+            instantiate_default_lambda_def_axiom(n);
+            d->m_lambdas.push_back(n);
+        }
         return r;
     }
 
@@ -331,18 +346,16 @@ namespace smt {
         // v1 is the new root
         SASSERT(v1 == find(v1));
         var_data_full * d2 = m_var_data_full[v2];
-        for (enode * n : d2->m_maps) {
+        for (enode * n : d2->m_maps) 
             add_map(v1, n);
-        }
-        for (enode * n : d2->m_parent_maps) {
+        for (enode * n : d2->m_parent_maps) 
             add_parent_map(v1, n);
-        }
-        for (enode * n : d2->m_consts) {
+        for (enode * n : d2->m_consts) 
             add_const(v1, n);
-        }
-        for (enode * n : d2->m_as_arrays) {
+        for (enode * n : d2->m_as_arrays) 
             add_as_array(v1, n);
-        }
+        for (enode* n : d2->m_lambdas)
+            add_lambda(v1, n);
         TRACE("array", 
               tout << pp(get_enode(v1), m) << "\n";
               tout << pp(get_enode(v2), m) << "\n";
@@ -577,6 +590,23 @@ namespace smt {
 #endif
     }
 
+    bool theory_array_full::instantiate_default_lambda_def_axiom(enode* arr) {
+        if (!ctx.add_fingerprint(this, m_default_lambda_fingerprint, 1, &arr))
+            return false;
+        m_stats.m_num_default_lambda_axiom++;
+        expr* def = mk_default(arr->get_expr());
+        quantifier* lam = m.is_lambda_def(arr->get_decl());
+        expr_ref_vector args(m);
+        args.push_back(lam);
+        for (unsigned i = 0; i < lam->get_num_decls(); ++i) 
+            args.push_back(mk_epsilon(lam->get_decl_sort(i)).first);
+        expr_ref val(mk_select(args), m);
+        ctx.internalize(def, false);
+        ctx.internalize(val.get(), false);
+        return try_assign_eq(val.get(), def);
+    }
+
+
     bool theory_array_full::has_unitary_domain(app* array_term) {
         SASSERT(is_array_sort(array_term));
         sort* s = array_term->get_sort();
@@ -863,5 +893,6 @@ namespace smt {
         st.update("array def store", m_stats.m_num_default_store_axiom);
         st.update("array def as-array", m_stats.m_num_default_as_array_axiom);
         st.update("array sel as-array", m_stats.m_num_select_as_array_axiom);
+        st.update("array def lambda", m_stats.m_num_default_lambda_axiom);
     }
 }
diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h
index 19b0e2f6d..09a6daaec 100644
--- a/src/smt/theory_array_full.h
+++ b/src/smt/theory_array_full.h
@@ -28,6 +28,7 @@ namespace smt {
             ptr_vector<enode>  m_maps;
             ptr_vector<enode>  m_consts;
             ptr_vector<enode>  m_as_arrays;
+            ptr_vector<enode>  m_lambdas;
             ptr_vector<enode>  m_parent_maps;
         };
 
@@ -41,6 +42,7 @@ namespace smt {
         static unsigned const m_default_store_fingerprint = UINT_MAX - 113;
         static unsigned const m_default_const_fingerprint = UINT_MAX - 115;
         static unsigned const m_default_as_array_fingerprint = UINT_MAX - 116;
+        static unsigned const m_default_lambda_fingerprint = UINT_MAX - 117;
 
     protected:
 
@@ -66,6 +68,7 @@ namespace smt {
         void add_map(theory_var v, enode* s);
         void add_parent_map(theory_var v, enode* s);
         void add_as_array(theory_var v, enode* arr);
+        void add_lambda(theory_var v, enode* lam);
 
         void add_parent_select(theory_var v, enode * s) override;
         void add_parent_default(theory_var v);        
@@ -76,6 +79,7 @@ namespace smt {
         bool instantiate_default_store_axiom(enode* store);
         bool instantiate_default_map_axiom(enode* map);
         bool instantiate_default_as_array_axiom(enode* arr);
+        bool instantiate_default_lambda_def_axiom(enode* arr);
         bool instantiate_parent_stores_default(theory_var v);
 
         bool has_large_domain(app* array_term);