diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp
index 88ded842f..0dcdd9597 100644
--- a/src/ast/normal_forms/defined_names.cpp
+++ b/src/ast/normal_forms/defined_names.cpp
@@ -159,11 +159,11 @@ void defined_names::impl::bound_vars(sort_ref_buffer const & sorts, buffer<symbo
         expr * patterns[1] = { m.mk_pattern(name) };
         quantifier_ref q(m);
         q = m.mk_forall(sorts.size(),
-                                sorts.c_ptr(),
-                                names.c_ptr(),
-                                def_conjunct,
-                                1, qid, symbol::null,
-                                1, patterns);
+                        sorts.c_ptr(),
+                        names.c_ptr(),
+                        def_conjunct,
+                        1, qid, symbol::null,
+                        1, patterns);
         TRACE("mk_definition_bug", tout << "before elim_unused_vars:\n" << mk_ismt2_pp(q, m) << "\n";);
         result = elim_unused_vars(m, q, params_ref());
         TRACE("mk_definition_bug", tout << "after elim_unused_vars:\n" << result << "\n";);
diff --git a/src/ast/rewriter/array_rewriter.h b/src/ast/rewriter/array_rewriter.h
index a951db725..a8108711a 100644
--- a/src/ast/rewriter/array_rewriter.h
+++ b/src/ast/rewriter/array_rewriter.h
@@ -45,6 +45,7 @@ public:
     }
     ast_manager & m() const { return m_util.get_manager(); }
     family_id get_fid() const { return m_util.get_family_id(); }
+    array_util& util() { return m_util; }
 
     void set_expand_select_store(bool f) { m_expand_select_store = f; }
     void set_expand_select_ite(bool f) { m_expand_select_ite = f; }
diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h
index d380fa707..6895f7218 100644
--- a/src/ast/rewriter/rewriter.h
+++ b/src/ast/rewriter/rewriter.h
@@ -300,7 +300,7 @@ protected:
     void process_var(var * v);
 
     template<bool ProofGen>
-    void process_const(app * t);
+    bool process_const(app * t);
 
     template<bool ProofGen>
     bool visit(expr * t, unsigned max_depth);
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 0eeb1f52f..f628c2225 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -80,27 +80,42 @@ void rewriter_tpl<Config>::process_var(var * v) {
 
 template<typename Config>
 template<bool ProofGen>
-void rewriter_tpl<Config>::process_const(app * t) {
+bool rewriter_tpl<Config>::process_const(app * t0) {
+    app_ref t(t0, m());
+    bool rounds = 0;
+ retry:
     SASSERT(t->get_num_args() == 0);
     br_status st = m_cfg.reduce_app(t->get_decl(), 0, nullptr, m_r, m_pr);
     SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
-    SASSERT(st == BR_FAILED || st == BR_DONE);
-    if (st == BR_DONE) {
+    switch (st) {
+    case BR_FAILED:
+        if (rounds == 0) {
+            result_stack().push_back(t);
+            if (ProofGen)
+                result_pr_stack().push_back(nullptr); // implicit reflexivity
+            return true;
+        }
+        m_r = t;
+        // fall through
+    case BR_DONE:
         result_stack().push_back(m_r.get());
         if (ProofGen) {
             if (m_pr)
                 result_pr_stack().push_back(m_pr);
             else
-                result_pr_stack().push_back(m().mk_rewrite(t, m_r));
+                result_pr_stack().push_back(m().mk_rewrite(t0, m_r));
             m_pr = nullptr;
         }
         m_r = nullptr;
-        set_new_child_flag(t);
-    }
-    else {
-        result_stack().push_back(t);
-        if (ProofGen)
-            result_pr_stack().push_back(nullptr); // implicit reflexivity
+        set_new_child_flag(t0);
+        return true;
+    default: 
+        if (is_app(m_r) && to_app(m_r)->get_num_args() == 0) {
+            t = to_app(m_r);
+            rounds++;
+            goto retry;
+        }
+        return false;
     }
 }
 
@@ -115,6 +130,7 @@ void rewriter_tpl<Config>::process_const(app * t) {
 template<typename Config>
 template<bool ProofGen>
 bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
+ // retry:
     TRACE("rewriter_visit", tout << "visiting\n" << mk_ismt2_pp(t, m()) << "\n";);
     expr *  new_t = nullptr;
     proof * new_t_pr = nullptr;
@@ -164,15 +180,14 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
     switch (t->get_kind()) {
     case AST_APP:
         if (to_app(t)->get_num_args() == 0) {
-            process_const<ProofGen>(to_app(t));
-            return true;
-        }
-        else {
-            if (max_depth != RW_UNBOUNDED_DEPTH)
-                max_depth--;
-            push_frame(t, c, max_depth);
-            return false;
+            if (process_const<ProofGen>(to_app(t))) 
+                return true; 
+            t = m_r;
         }
+        if (max_depth != RW_UNBOUNDED_DEPTH)
+            max_depth--;
+        push_frame(t, c, max_depth);
+        return false;        
     case AST_VAR:
         process_var<ProofGen>(to_var(t));
         return true;
@@ -224,7 +239,7 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
 template<typename Config>
 template<bool ProofGen>
 void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
-    SASSERT(t->get_num_args() > 0);
+    // SASSERT(t->get_num_args() > 0);
     SASSERT(!frame_stack().empty());
     switch (fr.m_state) {
     case PROCESS_CHILDREN: {
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 4c81ab665..6a64eaa82 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -661,6 +661,13 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                 p1 = m().mk_pull_quant(old_q, q1);
             }
         }
+        else if (
+                 old_q->get_kind() == lambda_k &&
+                 is_ground(new_body)) {
+            result = m_ar_rw.util().mk_const_array(old_q->get_sort(), new_body);
+            result_pr = nullptr;
+            return true;
+        }
         else {
             ptr_buffer<expr> new_patterns_buf;
             ptr_buffer<expr> new_no_patterns_buf;
@@ -677,10 +684,10 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             TRACE("reduce_quantifier", tout << mk_ismt2_pp(old_q, m()) << "\n----->\n" << mk_ismt2_pp(q1, m()) << "\n";);
             SASSERT(is_well_sorted(m(), q1));
         }
-
         SASSERT(m().get_sort(old_q) == m().get_sort(q1));
         result = elim_unused_vars(m(), q1, params_ref());
 
+
         TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << result << "\n";);
 
         result_pr = nullptr;
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index b2b927faf..35cbfe9c7 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -140,24 +140,25 @@ struct evaluator_cfg : public default_rewriter_cfg {
         result_pr = nullptr;
         family_id fid = f->get_family_id();
         bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
+        br_status st = BR_FAILED;
         if (num == 0 && (fid == null_family_id || is_uninterp)) {
             expr * val = m_model.get_const_interp(f);
             if (val != nullptr) {
                 result = val;
-                return BR_DONE;
+                return m_ar.is_as_array(val)? BR_REWRITE1 : BR_DONE;
             }
-
-            if (m_model_completion) {
+            else if (m_model_completion) {
                 sort * s   = f->get_range();
                 expr * val = m_model.get_some_value(s);
                 m_model.register_decl(f, val);
                 result = val;
                 return BR_DONE;
             }
-            return BR_FAILED;
+            else {
+                return BR_FAILED;
+            }
         }
 
-        br_status st = BR_FAILED;
 
         if (fid == m_b_rw.get_fid()) {
             decl_kind k = f->get_decl_kind();
@@ -205,17 +206,18 @@ struct evaluator_cfg : public default_rewriter_cfg {
             TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
                   for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m) << "\n";
                   tout << "---->\n" << mk_ismt2_pp(result, m) << "\n";);
-            return BR_REWRITE1;
+            st = BR_REWRITE1;
         }
         if (st == BR_FAILED && !m.is_builtin_family_id(fid))
             st = evaluate_partial_theory_func(f, num, args, result, result_pr);
         if (st == BR_DONE && is_app(result)) {
             app* a = to_app(result);
             if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) {
-                return BR_REWRITE1;
+                st = BR_REWRITE1;
             }
         }
 #if 1
+        TRACE("model_evaluator", tout << st << " " << num << " " << m_ar.is_as_array(f) << " " << m_model_completion << "\n";);
         if (st == BR_FAILED && num == 0 && m_ar.is_as_array(f) && m_model_completion) {
             func_decl* g = nullptr;
             VERIFY(m_ar.is_as_array(f, g));
@@ -253,6 +255,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
     }
 
     void expand_stores(expr_ref& val) {
+        TRACE("model_evaluator", tout << val << "\n";);
         vector<expr_ref_vector> stores;
         expr_ref else_case(m);
         bool _unused;
@@ -503,6 +506,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
         if (!m_ar.is_as_array(a)) {
             TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m) << "\n";);
+            TRACE("model_evaluator", tout << m_model << "\n";);
             return false;
         }
 
@@ -630,6 +634,7 @@ void model_evaluator::reset(model_core &model, params_ref const& p) {
 void model_evaluator::operator()(expr * t, expr_ref & result) {
     TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";);
     m_imp->operator()(t, result);
+    TRACE("model_evaluator", tout << result << "\n";);
     m_imp->expand_stores(result);
 }
 
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index c27845ff6..065e5d952 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -380,11 +380,9 @@ namespace smt {
     */
     bool model_generator::include_func_interp(func_decl * f) const {
         family_id fid = f->get_family_id();
-        TRACE("model", tout << f->get_name() << " " << fid << "\n";);
         if (fid == null_family_id) return !m_hidden_ufs.contains(f); 
         if (fid == m_manager.get_basic_family_id()) return false;
         theory * th = m_context->get_theory(fid);
-        TRACE("model", tout << th << "\n";);
         if (!th) return true;
         return th->include_func_interp(f);
     }