diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp
index fa17b591d..44c423c09 100644
--- a/src/ast/array_decl_plugin.cpp
+++ b/src/ast/array_decl_plugin.cpp
@@ -571,6 +571,11 @@ func_decl * array_recognizers::get_as_array_func_decl(expr * n) const {
     return to_func_decl(to_app(n)->get_decl()->get_parameter(0).get_ast()); 
 }
 
+func_decl * array_recognizers::get_as_array_func_decl(func_decl * f) const { 
+    SASSERT(is_as_array(f)); 
+    return to_func_decl(f->get_parameter(0).get_ast()); 
+}
+
 array_util::array_util(ast_manager& m): 
     array_recognizers(m.mk_family_id("array")),
     m_manager(m) {
diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h
index beaccfbd3..c735fb811 100644
--- a/src/ast/array_decl_plugin.h
+++ b/src/ast/array_decl_plugin.h
@@ -149,7 +149,9 @@ public:
     bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); }
     bool is_map(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_MAP); }
     bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); }
+    bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); }
     func_decl * get_as_array_func_decl(expr * n) const;
+    func_decl * get_as_array_func_decl(func_decl* f) const;
 };
 
 class array_util : public array_recognizers {
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index b0e97e5e4..61bf8df96 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -40,6 +40,7 @@ Revision History:
 struct evaluator_cfg : public default_rewriter_cfg {
     ast_manager &                   m;
     model_core &                    m_model;
+    params_ref                      m_params;
     bool_rewriter                   m_b_rw;
     arith_rewriter                  m_a_rw;
     bv_rewriter                     m_bv_rw;
@@ -59,6 +60,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
     evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p):
         m(m),
         m_model(md),
+        m_params(p),
         m_b_rw(m),
         // We must allow customers to set parameters for arithmetic rewriter/evaluator.
         // In particular, the maximum degree of algebraic numbers that will be evaluated.
@@ -200,6 +202,26 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 return BR_REWRITE1;
             }
         }
+        if (st == BR_FAILED && num == 0 && m_ar.is_as_array(f)) {
+            func_decl* g = nullptr;
+            VERIFY(m_ar.is_as_array(f, g));
+            expr* def = nullptr;
+            quantifier* q = nullptr;
+            proof* def_pr = nullptr;
+            if (get_macro(g, def, q, def_pr)) {
+                sort_ref_vector vars(m);
+                svector<symbol> var_names;
+                for (unsigned i = 0; i < g->get_arity(); ++i) {
+                    var_names.push_back(symbol(i));
+                    vars.push_back(g->get_domain(g->get_arity() - i - 1));
+                }
+                result = m.mk_lambda(vars.size(), vars.c_ptr(), var_names.c_ptr(), def);
+                model_evaluator ev(m_model, m_params);
+                result = ev(result);
+                return BR_DONE;
+            }
+        }
+
         CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
         return st;
     }
@@ -222,7 +244,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         }
     }
 
-    bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
+    bool get_macro(func_decl * f, expr * & def, quantifier * & , proof * &) {
 
 #define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
 
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 96b1588a2..9688b1d6e 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1032,7 +1032,7 @@ namespace sat {
         }
 
         void insert(literal l) {
-            VERIFY(process_var(l.var()));
+            SASSERT(process_var(l.var()));
             m_queue.insert(l);
         }
 
@@ -1075,6 +1075,7 @@ namespace sat {
         }
 
         void insert_queue() {
+            m_queue.reset();
             unsigned num_vars = s.s.num_vars();
             for (bool_var v = 0; v < num_vars; v++) {
                 if (process_var(v)) {
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 37297997a..dc3f80385 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2873,9 +2873,9 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
             ctx.get_assignment(i_lt_len_s) == l_true) {
             len = m_autil.mk_int(1);
             lits.append(2, _lits);
+            TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
             return true;
         }
-        TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
     }
     else if (is_pre(e, s, i)) {
         expr_ref zero(m_autil.mk_int(0), m);
@@ -2887,9 +2887,9 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
             ctx.get_assignment(i_lt_len_s) == l_true) {
             len = i;
             lits.append(2, _lits);
+            TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
             return true;
         }
-        TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
     }
     else if (is_post(e, s, l)) {
         expr_ref zero(m_autil.mk_int(0), m);
@@ -2900,9 +2900,9 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
             ctx.get_assignment(l_le_len_s) == l_true) {
             len = l;
             lits.append(2, _lits);
+            TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
             return true;
         }
-        TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
     }
     else if (is_skolem(m_tail, e)) {
         // e = tail(s, l), len(s) > l => len(tail(s, l)) = len(s) - l - 1
@@ -4942,6 +4942,7 @@ void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
 
 */
 void theory_seq::add_at_axiom(expr* e) {
+    TRACE("seq", tout << "at-axiom: " << mk_pp(e, m) << "\n";);
     expr* s = nullptr, *i = nullptr;
     VERIFY(m_util.str.is_at(e, s, i));
     expr_ref zero(m_autil.mk_int(0), m);
@@ -5082,9 +5083,36 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
     TRACE("seq", ctx.display_literals_verbose(tout << "assert:\n", lits) << "\n";);
     m_new_propagation = true;
     ++m_stats.m_add_axiom;
+
+#if 0
+    static unsigned level = 0;
+    if (level == 0) {
+        level++;
+        disable_trace("seq");
+        kernel k(m, ctx.get_fparams());
+        expr_ref tmp(m);
+        for (literal lit: lits) {
+            ctx.literal2expr(~lit, tmp);
+            k.assert_expr(tmp);
+        }
+        lbool r = k.check();        
+        enable_trace("seq");
+        if (r == l_true) {
+            k.display(std::cout); std::cout << "\n";
+            TRACE("seq", k.display(tout << "sat\n"); tout << "\n";);
+        }
+        level--;
+    }
+#endif
     ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
 }
 
+#if 0
+void theory_seq::dump_axiom(literal_vector const& lits) {
+    display_lemma_as_smt_problem(std::cout << "; lemma\n", lits.size(), lits.c_ptr());
+}
+#endif
+
 expr_ref theory_seq::coalesce_chars(expr* const& e) {
     context& ctx = get_context();
     expr* s;