diff --git a/src/ast/euf/ho_matcher.cpp b/src/ast/euf/ho_matcher.cpp
index acfe800f2..ef4c46069 100644
--- a/src/ast/euf/ho_matcher.cpp
+++ b/src/ast/euf/ho_matcher.cpp
@@ -689,20 +689,21 @@ namespace euf {
         });
         if (!is_ho)
             return { q, p };
-        ptr_vector<expr> todo;
+        vector<std::pair<expr*, unsigned>> todo;
         ptr_buffer<var> bound;
         expr_ref_vector cache(m);
         unsigned nb = q->get_num_decls();
         bool contains_pat2abs = m_pat2abs.contains(p);
-        todo.push_back(p);
+        SASSERT(m.is_pattern(p));
+        todo.push_back({p, 0});
         while (!todo.empty()) {
-            auto t = todo.back();
+            auto [t, lvl] = todo.back();
             if (is_var(t)) {
                 cache.setx(t->get_id(), t);
                 todo.pop_back();
                 continue;
             }
-            if (m_unitary.is_flex(0, t) || m.is_lambda_def(t) || is_lambda(t)) {
+            if ((m_unitary.is_flex(0, t) && lvl > 1) || m.is_lambda_def(t) || is_lambda(t)) {
                 if (!contains_pat2abs)
                     m_pat2abs.insert_if_not_there(p, svector<std::pair<unsigned, expr*>>()).push_back({ nb, t });
                 auto v = m.mk_var(nb++, t->get_sort());
@@ -720,7 +721,7 @@ namespace euf {
                     cache.reserve(arg->get_id() + 1);
                     expr* arg1 = cache.get(arg->get_id());
                     if (!arg1)
-                        todo.push_back(arg);
+                        todo.push_back({arg, lvl + 1});
                     else
                         args.push_back(arg1);
                 }
@@ -736,6 +737,9 @@ namespace euf {
             }
         }
         p1 = to_app(cache.get(p->get_id()));
+
+        if (p1 == p)
+            return {q, p};
         expr_free_vars free_vars;
         free_vars(p1);
         app_ref_vector new_ground(m);
@@ -762,6 +766,8 @@ namespace euf {
         auto body = q->get_expr();
         if (!new_patterns.empty()) {
             ptr_vector<app> pats;
+            CTRACE(ho_matching, !m.is_pattern(p1), 
+                tout << mk_pp(p, m) << "\n" << mk_pp(p1, m) << "\n";);
             VERIFY(m.is_pattern(p1, pats));
             for (auto p : new_patterns) // patterns for variables that are not free in new pattern
                 pats.push_back(p);
@@ -800,6 +806,10 @@ namespace euf {
         if (!contains_pat2abs)
             trail().push(insert_map(m_pat2abs, p));
 
+        TRACE(ho_matching, tout << mk_pp(q, m) << "\n"
+                                << mk_pp(p, m) << "\n->\n"
+                                << mk_pp(q1, m) << "\n"
+                                << mk_pp(p1, m) << "\n");
         return { q1, p1 };
     }
 
diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp
index 997022c69..4bf9ea5ea 100644
--- a/src/ast/normal_forms/defined_names.cpp
+++ b/src/ast/normal_forms/defined_names.cpp
@@ -193,43 +193,7 @@ void defined_names::impl::mk_definition(expr * e, app * n, sort_ref_buffer & var
     else if (m.is_term_ite(e)) {
         bound_vars(var_sorts, var_names, MK_OR(MK_NOT(to_app(e)->get_arg(0)), MK_EQ(n, to_app(e)->get_arg(1))), n, defs);
         bound_vars(var_sorts, var_names, MK_OR(to_app(e)->get_arg(0),         MK_EQ(n, to_app(e)->get_arg(2))), n, defs);
-    }
-    else if (is_lambda(e)) {
-        //    n(y) = \x . M[x,y]
-        // => 
-        //    n(y)[x] = M,  forall x y
-        // 
-        // NB. The pattern is incomplete.
-        // consider store(a, i, v) == \lambda j . if i = j then v else a[j]
-        // the instantiation rules for store(a, i, v) are:
-        //     store(a, i, v)[j] = if i = j then v else a[j] with patterns {a[j], store(a, i, v)} { store(a, i, v)[j] }
-        // The first pattern is not included.
-        // TBD use a model-based scheme for extracting instantiations instead of
-        // using multi-patterns.
-        // 
-
-        quantifier* q = to_quantifier(e);
-        expr_ref_vector args(m);
-        expr_ref n2(m), n3(m);
-        var_shifter vs(m);
-        vs(n, q->get_num_decls(), n2);        
-        args.push_back(n2);
-        var_sorts.append(q->get_num_decls(), q->get_decl_sorts());
-        var_names.append(q->get_num_decls(), q->get_decl_names());
-        for (unsigned i = 0; i < q->get_num_decls(); ++i) {
-            args.push_back(m.mk_var(q->get_num_decls() - i - 1, q->get_decl_sort(i)));
-        }
-        array_util autil(m);
-        func_decl * f = nullptr;
-        if (autil.is_as_array(n2, f)) {
-            n3 = m.mk_app(f, args.size()-1, args.data() + 1);
-        }
-        else {
-            n3 = autil.mk_select(args.size(), args.data());
-        }
-        bound_vars(var_sorts, var_names, MK_EQ(q->get_expr(), n3), to_app(n3), defs, m.lambda_def_qid());
-        
-    }
+    }    
     else {
         bound_vars(var_sorts, var_names, MK_EQ(e, n), n, defs);
     }
diff --git a/src/ast/normal_forms/name_exprs.cpp b/src/ast/normal_forms/name_exprs.cpp
index 9cf1ab08f..577c3d51a 100644
--- a/src/ast/normal_forms/name_exprs.cpp
+++ b/src/ast/normal_forms/name_exprs.cpp
@@ -100,7 +100,7 @@ class name_quantifier_labels : public name_exprs_core {
     public:
         pred(ast_manager & m):m(m) {}
         bool operator()(expr * t) override {
-            return is_quantifier(t) || m.is_label(t);
+            return (is_quantifier(t) && !is_lambda(t)) || m.is_label(t);
         }
     };
     
@@ -127,7 +127,7 @@ class name_nested_formulas : public name_exprs_core {
             TRACE(name_exprs, tout << "name_nested_formulas::pred:\n" << mk_ismt2_pp(t, m) << "\n";);
             if (is_app(t)) 
                 return to_app(t)->get_family_id() == m.get_basic_family_id() && to_app(t)->get_num_args() > 0 && t != m_root;
-            return m.is_label(t) || is_quantifier(t);
+            return m.is_label(t) || (is_quantifier(t) && !is_lambda(t));
         }
     };
     
diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp
index 8ec88096a..2dbe48ac1 100644
--- a/src/ast/pattern/pattern_inference.cpp
+++ b/src/ast/pattern/pattern_inference.cpp
@@ -384,6 +384,8 @@ bool pattern_inference_cfg::contains_subpattern::operator()(expr * n) {
             break;
         case AST_VAR:
             break;
+        case AST_QUANTIFIER: 
+            break;
         default:
             UNREACHABLE();
         }
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 7e32eaaf6..946a480be 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -598,19 +598,7 @@ namespace smt {
         if (e_internalized(q)) 
             return;
         app_ref lam_name(m.mk_fresh_const("lambda", q->get_sort()), m);
-        app_ref eq(m), lam_app(m);
-        expr_ref_vector vars(m);
-        vars.push_back(lam_name);
-        unsigned sz = q->get_num_decls();
-        for (unsigned i = 0; i < sz; ++i) 
-            vars.push_back(m.mk_var(sz - i - 1, q->get_decl_sort(i)));
-        array_util autil(m);
-        lam_app = autil.mk_select(vars.size(), vars.data());
-        eq = m.mk_eq(lam_app, q->get_expr());
-        quantifier_ref fa(m);
-        expr * patterns[1] = { m.mk_pattern(lam_app) };
-        fa = m.mk_forall(sz, q->get_decl_sorts(), q->get_decl_names(), eq, 0, m.lambda_def_qid(), symbol::null, 1, patterns);
-        internalize_quantifier(fa, true);
+        m.add_lambda_def(lam_name->get_decl(), q);
         if (!e_internalized(lam_name)) 
             internalize_uninterpreted(lam_name);
         enode* lam_node = get_enode(lam_name);
@@ -619,9 +607,6 @@ namespace smt {
         m_app2enode.setx(q->get_id(), lam_node, nullptr);
         m_l_internalized_stack.push_back(q);
         m_trail_stack.push_ptr(&m_mk_lambda_trail);
-        bool_var bv = get_bool_var(fa);
-        assign(literal(bv, false), nullptr);
-        mark_as_relevant(bv);
     }
 
     bool context::has_lambda() {
diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp
index 8e3827188..4eeea0ca4 100644
--- a/src/smt/theory_array.cpp
+++ b/src/smt/theory_array.cpp
@@ -68,12 +68,12 @@ namespace smt {
         m_var_data.push_back(alloc(var_data));
         var_data * d  = m_var_data[r];
         TRACE(array, tout << mk_bounded_pp(n->get_expr(), m) << "\nis_array: " << is_array_sort(n) << ", is_select: " << is_select(n) <<
-              ", is_store: " << is_store(n) << "\n";);
+              ", is_store: " << is_store(n) << ", is_lambda: " << is_lambda(n) << "\n";);
         d->m_is_array  = is_array_sort(n);
         if (d->m_is_array) 
             register_sort(n->get_expr()->get_sort());
         d->m_is_select = is_select(n);        
-        if (is_store(n))
+        if (is_store(n) || is_lambda(n))
             d->m_stores.push_back(n);
         ctx.attach_th_var(n, this, r);
         if (laziness() <= 1 && is_store(n))
@@ -95,7 +95,7 @@ namespace smt {
 
         if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
             for (enode* store : d->m_parent_stores) {
-                SASSERT(is_store(store));
+                SASSERT(is_store(store) || is_lambda(store));
                 if (!m_params.m_array_cg || store->is_cgr()) {
                     instantiate_axiom2b(s, store);
                 }
@@ -106,7 +106,7 @@ namespace smt {
     void theory_array::add_parent_store(theory_var v, enode * s) {
         if (m_params.m_array_cg && !s->is_cgr())
             return;
-        SASSERT(is_store(s));
+        SASSERT(is_store(s) || is_lambda(s));
         v                = find(v);
         var_data * d     = m_var_data[v];
         d->m_parent_stores.push_back(s);
@@ -177,7 +177,7 @@ namespace smt {
     void theory_array::add_store(theory_var v, enode * s) {
         if (m_params.m_array_cg && !s->is_cgr())
             return;
-        SASSERT(is_store(s));
+        SASSERT(is_store(s) || is_lambda(s));
         v                = find(v);
         var_data * d     = m_var_data[v];
         unsigned lambda_equiv_class_size = get_lambda_equiv_size(v, d);
@@ -204,7 +204,7 @@ namespace smt {
     void theory_array::instantiate_axiom2a(enode * select, enode * store) {
         TRACE(array, tout << "axiom 2a: #" << select->get_owner_id() << " #" << store->get_owner_id() << "\n";);
         SASSERT(is_select(select));
-        SASSERT(is_store(store));
+        SASSERT(is_store(store) || is_lambda(store));
         if (assert_store_axiom2(store, select))
             m_stats.m_num_axiom2a++;
     }
@@ -212,7 +212,7 @@ namespace smt {
     bool theory_array::instantiate_axiom2b(enode * select, enode * store) {
         TRACE(array_axiom2b, tout << "axiom 2b: #" << select->get_owner_id() << " #" << store->get_owner_id() << "\n";);
         SASSERT(is_select(select));
-        SASSERT(is_store(store));
+        SASSERT(is_store(store) || is_lambda(store));
         if (assert_store_axiom2(store, select)) {
             m_stats.m_num_axiom2b++;
             return true;
@@ -261,7 +261,7 @@ namespace smt {
     }
 
     bool theory_array::internalize_term(app * n) {
-        if (!is_store(n) && !is_select(n)) {
+        if (!is_store(n) && !is_select(n) && !is_lambda(n)) {
             if (!is_array_ext(n))
                 found_unsupported_op(n);
             return false;
@@ -282,7 +282,7 @@ namespace smt {
             if (is_select(n)) {
                 add_parent_select(v_arg, ctx.get_enode(n));
             }
-            else if (is_store(n)) {
+            else if (is_store(n) || is_lambda(n)) {
                 add_parent_store(v_arg, ctx.get_enode(n));
             }
         }
@@ -325,9 +325,11 @@ namespace smt {
         if (m.is_ite(n)) {
             TRACE(array, tout << "relevant ite " << mk_pp(n, m) << "\n";);
         }
-        if (!is_store(n) && !is_select(n))
+        if (!is_store(n) && !is_select(n) && !is_lambda(n))
             return;
         if (!ctx.e_internalized(n)) ctx.internalize(n, false);
+        if (is_lambda(n))
+            return;
         enode * arg      = ctx.get_enode(to_app(n)->get_arg(0));
         theory_var v_arg = arg->get_th_var(get_id());
         SASSERT(v_arg != null_theory_var);
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index b4966c2a7..2f709b6d4 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -217,18 +217,41 @@ namespace smt {
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         }
     }
+
+    void theory_array_base::assert_lambda_axiom_core(enode* n, enode* select) {
+        SASSERT(is_lambda(n));
+        SASSERT(is_select(select));
+        expr *e = n->get_expr();
+        app *s = select->get_app();
+        auto q = is_quantifier(e) ? to_quantifier(e) : m.is_lambda_def(e);
+        SASSERT(q);
+        SASSERT(::is_lambda(q));
+        SASSERT(q->get_num_decls() == s->get_num_args() - 1);
+        // do the same thing as in sat/smt/array_axioms:
+        ptr_vector<expr> args(s->get_num_args(), s->get_args());
+        args[0] = q;
+        array_util a(m);
+        expr_ref alpha(a.mk_select(args), m);
+        expr_ref beta(alpha);
+        ctx.get_rewriter()(beta);
+        TRACE(array, tout << alpha << " == " << beta << "\n";);
+        auto alpha_n = ensure_enode(alpha);
+        auto beta_n = ensure_enode(beta);
+        ctx.assign_eq(alpha_n, beta_n, eq_justification::mk_axiom());
+    }
     
     bool theory_array_base::assert_store_axiom2(enode * store, enode * select) { 
+        SASSERT(is_store(store) || is_lambda(store));
         unsigned num_args = select->get_num_args();
         unsigned        i = 1;
         for (; i < num_args; ++i) 
-            if (store->get_arg(i)->get_root() != select->get_arg(i)->get_root())
+            if (is_store(store) && store->get_arg(i)->get_root() != select->get_arg(i)->get_root())
                 break;
         if (i == num_args)
             return false;
         if (ctx.add_fingerprint(store, store->get_owner_id(), select->get_num_args() - 1, select->get_args() + 1)) {
             TRACE(array, tout << "adding axiom2 to todo queue\n";);
-            m_axiom2_todo.push_back(std::make_pair(store, select)); 
+            m_axiom2_todo.push_back({store, select}); 
             return true;
         }
         TRACE(array, tout << "axiom already instantiated: #" << store->get_owner_id() << " #" << select->get_owner_id() << "\n";);
@@ -426,7 +449,10 @@ namespace smt {
             m_axiom1_todo.reset();
             for (unsigned i = 0; i < m_axiom2_todo.size(); ++i) {
                 auto [store, select] = m_axiom2_todo[i];
-                assert_store_axiom2_core(store, select);
+                if (is_store(store))
+                    assert_store_axiom2_core(store, select);
+                else
+                    assert_lambda_axiom_core(store, select);
             }
             m_axiom2_todo.reset();
             for (unsigned i = 0; i < m_extensionality_todo.size(); ++i) {
diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h
index f9bf35e13..87d12c156 100644
--- a/src/smt/theory_array_base.h
+++ b/src/smt/theory_array_base.h
@@ -46,6 +46,10 @@ namespace smt {
         bool is_choice(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_CHOICE); }
         bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); }
         bool is_array_sort(expr const* n) const { return is_array_sort(n->get_sort()); }
+        bool is_lambda(expr *n) const {
+            return m.is_lambda_def(n) || ::is_lambda(n);
+        }
+        
 
         bool is_store(enode const * n) const { return is_store(n->get_expr()); }
         bool is_map(enode const* n) const { return is_map(n->get_expr()); }
@@ -55,6 +59,12 @@ namespace smt {
         bool is_choice(enode const* n) const { return is_choice(n->get_expr()); }
         bool is_default(enode const* n) const { return is_default(n->get_expr()); }
         bool is_array_sort(enode const* n) const { return is_array_sort(n->get_sort()); }
+        bool is_lambda(enode const *n) const {
+            return is_lambda(n->get_expr());
+        }
+        
+        
+        
         bool is_select_arg(enode* r);
 
         app * mk_select(unsigned num_args, expr * const * args);
@@ -76,6 +86,7 @@ namespace smt {
         void assert_axiom(literal l);
         void assert_store_axiom1_core(enode * n);
         void assert_store_axiom2_core(enode * store, enode * select);
+        void assert_lambda_axiom_core(enode *lambda, enode *select);
         void assert_store_axiom1(enode * n) { m_axiom1_todo.push_back(n); }
         bool assert_store_axiom2(enode * store, enode * select);
 
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index 28f4f17d8..0a046e023 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -248,7 +248,7 @@ namespace smt {
             instantiate_default_as_array_axiom(n);
             d->m_as_arrays.push_back(n);
         }
-        else if (m.is_lambda_def(n->get_expr())) {
+        else if (is_lambda(n)) {
             instantiate_default_lambda_def_axiom(n);
             d->m_lambdas.push_back(n);
             m_lambdas.push_back(n);
@@ -329,9 +329,6 @@ namespace smt {
             ctx.push_trail(push_back_vector(m_as_array));
             instantiate_default_as_array_axiom(node);
         }
-        else if (is_choice(n)) {
-            instantiate_choice_axiom(node);
-        }
         else if (is_array_ext(n)) {
             SASSERT(n->get_num_args() == 2);
             instantiate_extensionality(ctx.get_enode(n->get_arg(0)), ctx.get_enode(n->get_arg(1)));
@@ -371,8 +368,8 @@ namespace smt {
         TRACE(array, tout << "v" << v << " " << pp(get_enode(v), m) << " " 
               << d->m_prop_upward << " " << m_params.m_array_delay_exp_axiom << "\n";);
         for (enode * store : d->m_stores) {
-            SASSERT(is_store(store));
-            instantiate_default_store_axiom(store);
+            if (is_store(store))
+                instantiate_default_store_axiom(store);
         }        
 
         if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
@@ -410,7 +407,7 @@ namespace smt {
         TRACE(array, tout << mk_pp(n, m) << "\n";);
         theory_array::relevant_eh(n);
         if (!is_default(n) && !is_select(n) && !is_map(n) && 
-            !is_const(n) && !is_as_array(n) && !is_choice(n) && !is_lambda(n)){
+            !is_const(n) && !is_as_array(n) && !is_choice(n)) {
             return;
         }
         ctx.ensure_internalized(n);
@@ -447,10 +444,8 @@ namespace smt {
             instantiate_default_as_array_axiom(node);
         }
         else if (is_choice(n)) {
-            instantiate_choice_axiom(node);
-        }
-        else if (is_lambda(n)) {
-            NOT_IMPLEMENTED_YET();
+            m_choice_terms.push_back(node);
+            ctx.push_trail(push_back_vector(m_choice_terms));            
         }
     }
 
@@ -585,7 +580,7 @@ namespace smt {
         m_stats.m_num_default_lambda_axiom++;
         expr* e = arr->get_expr();
         expr_ref def(mk_default(e), m);
-        quantifier* lam = m.is_lambda_def(e);
+        quantifier* lam = is_quantifier(e) ? to_quantifier(e) : m.is_lambda_def(e);
         TRACE(array, tout << mk_pp(lam, m) << "\n" << mk_pp(e, m) << "\n");
         expr_ref_vector args(m);       
         var_subst subst(m, false);
@@ -627,8 +622,9 @@ namespace smt {
         symbol x_name("x");
         expr_ref q(m.mk_forall(1, &x_sort, &x_name, ax), m);
         ctx.get_rewriter()(q);
-        literal l = mk_literal(q);
-        assert_axiom(l);
+        TRACE(array, tout << "choice " << q << "\n");        
+        ctx.assert_expr(q);
+        ctx.internalize_assertions();
         return true;
     }
 
@@ -783,6 +779,16 @@ namespace smt {
         return {eps, diag};
     }
 
+    void theory_array_full::propagate() {
+        if (m_choice_qhead == m_choice_terms.size())
+            return;
+        ctx.push_trail(value_trail(m_choice_qhead));
+        for (; m_choice_qhead < m_choice_terms.size(); ++m_choice_qhead) {
+            enode *choice = m_choice_terms[m_choice_qhead];
+            instantiate_choice_axiom(choice);
+        }
+    }
+
     final_check_status theory_array_full::assert_delayed_axioms() {        
         final_check_status r = FC_DONE;
         if (!m_params.m_array_delay_exp_axiom) {
diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h
index 97e9d06a6..f66762e6b 100644
--- a/src/smt/theory_array_full.h
+++ b/src/smt/theory_array_full.h
@@ -37,6 +37,8 @@ namespace smt {
         ast2ast_trailmap<sort, app> m_sort2epsilon;
         ast2ast_trailmap<sort, func_decl> m_sort2diag;
         obj_pair_map<expr, expr, bool> m_eqs;
+        enode_vector m_choice_terms;
+        unsigned m_choice_qhead = 0;
         
         static unsigned const m_default_map_fingerprint = UINT_MAX - 112;
         static unsigned const m_default_store_fingerprint = UINT_MAX - 113;
@@ -111,6 +113,8 @@ namespace smt {
         void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) override;
         void display_var(std::ostream & out, theory_var v) const override;
         void collect_statistics(::statistics & st) const override;
+        bool can_propagate() override { return theory_array::can_propagate() || m_choice_qhead < m_choice_terms.size(); }
+        void propagate() override;
     };
 
 };