diff --git a/src/ackermannization/ackermannize_bv_model_converter.cpp b/src/ackermannization/ackermannize_bv_model_converter.cpp
index 360714c8ba8..92b63ca0fa0 100644
--- a/src/ackermannization/ackermannize_bv_model_converter.cpp
+++ b/src/ackermannization/ackermannize_bv_model_converter.cpp
@@ -18,5 +18,5 @@
 #include "ackermannization/ackermannize_bv_model_converter.h"
 
 model_converter * mk_ackermannize_bv_model_converter(ast_manager & m, const ackr_info_ref& info) {
- return mk_ackr_model_converter(m, info);
+    return mk_ackr_model_converter(m, info);
 }
diff --git a/src/ackermannization/ackr_bound_probe.cpp b/src/ackermannization/ackr_bound_probe.cpp
index 4c18a3f7ee0..1c780386be4 100644
--- a/src/ackermannization/ackr_bound_probe.cpp
+++ b/src/ackermannization/ackr_bound_probe.cpp
@@ -14,9 +14,10 @@
 
  Revision History:
 --*/
+#include "ast/array_decl_plugin.h"
+#include "ast/ast_smt2_pp.h"
 #include "ackermannization/ackr_helper.h"
 #include "ackermannization/ackr_bound_probe.h"
-#include "ast/ast_smt2_pp.h"
 
 /*
   For each function f, calculate the number of its occurrences o_f and compute "o_f choose 2".
@@ -24,32 +25,56 @@
   This upper bound might be crude because some congruence lemmas trivially simplify to true.
 */
 class ackr_bound_probe : public probe {
+
     struct proc {
         typedef ackr_helper::fun2terms_map fun2terms_map;
+        typedef ackr_helper::sel2terms_map sel2terms_map;
         typedef ackr_helper::app_set       app_set;
-        ast_manager&                 m_m;
+        ast_manager&                 m;
         fun2terms_map                m_fun2terms; // a map from functions to occurrences
+        sel2terms_map                m_sel2terms; // a map from functions to occurrences
         ackr_helper                  m_ackr_helper;
+        expr_mark                    m_non_select;
 
-        proc(ast_manager & m) : m_m(m), m_ackr_helper(m) { }
+        proc(ast_manager & m) : m(m), m_ackr_helper(m) { }
 
         ~proc() {
-            fun2terms_map::iterator it = m_fun2terms.begin();
-            const fun2terms_map::iterator end = m_fun2terms.end();
-            for (; it != end; ++it) dealloc(it->get_value());
+            for (auto & kv : m_fun2terms) {
+                dealloc(kv.m_value);
+            }
+            for (auto & kv : m_sel2terms) {
+                dealloc(kv.m_value);
+            }
+        }
+
+        void prune_non_select() {
+            m_ackr_helper.prune_non_select(m_sel2terms, m_non_select);
         }
 
         void operator()(quantifier *) {}
         void operator()(var *) {}
         void operator()(app * a) {
             if (a->get_num_args() == 0) return;
-            if (!m_ackr_helper.should_ackermannize(a)) return;
-            func_decl* const fd = a->get_decl();
+            m_ackr_helper.mark_non_select(a, m_non_select);
             app_set* ts = nullptr;
-            if (!m_fun2terms.find(fd, ts)) {
-                ts = alloc(app_set);
-                m_fun2terms.insert(fd, ts);
+            if (m_ackr_helper.is_select(a)) {
+                app* sel = to_app(a->get_arg(0));
+                if (!m_sel2terms.find(sel, ts)) {
+                    ts = alloc(app_set);
+                    m_sel2terms.insert(sel, ts);
+                }
+            }
+            else if (m_ackr_helper.is_uninterp_fn(a)) {
+                func_decl* const fd = a->get_decl();
+                if (!m_fun2terms.find(fd, ts)) {
+                    ts = alloc(app_set);
+                    m_fun2terms.insert(fd, ts);
+                }
+            }
+            else {
+                return;
             }
+            
             ts->insert(a);
         }
     };
@@ -64,7 +89,8 @@ class ackr_bound_probe : public probe {
         for (unsigned i = 0; i < sz; i++) {
             for_each_expr_core<proc, expr_fast_mark1, true, true>(p, visited, g.form(i));
         }
-        const double total = ackr_helper::calculate_lemma_bound(p.m_fun2terms);
+        p.prune_non_select();
+        double total = ackr_helper::calculate_lemma_bound(p.m_fun2terms, p.m_sel2terms);
         TRACE("ackermannize", tout << "total=" << total << std::endl;);
         return result(total);
     }
diff --git a/src/ackermannization/ackr_helper.cpp b/src/ackermannization/ackr_helper.cpp
index 2e0fda6874c..3e8bc09f0fd 100644
--- a/src/ackermannization/ackr_helper.cpp
+++ b/src/ackermannization/ackr_helper.cpp
@@ -16,14 +16,13 @@
 --*/
 #include "ackermannization/ackr_helper.h"
 
-double ackr_helper::calculate_lemma_bound(ackr_helper::fun2terms_map& occurrences) {
-    fun2terms_map::iterator it = occurrences.begin();
-    const fun2terms_map::iterator end = occurrences.end();
+double ackr_helper::calculate_lemma_bound(fun2terms_map const& occs1, sel2terms_map const& occs2) {
     double total = 0;
-    for (; it != end; ++it) {
-        const unsigned fsz = it->m_value->size();
-        const double n2 = n_choose_2_chk(fsz);
-        total += n2;
+    for (auto const& kv : occs1) {
+        total += n_choose_2_chk(kv.m_value->size());
+    }
+    for (auto const& kv : occs2) {
+        total += n_choose_2_chk(kv.m_value->size());
     }
     return total;
 }
diff --git a/src/ackermannization/ackr_helper.h b/src/ackermannization/ackr_helper.h
index 651b25b12f4..422f7475125 100644
--- a/src/ackermannization/ackr_helper.h
+++ b/src/ackermannization/ackr_helper.h
@@ -18,45 +18,86 @@
 #define ACKR_HELPER_H_
 
 #include "ast/bv_decl_plugin.h"
+#include "ast/array_decl_plugin.h"
 
 class ackr_helper {
-    public:
-        typedef obj_hashtable<app>           app_set;
-        typedef obj_map<func_decl, app_set*> fun2terms_map;
-
-        ackr_helper(ast_manager& m) : m_bvutil(m) {}
-
-        /**
-        \brief  Determines if a given function should be Ackermannized.
-
-         This includes all uninterpreted functions but also "special" functions, e.g. OP_BSMOD0,
-         which are not marked as uninterpreted but effectively are.
-        */
-        inline bool should_ackermannize(app const * a) const {
-            if (is_uninterp(a))
-                return true;
-            else {
-                decl_plugin * p = m_bvutil.get_manager().get_plugin(a->get_family_id());
-                return p->is_considered_uninterpreted(a->get_decl());
+public:
+    typedef obj_hashtable<app>           app_set;
+    typedef obj_map<func_decl, app_set*> fun2terms_map;
+    typedef obj_map<app, app_set*>      sel2terms_map;
+    
+    ackr_helper(ast_manager& m) : m_bvutil(m), m_autil(m) {}
+    
+    /**
+       \brief  Determines if a given function should be Ackermannized.
+       
+       This includes all uninterpreted functions but also "special" functions, e.g. OP_BSMOD0,
+       which are not marked as uninterpreted but effectively are.
+    */
+    inline bool is_uninterp_fn(app const * a) const {
+        if (is_uninterp(a))
+            return true;
+        else {
+            decl_plugin * p = m_bvutil.get_manager().get_plugin(a->get_family_id());
+            return p->is_considered_uninterpreted(a->get_decl());
+        }
+    }
+
+    /**
+       \brief determines if a term is a candidate select for Ackerman reduction
+    */
+    inline bool is_select(app* a) {
+        return m_autil.is_select(a) && is_uninterp_const(a->get_arg(0));
+    }
+
+    void mark_non_select(app* a, expr_mark& non_select) {
+        if (m_autil.is_select(a)) {
+            bool first = true;
+            for (expr* arg : *a) {
+                if (first) 
+                    first = false; 
+                else 
+                    non_select.mark(arg, true);
             }
         }
-
-        inline bv_util& bvutil() { return m_bvutil; }
-
-        /**
-        \brief Calculates an upper bound for congruence lemmas given a map of function of occurrences.
-        */
-        static double calculate_lemma_bound(fun2terms_map& occurrences);
-
-        /** \brief Calculate n choose 2. **/
-        inline static unsigned n_choose_2(unsigned n) { return n & 1 ? (n * (n >> 1)) : (n >> 1) * (n - 1); }
-
-        /** \brief Calculate n choose 2 guarded for overflow. Returns infinity if unsafe. **/
-        inline static double n_choose_2_chk(unsigned n) {
-            SASSERT(std::numeric_limits<unsigned>().max() & 32);
-            return n & (1 << 16) ? std::numeric_limits<double>().infinity() : n_choose_2(n);
+        else {
+            for (expr* arg : *a) {
+                non_select.mark(arg, true);
+            }
+        }
+    }
+
+    void prune_non_select(obj_map<app, app_set*> & sels, expr_mark& non_select) {
+        ptr_vector<app> nons;
+        for (auto& kv : sels) {
+            if (non_select.is_marked(kv.m_key)) {
+                nons.push_back(kv.m_key);
+                dealloc(kv.m_value);
+            }
+        }
+        for (app* s : nons) {
+            sels.erase(s);
         }
-    private:
-        bv_util                              m_bvutil;
+    }
+    
+    inline bv_util& bvutil() { return m_bvutil; }
+    
+    /**
+       \brief Calculates an upper bound for congruence lemmas given a map of function of occurrences.
+    */
+    static double calculate_lemma_bound(fun2terms_map const& occs1, sel2terms_map const& occs2);
+    
+    /** \brief Calculate n choose 2. **/
+    inline static unsigned n_choose_2(unsigned n) { return n & 1 ? (n * (n >> 1)) : (n >> 1) * (n - 1); }
+    
+    /** \brief Calculate n choose 2 guarded for overflow. Returns infinity if unsafe. **/
+    inline static double n_choose_2_chk(unsigned n) {
+        SASSERT(std::numeric_limits<unsigned>().max() & 32);
+        return n & (1 << 16) ? std::numeric_limits<double>().infinity() : n_choose_2(n);
+    }
+    
+private:
+    bv_util                              m_bvutil;
+    array_util                           m_autil;
 };
-#endif /* ACKR_HELPER_H_6475 */
+#endif /* ACKR_HELPER_H_ */
diff --git a/src/ackermannization/ackr_info.h b/src/ackermannization/ackr_info.h
index db5f64a70b6..5180b68d968 100644
--- a/src/ackermannization/ackr_info.h
+++ b/src/ackermannization/ackr_info.h
@@ -16,9 +16,9 @@ Revision History:
 #ifndef ACKR_INFO_H_
 #define ACKR_INFO_H_
 
+#include "util/ref.h"
 #include "util/obj_hashtable.h"
 #include "ast/ast.h"
-#include "util/ref.h"
 #include "ast/rewriter/expr_replacer.h"
 #include "ast/ast_translation.h"
 
@@ -34,18 +34,18 @@ Revision History:
 **/
 class ackr_info {
     public:
-        ackr_info(ast_manager& m)
-        : m_m(m)
-        , m_er(mk_default_expr_replacer(m))
-        , m_subst(m_m)
-        , m_ref_count(0)
-        , m_sealed(false)
+        ackr_info(ast_manager& m) : 
+            m(m),
+            m_er(mk_default_expr_replacer(m)),
+            m_subst(m),
+            m_ref_count(0),
+            m_sealed(false)
         {}
 
         virtual ~ackr_info() {
-            for (t2ct::iterator i = m_t2c.begin(); i != m_t2c.end(); ++i) {
-                m_m.dec_ref(i->m_key);
-                m_m.dec_ref(i->m_value);
+            for (auto & kv : m_t2c) {
+                m.dec_ref(kv.m_key);
+                m.dec_ref(kv.m_value);
             }
         }
 
@@ -55,13 +55,15 @@ class ackr_info {
             m_t2c.insert(term,c);
             m_c2t.insert(c->get_decl(),term);
             m_subst.insert(term, c);
-            m_m.inc_ref(term);
-            m_m.inc_ref(c);
+            m.inc_ref(term);
+            m.inc_ref(c);
         }
 
-        inline void abstract(expr * e, expr_ref& res) {
+        inline expr_ref abstract(expr * e) {
+            expr_ref res(m);
             SASSERT(m_sealed);
             (*m_er)(e, res);
+            return res;
         }
 
         inline app* find_term(func_decl* c)  const {
@@ -71,22 +73,18 @@ class ackr_info {
         }
 
         inline app* get_abstr(app* term)  const {
-            app * const rv = m_t2c.find(term);
-            SASSERT(rv);
-            return rv;
+            return m_t2c.find(term);
         }
 
         inline void seal() {
-            m_sealed=true;
+            m_sealed = true;
             m_er->set_substitution(&m_subst);
         }
 
         virtual ackr_info * translate(ast_translation & translator) {
             ackr_info * const retv = alloc(ackr_info, translator.to());
-            for (t2ct::iterator i = m_t2c.begin(); i != m_t2c.end(); ++i) {
-                app * const k = translator(i->m_key);
-                app * const v = translator(i->m_value);
-                retv->set_abstr(k, v);
+            for (auto & kv : m_t2c) {
+                retv->set_abstr(translator(kv.m_key), translator(kv.m_value));
             }
             if (m_sealed) retv->seal();
             return retv;
@@ -102,10 +100,11 @@ class ackr_info {
                 dealloc(this);
             }
         }
+
     private:
         typedef obj_map<app, app*> t2ct;
         typedef obj_map<func_decl, app*> c2tt;
-        ast_manager& m_m;
+        ast_manager& m;
 
         t2ct m_t2c; // terms to constants
         c2tt m_c2t; // constants to terms (inversion of m_t2c)
diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp
index 4815d5a2c06..d239fe744da 100644
--- a/src/ackermannization/ackr_model_converter.cpp
+++ b/src/ackermannization/ackr_model_converter.cpp
@@ -13,9 +13,11 @@ Module Name:
 
 Revision History:
 --*/
-#include "ackermannization/ackr_model_converter.h"
-#include "model/model_evaluator.h"
+
 #include "ast/ast_smt2_pp.h"
+#include "ast/array_decl_plugin.h"
+#include "model/model_evaluator.h"
+#include "ackermannization/ackr_model_converter.h"
 #include "ackermannization/ackr_info.h"
 
 
@@ -24,17 +26,17 @@ class ackr_model_converter : public model_converter {
     ackr_model_converter(ast_manager & m,
                          const ackr_info_ref& info,
                          model_ref& abstr_model)
-        : m(m)
-        , info(info)
-        , abstr_model(abstr_model)
-        , fixed_model(true)
+        : m(m),
+          info(info),
+          abstr_model(abstr_model),
+          fixed_model(true)
     { }
 
     ackr_model_converter(ast_manager & m,
                          const ackr_info_ref& info)
-        : m(m)
-        , info(info)
-        , fixed_model(false)
+        : m(m),
+          info(info),
+          fixed_model(false)
     { }
 
     ~ackr_model_converter() override { }
@@ -74,6 +76,9 @@ class ackr_model_converter : public model_converter {
     void add_entry(model_evaluator & evaluator,
                    app* term, expr* value,
                    obj_map<func_decl, func_interp*>& interpretations);
+    void add_entry(model_evaluator & evaluator,
+                   app* term, expr* value,
+                   obj_map<app, expr*>& interpretations);
     void convert_constants(model * source, model * destination);
 };
 
@@ -86,8 +91,11 @@ void ackr_model_converter::convert(model * source, model * destination) {
 void ackr_model_converter::convert_constants(model * source, model * destination) {
     TRACE("ackermannize", tout << "converting constants\n";);
     obj_map<func_decl, func_interp*> interpretations;
+    obj_map<app, expr*> array_interpretations; 
     model_evaluator evaluator(*source);
     evaluator.set_model_completion(true);
+    array_util autil(m);
+
     for (unsigned i = 0; i < source->get_num_constants(); i++) {
         func_decl * const c = source->get_constant(i);
         app * const term = info->find_term(c);
@@ -95,19 +103,53 @@ void ackr_model_converter::convert_constants(model * source, model * destination
         if (!term) {
             destination->register_decl(c, value);
         }
+        else if (autil.is_select(term)) {
+            add_entry(evaluator, term, value, array_interpretations);
+        }
         else {
             add_entry(evaluator, term, value, interpretations);
         }
     }
 
-    obj_map<func_decl, func_interp*>::iterator e = interpretations.end();
-    for (obj_map<func_decl, func_interp*>::iterator i = interpretations.begin();
-         i != e; ++i) {
-        func_decl* const fd = i->m_key;
-        func_interp* const fi = i->get_value();
+    for (auto & kv : interpretations) {
+        func_decl* const fd = kv.m_key;
+        func_interp* const fi = kv.m_value;
         fi->set_else(m.get_some_value(fd->get_range()));
         destination->register_decl(fd, fi);
     }
+    for (auto & kv : array_interpretations) {
+        destination->register_decl(kv.m_key->get_decl(), kv.m_value);
+    }
+}
+
+void ackr_model_converter::add_entry(model_evaluator & evaluator,
+                                     app* term, expr* value,
+                                     obj_map<app, expr*>& array_interpretations) {
+    
+    array_util autil(m);
+    app* A = to_app(term->get_arg(0));
+    expr * e = nullptr, *c = nullptr;
+    if (!array_interpretations.find(A, e)) {
+        e = autil.mk_const_array(m.get_sort(A), value);
+    }
+    else {
+        // avoid storing the same as the default value.
+        c = e;
+        while (autil.is_store(c)) c = to_app(c)->get_arg(0);
+        if (autil.is_const(c, c) && c == value) {
+            return;
+        }
+        expr_ref_vector args(m);
+        unsigned sz = term->get_num_args();
+        args.push_back(e);
+        for (unsigned i = 1; i < sz; ++i) {
+            expr * arg = term->get_arg(i);
+            args.push_back(evaluator(info->abstract(arg)));
+        }    
+        args.push_back(value);
+        e = autil.mk_store(args.size(), args.c_ptr());
+    }
+    array_interpretations.insert(A, e);
 }
 
 void ackr_model_converter::add_entry(model_evaluator & evaluator,
@@ -116,8 +158,7 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator,
     TRACE("ackermannize", tout << "add_entry"
           << mk_ismt2_pp(term, m, 2)
           << "->"
-          << mk_ismt2_pp(value, m, 2) << "\n";
-    );
+          << mk_ismt2_pp(value, m, 2) << "\n";);
 
     func_interp * fi = nullptr;
     func_decl * const declaration = term->get_decl();
@@ -128,20 +169,16 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator,
         interpretations.insert(declaration, fi);
     }
     expr_ref_vector args(m);
-    for (unsigned gi = 0; gi < sz; ++gi) {
-        expr * const arg = term->get_arg(gi);
-        expr_ref aarg(m);
-        info->abstract(arg, aarg);
-        expr_ref arg_value(m);
-        evaluator(aarg, arg_value);
-        args.push_back(std::move(arg_value));
+    for (expr* arg : *term) {
+        args.push_back(evaluator(info->abstract(arg)));
     }
     if (fi->get_entry(args.c_ptr()) == nullptr) {
         TRACE("ackermannize",
               tout << mk_ismt2_pp(declaration, m) << " args: " << std::endl;
-                for (unsigned i = 0; i < args.size(); i++)
-                    tout << mk_ismt2_pp(args.get(i), m) << std::endl;
-                tout << " -> " << mk_ismt2_pp(value, m) << "\n"; );
+              for (expr* arg : args) {
+                  tout << mk_ismt2_pp(arg, m) << std::endl;
+              }
+              tout << " -> " << mk_ismt2_pp(value, m) << "\n"; );
         fi->insert_new_entry(args.c_ptr(), value);
     }
     else {
diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp
index 4fe7797d429..83c399f63bb 100644
--- a/src/ackermannization/lackr.cpp
+++ b/src/ackermannization/lackr.cpp
@@ -21,20 +21,22 @@
 #include "ackermannization/lackr_model_constructor.h"
 #include "ackermannization/ackr_info.h"
 #include "ast/for_each_expr.h"
+#include "ast/ast_util.h"
 #include "model/model_smt2_pp.h"
 
 lackr::lackr(ast_manager& m, const params_ref& p, lackr_stats& st,
              const ptr_vector<expr>& formulas, solver * uffree_solver)
-    : m_m(m)
-    , m_p(p)
-    , m_formulas(formulas)
-    , m_abstr(m)
-    , m_sat(uffree_solver)
-    , m_ackr_helper(m)
-    , m_simp(m)
-    , m_ackrs(m)
-    , m_st(st)
-    , m_is_init(false)
+    : m(m),
+      m_p(p),
+      m_formulas(formulas),
+      m_autil(m),
+      m_abstr(m),
+      m_solver(uffree_solver),
+      m_ackr_helper(m),
+      m_simp(m),
+      m_ackrs(m),
+      m_st(st),
+      m_is_init(false)
 {
     updt_params(p);
 }
@@ -44,44 +46,53 @@ void lackr::updt_params(params_ref const & _p) {
     m_eager = p.eager();
 }
 
-lackr::~lackr() {
-    const fun2terms_map::iterator e = m_fun2terms.end();
-    for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
-        dealloc(i->get_value());
+lackr::~lackr() {    
+    for (auto& kv : m_fun2terms) {
+        dealloc(kv.get_value());
+    }
+    for (auto& kv : m_sel2terms) {
+        dealloc(kv.get_value());
     }
 }
 
-lbool lackr::operator() () {
-    SASSERT(m_sat);
-    if (!init()) return l_undef;
-    const lbool rv = m_eager ? eager() : lazy();
-    if (rv == l_true) m_sat->get_model(m_model);
-    CTRACE("ackermannize", rv == l_true,
-        model_smt2_pp(tout << "abstr_model(\n", m_m, *(m_model.get()), 2); tout << ")\n"; );
+lbool lackr::operator()() {
+    SASSERT(m_solver);
+    if (!init()) 
+        return l_undef;
+    lbool rv = m_eager ? eager() : lazy();
+    if (rv == l_true) {
+        m_solver->get_model(m_model);
+    }
+    CTRACE("ackermannize", rv == l_true, model_smt2_pp(tout << "abstr_model(\n", m, *(m_model.get()), 2); tout << ")\n"; );
     return rv;
 }
 
-bool lackr::mk_ackermann(/*out*/goal_ref& g, double lemmas_upper_bound) {
-    if (lemmas_upper_bound <= 0) return false;
-    if (!init()) return false;
-    if (lemmas_upper_bound != std::numeric_limits<double>::infinity()) {
-        const double lemmas_bound = ackr_helper::calculate_lemma_bound(m_fun2terms);
-        if (lemmas_bound > lemmas_upper_bound) return false;
-    }
+bool lackr::mk_ackermann(/*out*/goal_ref& g, double lemmas_upper_bound) {    
+    if (lemmas_upper_bound <= 0)
+        return false;
+    if (!init())
+        return false;
+    if (lemmas_upper_bound != std::numeric_limits<double>::infinity() &&
+        ackr_helper::calculate_lemma_bound(m_fun2terms, m_sel2terms) > lemmas_upper_bound) 
+        return false;
     eager_enc();
-    for (unsigned i = 0; i < m_abstr.size(); ++i) g->assert_expr(m_abstr.get(i));
-    for (unsigned i = 0; i < m_ackrs.size(); ++i) g->assert_expr(m_ackrs.get(i));
+    for (expr* a : m_abstr) 
+        g->assert_expr(a);
+    for (expr* a : m_ackrs) 
+        g->assert_expr(a);
     return true;
 }
 
 bool lackr::init() {
-    SASSERT(!m_is_init);    
-    params_ref simp_p(m_p);
-    m_simp.updt_params(simp_p);
-    m_info = alloc(ackr_info, m_m);
-    if (!collect_terms()) return false;
-    abstract();
-    m_is_init = true;
+    if (!m_is_init) {
+        params_ref simp_p(m_p);
+        m_simp.updt_params(simp_p);
+        m_info = alloc(ackr_info, m);
+        if (!collect_terms()) 
+            return false;
+        abstract();
+        m_is_init = true;
+    }
     return true;
 }
 
@@ -89,38 +100,38 @@ bool lackr::init() {
 // Introduce ackermann lemma for the two given terms.
 //
 bool lackr::ackr(app * const t1, app * const t2) {
-    TRACE("ackermannize", tout << "ackr "
-            << mk_ismt2_pp(t1, m_m, 2) << " , " << mk_ismt2_pp(t2, m_m, 2) << "\n";);
+    TRACE("ackermannize", tout << "ackr " << mk_ismt2_pp(t1, m, 2) << " , " << mk_ismt2_pp(t2, m, 2) << "\n";);
     const unsigned sz = t1->get_num_args();
     SASSERT(t2->get_num_args() == sz);
-    expr_ref_vector eqs(m_m);
+    expr_ref_vector eqs(m);
     for (unsigned i = 0; i < sz; ++i) {
         expr * const arg1 = t1->get_arg(i);
         expr * const arg2 = t2->get_arg(i);
-        if (m_m.are_equal(arg1, arg2)) continue; // quickly skip syntactically equal
-        if (m_m.are_distinct(arg1, arg2)){ // quickly abort if there are two distinct (e.g. numerals)                    
+        if (m.are_equal(arg1, arg2)) continue; // quickly skip syntactically equal
+        if (m.are_distinct(arg1, arg2)){ // quickly abort if there are two distinct (e.g. numerals)                    
             TRACE("ackermannize", tout << "never eq\n";);
             return false;
         }
-        eqs.push_back(m_m.mk_eq(arg1, arg2));
+        eqs.push_back(m.mk_eq(arg1, arg2));
     }
     app * const a1 = m_info->get_abstr(t1);
     app * const a2 = m_info->get_abstr(t2);
     SASSERT(a1 && a2);
-    TRACE("ackermannize", tout << "abstr1 " << mk_ismt2_pp(a1, m_m, 2) << "\n";);
-    TRACE("ackermannize", tout << "abstr2 " << mk_ismt2_pp(a2, m_m, 2) << "\n";);
-    expr_ref lhs(m_m);
-    lhs = (eqs.size() == 1) ? eqs.get(0) : m_m.mk_and(eqs.size(), eqs.c_ptr());
-    TRACE("ackermannize", tout << "ackr constr lhs" << mk_ismt2_pp(lhs, m_m, 2) << "\n";);
-    expr_ref rhs(m_m.mk_eq(a1, a2),m_m);
-    TRACE("ackermannize", tout << "ackr constr rhs" << mk_ismt2_pp(rhs, m_m, 2) << "\n";);
-    expr_ref cg(m_m.mk_implies(lhs, rhs), m_m);
-    TRACE("ackermannize", tout << "ackr constr" << mk_ismt2_pp(cg, m_m, 2) << "\n";);
-    expr_ref cga(m_m);
-    m_info->abstract(cg, cga); // constraint needs abstraction due to nested applications
+    expr_ref lhs = mk_and(eqs);
+    expr_ref rhs(m.mk_eq(a1, a2),m);
+    expr_ref cg(m.mk_implies(lhs, rhs), m);
+    expr_ref cga = m_info->abstract(cg); // constraint needs abstraction due to nested applications
     m_simp(cga);
-    TRACE("ackermannize", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";);
-    if (m_m.is_true(cga)) return false;
+    TRACE("ackermannize", 
+          tout << "abstr1 " << mk_ismt2_pp(a1, m, 2) << "\n";
+          tout << "abstr2 " << mk_ismt2_pp(a2, m, 2) << "\n";
+          tout << "ackr constr lhs" << mk_ismt2_pp(lhs, m, 2) << "\n";
+          tout << "ackr constr rhs" << mk_ismt2_pp(rhs, m, 2) << "\n";
+          tout << "ackr constr" << mk_ismt2_pp(cg, m, 2) << "\n";
+          tout << "ackr constr abs:" << mk_ismt2_pp(cga, m, 2) << "\n";);
+    if (m.is_true(cga)) {
+        return false;
+    }
     m_st.m_ackrs_sz++;
     m_ackrs.push_back(std::move(cga));
     return true;
@@ -130,22 +141,27 @@ bool lackr::ackr(app * const t1, app * const t2) {
 // Introduce the ackermann lemma for each pair of terms.
 //
 void lackr::eager_enc() {
-    TRACE("ackermannize", tout << "#funs: " << m_fun2terms.size() << std::endl;);
+    TRACE("ackermannize", tout << "#funs: " << m_fun2terms.size() << "#sels: " << m_sel2terms.size() << std::endl;);
     for (auto const& kv : m_fun2terms) {
         checkpoint();
-        app_set * const  ts = kv.get_value();
-        const app_set::iterator r = ts->end();
-        for (app_set::iterator j = ts->begin(); j != r; ++j) {
-            app_set::iterator k = j;
-            ++k;
-            for (;  k != r; ++k) {
-                app * const t1 = *j;
-                app * const t2 = *k;
-                SASSERT(t1->get_decl() == kv.m_key);
-                SASSERT(t2->get_decl() == kv.m_key);
-                if (t1 != t2) {
-                    ackr(t1,t2);
-                }
+        ackr(kv.get_value());
+    }
+    for (auto const& kv : m_sel2terms) {
+        checkpoint();
+        ackr(kv.get_value());
+    }
+}
+
+void lackr::ackr(app_set const* ts) {
+    const app_set::iterator r = ts->end();
+    for (app_set::iterator j = ts->begin(); j != r; ++j) {
+        app * const t1 = *j;
+        app_set::iterator k = j;
+        ++k;
+        for (; k != r; ++k) {
+            app * const t2 = *k;
+            if (t1 != t2) {
+                ackr(t1, t2);
             }
         }
     }
@@ -154,46 +170,57 @@ void lackr::eager_enc() {
 
 void lackr::abstract() {
     for (auto const& kv : m_fun2terms) {
-        func_decl* const fd = kv.m_key;
-        app_set * const ts = kv.get_value();
-        sort* const s = fd->get_range();
-        for (app * t : (*ts)) {
-            app * const fc = m_m.mk_fresh_const(fd->get_name().str().c_str(), s);
+        func_decl* fd = kv.m_key;
+        for (app * t : *kv.m_value) {
+            app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t));
             SASSERT(t->get_decl() == fd);
             m_info->set_abstr(t, fc);
-            TRACE("ackermannize", tout << "abstr term "
-                    << mk_ismt2_pp(t, m_m, 2)
-                    << " -> "
-                    << mk_ismt2_pp(fc, m_m, 2)
-                    << "\n";);
+        }
+    }
+
+    for (auto& kv : m_sel2terms) {
+        func_decl * fd = kv.m_key->get_decl();
+        for (app * t : *kv.m_value) {
+            app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t));
+            m_info->set_abstr(t, fc);
         }
     }
     m_info->seal();
     // perform abstraction of the formulas
     for (expr * f : m_formulas) {
-        expr_ref a(m_m);
-        m_info->abstract(f, a);
+        expr_ref a = m_info->abstract(f);
         m_abstr.push_back(std::move(a));
     }
 }
 
 void lackr::add_term(app* a) {
-    if (a->get_num_args() == 0) return;
-    if (!m_ackr_helper.should_ackermannize(a)) return;
-    func_decl* const fd = a->get_decl();
     app_set* ts = nullptr;
-    if (!m_fun2terms.find(fd, ts)) {
-        ts = alloc(app_set);
-        m_fun2terms.insert(fd, ts);
+    if (a->get_num_args() == 0) 
+        return;
+    if (m_ackr_helper.is_select(a)) {
+        app* sel = to_app(a->get_arg(0));
+        if (!m_sel2terms.find(sel, ts)) {
+            ts = alloc(app_set);
+            m_sel2terms.insert(sel, ts);
+        }
+    }
+    else if (m_ackr_helper.is_uninterp_fn(a)) {
+        func_decl* const fd = a->get_decl();
+        if (!m_fun2terms.find(fd, ts)) {
+            ts = alloc(app_set);
+            m_fun2terms.insert(fd, ts);
+        }
     }
-    TRACE("ackermannize", tout << "term(" << mk_ismt2_pp(a, m_m, 2) << ")\n";);
+    else {
+        return;
+    }
+    TRACE("ackermannize", tout << "term(" << mk_ismt2_pp(a, m, 2) << ")\n";);
     ts->insert(a);
 }
 
 void  lackr::push_abstraction() {
-    const unsigned sz = m_abstr.size();
-    for (unsigned i = 0; i < sz; ++i) {
-        m_sat->assert_expr(m_abstr.get(i));
+    for (expr* a : m_abstr) {
+        m_solver->assert_expr(a);
     }
 }
 
@@ -201,42 +228,41 @@ lbool lackr::eager() {
     SASSERT(m_is_init);
     push_abstraction();
     TRACE("ackermannize", tout << "run sat 0\n"; );
-    const lbool rv0 = m_sat->check_sat(0, nullptr);
-    if (rv0 == l_false) return l_false;
+    lbool rv0 = m_solver->check_sat(0, nullptr);
+    if (rv0 == l_false) {
+        return l_false;
+    }
     eager_enc();
-    expr_ref all(m_m);
-    all = m_m.mk_and(m_ackrs.size(), m_ackrs.c_ptr());
+    expr_ref all = mk_and(m_ackrs);
     m_simp(all);
-    m_sat->assert_expr(all);
+    m_solver->assert_expr(all);
     TRACE("ackermannize", tout << "run sat all\n"; );
-    return m_sat->check_sat(0, nullptr);
+    return m_solver->check_sat(0, nullptr);
 }
 
 lbool lackr::lazy() {
     SASSERT(m_is_init);
-    lackr_model_constructor mc(m_m, m_info);
+    lackr_model_constructor mc(m, m_info);
     push_abstraction();
     unsigned ackr_head = 0;
     while (true) {
         m_st.m_it++;
         checkpoint();
         TRACE("ackermannize", tout << "lazy check: " << m_st.m_it << "\n";);
-        const lbool r = m_sat->check_sat(0, nullptr);
+        const lbool r = m_solver->check_sat(0, nullptr);
         if (r == l_undef) return l_undef; // give up
         if (r == l_false) return l_false; // abstraction unsat
         // reconstruct model
         model_ref am;
-        m_sat->get_model(am);
+        m_solver->get_model(am);
         const bool mc_res = mc.check(am);
         if (mc_res) return l_true; // model okay
         // refine abstraction
-        const lackr_model_constructor::conflict_list conflicts = mc.get_conflicts();
-        for (lackr_model_constructor::conflict_list::const_iterator i = conflicts.begin();
-             i != conflicts.end(); ++i) {
-            ackr(i->first, i->second);
+        for (auto const& kv : mc.get_conflicts()) {
+            ackr(kv.first, kv.second);
         }
         while (ackr_head < m_ackrs.size()) {
-            m_sat->assert_expr(m_ackrs.get(ackr_head++));
+            m_solver->assert_expr(m_ackrs.get(ackr_head++));
         }
     }
 }
@@ -246,16 +272,14 @@ lbool lackr::lazy() {
 //
 bool lackr::collect_terms() {
     ptr_vector<expr> stack = m_formulas;
-    expr *           curr;
     expr_mark        visited;
 
     while (!stack.empty()) {
-        curr = stack.back();
+        expr * curr = stack.back();
         if (visited.is_marked(curr)) {
             stack.pop_back();
             continue;
         }
-
         switch (curr->get_kind()) {
             case AST_VAR:
                 visited.mark(curr, true);
@@ -266,8 +290,9 @@ bool lackr::collect_terms() {
                 if (for_each_expr_args(stack, visited, a->get_num_args(), a->get_args())) {
                     visited.mark(curr, true);
                     stack.pop_back();
+                    m_ackr_helper.mark_non_select(a, m_non_select);
                     add_term(a);
-                }
+                }                
                 break;
             }
             case AST_QUANTIFIER:
@@ -277,5 +302,8 @@ bool lackr::collect_terms() {
                 return false;
         }
     }
+
+    m_ackr_helper.prune_non_select(m_sel2terms, m_non_select);
+    
     return true;
 }
diff --git a/src/ackermannization/lackr.h b/src/ackermannization/lackr.h
index 19d4e35d85d..f6d77fc85ed 100644
--- a/src/ackermannization/lackr.h
+++ b/src/ackermannization/lackr.h
@@ -17,16 +17,16 @@
 #ifndef LACKR_H_
 #define LACKR_H_
 
-#include "ackermannization/ackr_info.h"
-#include "ackermannization/ackr_helper.h"
+#include "util/lbool.h"
+#include "util/util.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/bv_decl_plugin.h"
-#include "util/lbool.h"
 #include "model/model.h"
 #include "solver/solver.h"
-#include "util/util.h"
 #include "tactic/tactic_exception.h"
 #include "tactic/goal.h"
+#include "ackermannization/ackr_info.h"
+#include "ackermannization/ackr_helper.h"
 
 struct lackr_stats {
     lackr_stats() : m_it(0), m_ackrs_sz(0) {}
@@ -71,25 +71,29 @@ class lackr {
         //  timeout mechanism
         //
         void checkpoint() {
-            if (m_m.canceled()) {
+            if (m.canceled()) {
                 throw tactic_exception(TACTIC_CANCELED_MSG);
             }
         }
     private:
         typedef ackr_helper::fun2terms_map fun2terms_map;
+        typedef ackr_helper::sel2terms_map sel2terms_map;
         typedef ackr_helper::app_set       app_set;
-        ast_manager&                         m_m;
+        ast_manager&                         m;
         params_ref                           m_p;
         const ptr_vector<expr>&              m_formulas;
+        array_util                           m_autil;
         expr_ref_vector                      m_abstr;
         fun2terms_map                        m_fun2terms;
+        sel2terms_map                        m_sel2terms;
         ackr_info_ref                        m_info;
-        solver*                              m_sat;
+        solver*                              m_solver;
         ackr_helper                          m_ackr_helper;
         th_rewriter                          m_simp;
         expr_ref_vector                      m_ackrs;
         model_ref                            m_model;
         bool                                 m_eager;
+        expr_mark                            m_non_select;
         lackr_stats&                         m_st;
         bool                                 m_is_init;
 
@@ -102,6 +106,8 @@ class lackr {
         //
         bool ackr(app * t1, app * t2);
 
+        void ackr(app_set const* ts);
+
         //
         // Introduce the ackermann lemma for each pair of terms.
         //
diff --git a/src/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp
index f24a53cdbe6..ac5a5cb3baf 100644
--- a/src/ackermannization/lackr_model_constructor.cpp
+++ b/src/ackermannization/lackr_model_constructor.cpp
@@ -23,346 +23,328 @@
 #include "ast/rewriter/bool_rewriter.h"
 
 struct lackr_model_constructor::imp {
-    public:
-        imp(ast_manager & m,
-            ackr_info_ref info,
-            model_ref & abstr_model,
-            conflict_list & conflicts)
-            : m_m(m)
-            , m_info(info)
-            , m_abstr_model(abstr_model)
-            , m_conflicts(conflicts)
-            , m_b_rw(m)
-            , m_bv_rw(m)
-            , m_evaluator(nullptr)
-            , m_empty_model(m)
-            , m_ackr_helper(m)
-        {}
-
-        ~imp() {
-            if (m_evaluator) dealloc(m_evaluator);
-            {
-                values2val_t::iterator i = m_values2val.begin();
-                const values2val_t::iterator e = m_values2val.end();
-                for (; i != e; ++i) {
-                    m_m.dec_ref(i->m_key);
-                    m_m.dec_ref(i->m_value.value);
-                    m_m.dec_ref(i->m_value.source_term);
-                }
-            }
-            {
-                app2val_t::iterator i = m_app2val.begin();
-                const app2val_t::iterator e = m_app2val.end();
-                for (; i != e; ++i) {
-                    m_m.dec_ref(i->m_value);
-                    m_m.dec_ref(i->m_key);
-                }
-            }
+public:
+    imp(ast_manager & m,
+        ackr_info_ref info,
+        model_ref & abstr_model,
+        conflict_list & conflicts)
+        : m(m)
+        , m_info(info)
+        , m_abstr_model(abstr_model)
+        , m_conflicts(conflicts)
+        , m_pinned(m)
+        , m_b_rw(m)
+        , m_bv_rw(m)
+        , m_evaluator(nullptr)
+        , m_empty_model(m)
+        , m_ackr_helper(m)
+    {}
+    
+    ~imp() { }
+    
+    //
+    // Returns true iff model was successfully constructed.
+    // Conflicts are saved as a side effect.
+    //
+    bool check() {
+        bool retv = true;
+        for (unsigned i = 0; i < m_abstr_model->get_num_constants(); i++) {
+            func_decl * const c = m_abstr_model->get_constant(i);
+            app * const  _term = m_info->find_term(c);
+            expr * const term  = _term ? _term : m.mk_const(c);
+            if (!check_term(term)) retv = false;
         }
-
-        //
-        // Returns true iff model was successfully constructed.
-        // Conflicts are saved as a side effect.
-        //
-        bool check() {
-            bool retv = true;
-            for (unsigned i = 0; i < m_abstr_model->get_num_constants(); i++) {
-                func_decl * const c = m_abstr_model->get_constant(i);
-                app * const  _term = m_info->find_term(c);
-                expr * const term  = _term ? _term : m_m.mk_const(c);
-                if (!check_term(term)) retv = false;
-            }
-            return retv;
+        return retv;
+    }
+    
+    
+    void make_model(model_ref& destination) {
+        for (unsigned i = 0; i < m_abstr_model->get_num_uninterpreted_sorts(); i++) {
+            sort * const s = m_abstr_model->get_uninterpreted_sort(i);
+            ptr_vector<expr> u = m_abstr_model->get_universe(s);
+            destination->register_usort(s, u.size(), u.c_ptr());
         }
-
-
-        void make_model(model_ref& destination) {
-            {
-                for (unsigned i = 0; i < m_abstr_model->get_num_uninterpreted_sorts(); i++) {
-                    sort * const s = m_abstr_model->get_uninterpreted_sort(i);
-                    ptr_vector<expr> u = m_abstr_model->get_universe(s);
-                    destination->register_usort(s, u.size(), u.c_ptr());
-                }
-            }
-            for (unsigned i = 0; i < m_abstr_model->get_num_functions(); i++) {
-                func_decl * const fd = m_abstr_model->get_function(i);
-                func_interp * const fi = m_abstr_model->get_func_interp(fd);
-                destination->register_decl(fd, fi);
-            }
-
-            {
-                const app2val_t::iterator e = m_app2val.end();
-                app2val_t::iterator i = m_app2val.end();
-                for (; i != e; ++i) {
-                    app * a = i->m_key;
-                    if (a->get_num_args()) continue;
-                    destination->register_decl(a->get_decl(), i->m_value);
-                }
-            }
-
-            obj_map<func_decl, func_interp*> interpretations;
-            {
-                const values2val_t::iterator e = m_values2val.end();
-                values2val_t::iterator i = m_values2val.end();
-                for (; i != e; ++i) add_entry(i->m_key, i->m_value.value, interpretations);
-            }
-
-            {
-                obj_map<func_decl, func_interp*>::iterator ie = interpretations.end();
-                obj_map<func_decl, func_interp*>::iterator ii = interpretations.begin();
-                for (; ii != ie; ++ii) {
-                    func_decl* const fd = ii->m_key;
-                    func_interp* const fi = ii->get_value();
-                    fi->set_else(m_m.get_some_value(fd->get_range()));
-                    destination->register_decl(fd, fi);
-                }
-            }
+        
+        for (unsigned i = 0; i < m_abstr_model->get_num_functions(); i++) {
+            func_decl * const fd = m_abstr_model->get_function(i);
+            func_interp * const fi = m_abstr_model->get_func_interp(fd);
+            destination->register_decl(fd, fi);
         }
-
-        void add_entry(app* term, expr* value,
-            obj_map<func_decl, func_interp*>& interpretations) {
-            func_interp* fi = nullptr;
-            func_decl * const declaration = term->get_decl();
-            const unsigned sz = declaration->get_arity();
-            SASSERT(sz == term->get_num_args());
-            if (!interpretations.find(declaration, fi)) {
-                fi = alloc(func_interp, m_m, sz);
-                interpretations.insert(declaration, fi);
-            }
-            fi->insert_new_entry(term->get_args(), value);
+        
+        for (auto & kv : m_app2val) {
+            app * a = kv.m_key;
+            if (a->get_num_args() == 0) 
+                destination->register_decl(a->get_decl(), kv.m_value);
         }
-    private:
-        ast_manager&                    m_m;
-        ackr_info_ref                   m_info;
-        model_ref&                      m_abstr_model;
-        conflict_list&                  m_conflicts;
-        bool_rewriter                   m_b_rw;
-        bv_rewriter                     m_bv_rw;
-        model_evaluator *               m_evaluator;
-        model                           m_empty_model;
-    private:
-        struct val_info { expr * value; app * source_term; };
-        typedef obj_map<app, expr *> app2val_t;
-        typedef obj_map<app, val_info> values2val_t;
-        values2val_t     m_values2val;
-        app2val_t        m_app2val;
-        ptr_vector<expr> m_stack;
-        ackr_helper      m_ackr_helper;
-        expr_mark        m_visited;
-
-        static inline val_info mk_val_info(expr* value, app* source_term) {
-            val_info rv;
-            rv.value = value;
-            rv.source_term = source_term;
-            return rv;
+        
+        obj_map<func_decl, func_interp*> interpretations;
+        for (auto & kv : m_values2val) {
+            add_entry(kv.m_key, kv.m_value.value, interpretations);
         }
-
-        // Performs congruence check on a given term.
-        bool check_term(expr * term) {
-            m_stack.push_back(term);
-            const bool rv = _check_stack();
-            m_stack.reset();
-            return rv;
+        
+        for (auto & kv : interpretations) {
+            func_decl* const fd = kv.m_key;
+            func_interp* const fi = kv.get_value();
+            fi->set_else(m.get_some_value(fd->get_range()));
+            destination->register_decl(fd, fi);
         }
-
-        // Performs congruence check on terms on the stack.
-        // Stops upon the first failure.
-        // Returns true if and only if all congruence checks succeeded.
-        bool _check_stack() {
-            if (m_evaluator == nullptr) m_evaluator = alloc(model_evaluator, m_empty_model);
-            expr *  curr;
-            while (!m_stack.empty()) {
-                curr = m_stack.back();
-                if (m_visited.is_marked(curr)) {
-                    m_stack.pop_back();
-                    continue;
-                }
-
-                switch (curr->get_kind()) {
-                    case AST_VAR:
-                        UNREACHABLE();
-                        return false;
-                    case AST_APP: {
-                            app * a = to_app(curr);
-                            if (for_each_expr_args(m_stack, m_visited, a->get_num_args(), a->get_args())) {
-                                m_visited.mark(a, true);
-                                m_stack.pop_back();
-                                if (!mk_value(a)) return false;
-                            }
-                    }
-                        break;
-                    case AST_QUANTIFIER:
-                        UNREACHABLE();
-                        return false;
-                    default:
-                        UNREACHABLE();
-                        return false;
-                }
-            }
-            return true;
+    }
+    
+    void add_entry(app* term, expr* value,
+                   obj_map<func_decl, func_interp*>& interpretations) {
+        func_interp* fi = nullptr;
+        func_decl * const declaration = term->get_decl();
+        const unsigned sz = declaration->get_arity();
+        SASSERT(sz == term->get_num_args());
+        if (!interpretations.find(declaration, fi)) {
+            fi = alloc(func_interp, m, sz);
+            interpretations.insert(declaration, fi);
         }
-
-        inline bool is_val(expr * e) { return m_m.is_value(e); }
-
-        inline bool eval_cached(app * a, expr *& val) {
-            if (is_val(a)) { val = a; return true; }
-            return m_app2val.find(a, val);
+        fi->insert_new_entry(term->get_args(), value);
+    }
+private:
+    ast_manager&                    m;    
+    ackr_info_ref                   m_info;
+    model_ref&                      m_abstr_model;
+    conflict_list&                  m_conflicts;
+    ast_ref_vector                  m_pinned;
+    bool_rewriter                   m_b_rw;
+    bv_rewriter                     m_bv_rw;
+    scoped_ptr<model_evaluator>     m_evaluator;
+    model                           m_empty_model;
+private:
+    struct val_info { expr * value; app * source_term; };
+    typedef obj_map<app, expr *> app2val_t;
+    typedef obj_map<app, val_info> values2val_t;
+    values2val_t     m_values2val;
+    app2val_t        m_app2val;
+    ptr_vector<expr> m_stack;
+    ackr_helper      m_ackr_helper;
+    expr_mark        m_visited;
+    
+    static inline val_info mk_val_info(expr* value, app* source_term) {
+        val_info rv;
+        rv.value = value;
+        rv.source_term = source_term;
+        return rv;
+    }
+    
+    // Performs congruence check on a given term.
+    bool check_term(expr * term) {
+        m_stack.push_back(term);
+        const bool rv = _check_stack();
+        m_stack.reset();
+        return rv;
+    }
+    
+    // Performs congruence check on terms on the stack.
+    // Stops upon the first failure.
+    // Returns true if and only if all congruence checks succeeded.
+    bool _check_stack() {
+        if (!m_evaluator) {
+            m_evaluator = alloc(model_evaluator, m_empty_model);
         }
-
-        bool evaluate(app * const a, expr_ref& result) {
-            SASSERT(!is_val(a));
-            const unsigned num = a->get_num_args();
-            if (num == 0) { // handle constants
-                make_value_constant(a, result);
-                return true;
+        expr *  curr;
+        while (!m_stack.empty()) {
+            curr = m_stack.back();
+            if (m_visited.is_marked(curr)) {
+                m_stack.pop_back();
+                continue;
             }
-            // evaluate arguments
-            expr_ref_vector values(m_m);
-            values.reserve(num);
-            expr * const * args = a->get_args();
-            for (unsigned i = 0; i < num; ++i) {
-                expr * val;
-                const bool b = eval_cached(to_app(args[i]), val); // TODO: OK conversion to_app?
-                CTRACE("model_constructor", m_conflicts.empty() && !b, tout << "fail arg val(\n" << mk_ismt2_pp(args[i], m_m, 2) << '\n'; );
-                if (!b) {
-                    // bailing out because args eval failed previously
-                    return false;
-                }
-                TRACE("model_constructor", tout <<
-                    "arg val " << i << "(\n" << mk_ismt2_pp(args[i], m_m, 2)
-                    << " : " << mk_ismt2_pp(val, m_m, 2) << '\n'; );
-                SASSERT(b);
-                values[i] = val;
-            }
-            // handle functions
-            if (m_ackr_helper.should_ackermannize(a)) { // handle uninterpreted
-                app_ref key(m_m.mk_app(a->get_decl(), values.c_ptr()), m_m);
-                if (!make_value_uninterpreted_function(a, key.get(), result)) {
-                    return false;
+            
+            switch (curr->get_kind()) {
+            case AST_VAR:
+                UNREACHABLE();
+                return false;
+            case AST_APP: {
+                app * a = to_app(curr);
+                if (for_each_expr_args(m_stack, m_visited, a->get_num_args(), a->get_args())) {
+                    m_visited.mark(a, true);
+                    m_stack.pop_back();
+                    if (!mk_value(a)) return false;
                 }
+                break;
             }
-            else { // handle interpreted
-                make_value_interpreted_function(a, values, result);
+            case AST_QUANTIFIER:
+                UNREACHABLE();
+                return false;
+            default:
+                UNREACHABLE();
+                return false;
             }
-            return true;
         }
-
-        //
-        // Check and record the value for a given term, given that all arguments are already checked.
-        //
-        bool mk_value(app * a) {
-            if (is_val(a)) return true; // skip numerals
-            TRACE("model_constructor", tout << "mk_value(\n" << mk_ismt2_pp(a, m_m, 2) << ")\n";);
-            SASSERT(!m_app2val.contains(a));
-            expr_ref result(m_m);
-            if (!evaluate(a, result)) return false;
-            SASSERT(is_val(result));
-            TRACE("model_constructor",
-                tout << "map term(\n" << mk_ismt2_pp(a, m_m, 2) << "\n->"
-                << mk_ismt2_pp(result.get(), m_m, 2)<< ")\n"; );
-            CTRACE("model_constructor",
-                !is_val(result.get()),
-                tout << "eval fail\n" << mk_ismt2_pp(a, m_m, 2) << mk_ismt2_pp(result, m_m, 2) << "\n";
-            );
-            SASSERT(is_val(result.get()));
-            m_app2val.insert(a, result.get()); // memoize
-            m_m.inc_ref(a);
-            m_m.inc_ref(result.get());
+        return true;
+    }
+    
+    inline bool is_val(expr * e) { return m.is_value(e); }
+    
+    inline bool eval_cached(app * a, expr *& val) {
+        if (is_val(a)) { 
+            val = a; 
+            return true; 
+        }
+        return m_app2val.find(a, val);
+    }
+    
+    bool evaluate(app * const a, expr_ref& result) {
+        SASSERT(!is_val(a));
+        const unsigned num = a->get_num_args();
+        if (num == 0) { // handle constants
+            make_value_constant(a, result);
             return true;
         }
-
-        // Constants from the abstract model are directly mapped to the concrete one.
-        void make_value_constant(app * const a, expr_ref& result) {
-            SASSERT(a->get_num_args() == 0);
-            func_decl * const fd = a->get_decl();
-            expr * val = m_abstr_model->get_const_interp(fd);
-            if (val == nullptr) { // TODO: avoid model completion?
-                sort * s = fd->get_range();
-                val = m_abstr_model->get_some_value(s);
+        // evaluate arguments
+        expr_ref_vector values(m);
+        values.reserve(num);
+        expr * const * args = a->get_args();
+        for (unsigned i = 0; i < num; ++i) {
+            expr * val = nullptr;
+            const bool b = eval_cached(to_app(args[i]), val); // TODO: OK conversion to_app?
+            CTRACE("model_constructor", m_conflicts.empty() && !b, tout << "fail arg val(\n" << mk_ismt2_pp(args[i], m, 2) << '\n'; );
+            if (!b) {
+                // bailing out because args eval failed previously
+                return false;
             }
-            result = val;
+            TRACE("model_constructor", tout <<
+                  "arg val " << i << "(\n" << mk_ismt2_pp(args[i], m, 2)
+                  << " : " << mk_ismt2_pp(val, m, 2) << '\n'; );
+            SASSERT(b);
+            values[i] = val;
         }
-
-        bool make_value_uninterpreted_function(app* a,
-                app* key,
-                expr_ref& result) {
-            // get ackermann constant
-            app * const ac = m_info->get_abstr(a);
-            func_decl * const a_fd = a->get_decl();
-            SASSERT(ac->get_num_args() == 0);
-            SASSERT(a_fd->get_range() == ac->get_decl()->get_range());
-            expr_ref value(m_m);
-            value = m_abstr_model->get_const_interp(ac->get_decl());
-            // get ackermann constant's interpretation
-            if (value.get() == nullptr) { // TODO: avoid model completion?
-                sort * s = a_fd->get_range();
-                value = m_abstr_model->get_some_value(s);
+        // handle functions
+        if (m_ackr_helper.is_uninterp_fn(a)) { // handle uninterpreted
+            app_ref key(m.mk_app(a->get_decl(), values.c_ptr()), m);
+            if (!make_value_uninterpreted_function(a, key.get(), result)) {
+                return false;
             }
-            // check congruence
-            val_info vi;
-            if(m_values2val.find(key,vi)) { // already is mapped to a value
-                SASSERT(vi.source_term);
-                const bool ok =  vi.value == value;
-                if (!ok) {
-                    TRACE("model_constructor",
-                        tout << "already mapped by(\n" << mk_ismt2_pp(vi.source_term, m_m, 2) << "\n->"
-                             << mk_ismt2_pp(vi.value, m_m, 2) << ")\n"; );
-                    m_conflicts.push_back(std::make_pair(a, vi.source_term));
-                }
-                result = vi.value;
-                return ok;
-            } else {                        // new value
-                result = value;
-                vi.value = value;
-                vi.source_term = a;
-                m_values2val.insert(key,vi);
-                m_m.inc_ref(vi.source_term);
-                m_m.inc_ref(vi.value);
-                m_m.inc_ref(key);
-                return true;
+        }
+        else if (m_ackr_helper.is_select(a)) {
+            // fail on select terms
+            return false;
+        }
+        else { // handle interpreted
+            make_value_interpreted_function(a, values, result);
+        }
+        return true;
+    }
+    
+    //
+    // Check and record the value for a given term, given that all arguments are already checked.
+    //
+    bool mk_value(app * a) {
+        if (is_val(a)) return true; // skip numerals
+        TRACE("model_constructor", tout << "mk_value(\n" << mk_ismt2_pp(a, m, 2) << ")\n";);
+        SASSERT(!m_app2val.contains(a));
+        expr_ref result(m);
+        if (!evaluate(a, result)) return false;
+        SASSERT(is_val(result));
+        TRACE("model_constructor",
+              tout << "map term(\n" << mk_ismt2_pp(a, m, 2) << "\n->"
+              << mk_ismt2_pp(result.get(), m, 2)<< ")\n"; );
+        CTRACE("model_constructor",
+               !is_val(result.get()),
+               tout << "eval fail\n" << mk_ismt2_pp(a, m, 2) << mk_ismt2_pp(result, m, 2) << "\n";
+               );
+        SASSERT(is_val(result.get()));
+        m_app2val.insert(a, result.get()); // memoize
+        m_pinned.push_back(a);
+        m_pinned.push_back(result);
+        return true;
+    }
+    
+    // Constants from the abstract model are directly mapped to the concrete one.
+    void make_value_constant(app * const a, expr_ref& result) {
+        SASSERT(a->get_num_args() == 0);
+        func_decl * const fd = a->get_decl();
+        expr * val = m_abstr_model->get_const_interp(fd);
+        if (val == nullptr) { // TODO: avoid model completion?
+            sort * s = fd->get_range();
+            val = m_abstr_model->get_some_value(s);
+        }
+        result = val;
+    }
+    
+    bool make_value_uninterpreted_function(app* a,
+                                           app* key,
+                                           expr_ref& result) {
+        // get ackermann constant
+        app * const ac = m_info->get_abstr(a);
+        func_decl * const a_fd = a->get_decl();
+        SASSERT(ac->get_num_args() == 0);
+        SASSERT(a_fd->get_range() == ac->get_decl()->get_range());
+        expr_ref value(m);
+        value = m_abstr_model->get_const_interp(ac->get_decl());
+        // get ackermann constant's interpretation
+        if (value.get() == nullptr) { // TODO: avoid model completion?
+            sort * s = a_fd->get_range();
+            value = m_abstr_model->get_some_value(s);
+        }
+        // check congruence
+        val_info vi;
+        if(m_values2val.find(key,vi)) { // already is mapped to a value
+            SASSERT(vi.source_term);
+            const bool ok =  vi.value == value;
+            if (!ok) {
+                TRACE("model_constructor",
+                      tout << "already mapped by(\n" << mk_ismt2_pp(vi.source_term, m, 2) << "\n->"
+                      << mk_ismt2_pp(vi.value, m, 2) << ")\n"; );
+                m_conflicts.push_back(std::make_pair(a, vi.source_term));
             }
-            UNREACHABLE();
+            result = vi.value;
+            return ok;
+        } 
+        else {                        // new value
+            result = value;
+            vi.value = value;
+            vi.source_term = a;
+            m_values2val.insert(key,vi);
+            m_pinned.push_back(vi.source_term);
+            m_pinned.push_back(vi.value);
+            m_pinned.push_back(key);
             return true;
         }
+        UNREACHABLE();
+        return true;
+    }
     
-        void make_value_interpreted_function(app* a,
-                expr_ref_vector& values,
-                expr_ref& result) {
-            const unsigned num = values.size();
-            func_decl * const fd = a->get_decl();
-            const family_id fid = fd->get_family_id();
-            expr_ref term(m_m);
-            term = m_m.mk_app(a->get_decl(), num, values.c_ptr());
-            m_evaluator->operator() (term, result);
-            TRACE("model_constructor",
-                tout << "eval(\n" << mk_ismt2_pp(term.get(), m_m, 2) << "\n->"
-                << mk_ismt2_pp(result.get(), m_m, 2) << ")\n"; );
-            return;
-            if (fid == m_b_rw.get_fid()) {
-                decl_kind k = fd->get_decl_kind();
-                if (k == OP_EQ) {
-                    // theory dispatch for =
-                    SASSERT(num == 2);
-                    family_id s_fid = m_m.get_sort(values.get(0))->get_family_id();
-                    if (s_fid == m_bv_rw.get_fid())
-                        m_bv_rw.mk_eq_core(values.get(0), values.get(1), result);
-                } else {
-                    m_b_rw.mk_app_core(fd, num, values.c_ptr(), result);
-                }
+    void make_value_interpreted_function(app* a,
+                                         expr_ref_vector& values,
+                                         expr_ref& result) {
+        const unsigned num = values.size();
+        func_decl * const fd = a->get_decl();
+        const family_id fid = fd->get_family_id();
+        expr_ref term(m);
+        term = m.mk_app(a->get_decl(), num, values.c_ptr());
+        m_evaluator->operator() (term, result);
+        TRACE("model_constructor",
+              tout << "eval(\n" << mk_ismt2_pp(term.get(), m, 2) << "\n->"
+              << mk_ismt2_pp(result.get(), m, 2) << ")\n"; );
+        return;
+        if (fid == m_b_rw.get_fid()) {
+            decl_kind k = fd->get_decl_kind();
+            if (k == OP_EQ) {
+                // theory dispatch for =
+                SASSERT(num == 2);
+                family_id s_fid = m.get_sort(values.get(0))->get_family_id();
+                if (s_fid == m_bv_rw.get_fid())
+                    m_bv_rw.mk_eq_core(values.get(0), values.get(1), result);
             } else {
-                if (fid == m_bv_rw.get_fid()) {
-                    m_bv_rw.mk_app_core(fd, num, values.c_ptr(), result);
-                }
-                else {
-                    UNREACHABLE();
-                }
+                m_b_rw.mk_app_core(fd, num, values.c_ptr(), result);
+            }
+        } else {
+            if (fid == m_bv_rw.get_fid()) {
+                m_bv_rw.mk_app_core(fd, num, values.c_ptr(), result);
+            }
+            else {
+                UNREACHABLE();
             }
         }
+    }
 };
 
 lackr_model_constructor::lackr_model_constructor(ast_manager& m, ackr_info_ref info)
     : m_imp(nullptr)
-    , m_m(m)
+    , m(m)
     , m_state(UNKNOWN)
     , m_info(info)
     , m_ref_count(0)
@@ -375,7 +357,7 @@ lackr_model_constructor::~lackr_model_constructor() {
 bool lackr_model_constructor::check(model_ref& abstr_model) {
     m_conflicts.reset();
     dealloc(m_imp);
-    m_imp = alloc(lackr_model_constructor::imp, m_m, m_info, abstr_model, m_conflicts);
+    m_imp = alloc(lackr_model_constructor::imp, m, m_info, abstr_model, m_conflicts);
     const bool rv = m_imp->check();
     m_state = rv ? CHECKED : CONFLICT;
     return rv;
diff --git a/src/ackermannization/lackr_model_constructor.h b/src/ackermannization/lackr_model_constructor.h
index d5847a24cb5..928d0c992ec 100644
--- a/src/ackermannization/lackr_model_constructor.h
+++ b/src/ackermannization/lackr_model_constructor.h
@@ -49,7 +49,7 @@ class lackr_model_constructor {
     private:
         struct imp;
         imp * m_imp;
-        ast_manager &                      m_m;
+        ast_manager &                      m;
         enum {CHECKED, CONFLICT, UNKNOWN}  m_state;
         conflict_list                      m_conflicts;
         const ackr_info_ref                m_info;
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index db5c33e7942..4df0f90a4b8 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -1287,7 +1287,7 @@ public boolean isString()
      */
     public String getString()
     {
-        return Native.getString(getContext().nCtx(), getNativeObject());
+	return Native.getString(getContext().nCtx(), getNativeObject());
     }
 
     /**
diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h
index 6f229b30d6a..b63da8220c7 100644
--- a/src/ast/array_decl_plugin.h
+++ b/src/ast/array_decl_plugin.h
@@ -184,6 +184,13 @@ class array_util : public array_recognizers {
         return m_manager.mk_app(m_fid, OP_STORE, 0, nullptr, num_args, args);
     }
 
+    app * mk_store(expr_ref_vector const& args) {
+        return mk_store(args.size(), args.c_ptr());
+    }
+    app * mk_store(ptr_vector<expr> const& args) {
+        return mk_store(args.size(), args.c_ptr());
+    }
+
     app * mk_select(unsigned num_args, expr * const * args) {
         return m_manager.mk_app(m_fid, OP_SELECT, 0, nullptr, num_args, args);
     }
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 0ea8b7e9472..132113ff944 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1940,6 +1940,14 @@ class ast_manager {
         return mk_const(mk_fresh_func_decl(prefix, 0, nullptr, s, skolem)); 
     }
 
+    app * mk_fresh_const(std::string const& prefix, sort * s, bool skolem = true) { 
+        return mk_fresh_const(prefix.c_str(), s, skolem);        
+    }
+
+    app * mk_fresh_const(symbol const& prefix, sort * s, bool skolem = true) { 
+        return mk_fresh_const(prefix.str().c_str(), s, skolem);
+    }
+
     symbol mk_fresh_var_name(char const * prefix = nullptr);
 
     var * mk_var(unsigned idx, sort * ty);
diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp
index f6f2d6f85a6..0778b98db1f 100644
--- a/src/ast/rewriter/enum2bv_rewriter.cpp
+++ b/src/ast/rewriter/enum2bv_rewriter.cpp
@@ -124,7 +124,7 @@ struct enum2bv_rewriter::imp {
 
                 // create a fresh variable, add bounds constraints for it.
                 unsigned nc = m_dt.get_datatype_num_constructors(s);
-                result = m.mk_fresh_const(f->get_name().str().c_str(), m_bv.mk_sort(bv_size));
+                result = m.mk_fresh_const(f->get_name(), m_bv.mk_sort(bv_size));
                 f_fresh = to_app(result)->get_decl();
                 if (!is_power_of_two(nc) || nc == 1) {
                     m_imp.m_bounds.push_back(m_bv.mk_ule(result, m_bv.mk_numeral(nc-1, bv_size)));
diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp
index 2eb3ccac38f..dbc75c49377 100644
--- a/src/model/func_interp.cpp
+++ b/src/model/func_interp.cpp
@@ -401,7 +401,7 @@ expr* func_interp::get_array_interp_core(func_decl * f) const {
             args.push_back(curr->get_arg(i));
         }
         args.push_back(res);
-        r = autil.mk_store(args.size(), args.c_ptr());
+        r = autil.mk_store(args);
     }
     return r;    
 }
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 50f8bde8a4f..9007abec7de 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -269,7 +269,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 expr_ref_vector args(m);
                 args.push_back(val);
                 args.append(stores[i].size(), stores[i].c_ptr());
-                val = m_ar.mk_store(args.size(), args.c_ptr());
+                val = m_ar.mk_store(args);
             }
         }
     }
diff --git a/src/model/model_implicant.cpp b/src/model/model_implicant.cpp
index 37583447731..2cd78b6ca01 100644
--- a/src/model/model_implicant.cpp
+++ b/src/model/model_implicant.cpp
@@ -897,7 +897,7 @@ expr_ref model_implicant::eval(model_ref& model, expr* e) {
                 args.resize(1);
                 args[0] = result;
                 args.append(stores[i]);
-                result = m_array.mk_store(args.size(), args.c_ptr());
+                result = m_array.mk_store(args);
             }
             return result;
         }
diff --git a/src/muz/spacer/spacer_legacy_mev.cpp b/src/muz/spacer/spacer_legacy_mev.cpp
index b62b24b0de6..944bd075f9d 100644
--- a/src/muz/spacer/spacer_legacy_mev.cpp
+++ b/src/muz/spacer/spacer_legacy_mev.cpp
@@ -816,7 +816,7 @@ expr_ref model_evaluator::eval(const model_ref& model, expr* e){
                 args.resize(1);
                 args[0] = result;
                 args.append(stores[i]);
-                result = m_array.mk_store(args.size(), args.c_ptr());
+                result = m_array.mk_store(args);
             }
             return result;
         }
diff --git a/src/muz/spacer/spacer_mev_array.cpp b/src/muz/spacer/spacer_mev_array.cpp
index fe7b54101e5..8fa9c6d4c4f 100644
--- a/src/muz/spacer/spacer_mev_array.cpp
+++ b/src/muz/spacer/spacer_mev_array.cpp
@@ -153,8 +153,8 @@ void model_evaluator_array_util::eval_array_eq(model& mdl, app* e, expr* arg1, e
         args2.resize(1);
         args1.append(store[i].size()-1, store[i].c_ptr());
         args2.append(store[i].size()-1, store[i].c_ptr());
-        s1 = m_array.mk_select(args1.size(), args1.c_ptr());
-        s2 = m_array.mk_select(args2.size(), args2.c_ptr());
+        s1 = m_array.mk_select(args1);
+        s2 = m_array.mk_select(args2);
         eval (mdl, s1, w1);
         eval (mdl, s2, w2);
         if (w1 == w2) {
@@ -207,7 +207,7 @@ void model_evaluator_array_util::eval(model& mdl, expr* e, expr_ref& r, bool mod
                 args.resize(1);
                 args[0] = r;
                 args.append(stores[i]);
-                r = m_array.mk_store(args.size(), args.c_ptr());
+                r = m_array.mk_store(args);
             }
             return;
         }
diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp
index ed5a0215c84..c4f7d23765e 100644
--- a/src/muz/spacer/spacer_qe_project.cpp
+++ b/src/muz/spacer/spacer_qe_project.cpp
@@ -170,7 +170,7 @@ void peq::mk_eq (app_ref_vector& aux_consts, app_ref& result, bool stores_on_rhs
             store_args.push_back (rhs);
             store_args.push_back (*it);
             store_args.push_back (val);
-            rhs = m_arr_u.mk_store (store_args.size (), store_args.c_ptr ());
+            rhs = m_arr_u.mk_store (store_args);
             aux_consts.push_back (val);
         }
         m_eq = m.mk_eq (lhs, rhs);
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index ea99b5ec276..515226387a8 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1167,7 +1167,7 @@ namespace opt {
     app* context::purify(generic_model_converter_ref& fm, expr* term) {
        std::ostringstream out;
        out << mk_pp(term, m);
-       app* q = m.mk_fresh_const(out.str().c_str(), m.get_sort(term));
+       app* q = m.mk_fresh_const(out.str(), m.get_sort(term));
        if (!fm) fm = alloc(generic_model_converter, m, "opt");
        if (m_arith.is_int_real(term)) {
            m_hard_constraints.push_back(m_arith.mk_ge(q, term));
diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp
index 828ed6a61de..9b96a388e63 100644
--- a/src/qe/qe_arrays.cpp
+++ b/src/qe/qe_arrays.cpp
@@ -139,7 +139,7 @@ namespace {
                     app_ref val(m.mk_fresh_const ("diff", val_sort), m);
                     store_args.push_back (val);
                     aux_consts.push_back (val);
-                    rhs = m_arr_u.mk_store (store_args.size (), store_args.c_ptr ());
+                    rhs = m_arr_u.mk_store (store_args);
                 }
                 m_eq = m.mk_eq (lhs, rhs);
             }
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index 4113fe3c21c..b5f7d973909 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -152,8 +152,7 @@ class lia2card_tactic : public tactic {
         for (unsigned i = lo; i < hi; ++i) {
             checkpoint();
 
-            std::string name(x->get_decl()->get_name().str());
-            expr_ref v(m.mk_fresh_const(name.c_str(), m.mk_bool_sort()), m);
+            expr_ref v(m.mk_fresh_const(x->get_decl()->get_name(), m.mk_bool_sort()), m);
             if (last_v) axioms.push_back(m.mk_implies(v, last_v));
             xs.push_back(m.mk_ite(v, a.mk_int(1), a.mk_int(0)));
             m_mc->hide(v);
diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp
index d11da3274ff..697944f9227 100644
--- a/src/tactic/arith/nla2bv_tactic.cpp
+++ b/src/tactic/arith/nla2bv_tactic.cpp
@@ -238,8 +238,7 @@ class nla2bv_tactic : public tactic {
                 set_satisfiability_preserving(false);
             }
             bv_sort = m_bv.mk_sort(num_bits);
-            std::string name = n->get_decl()->get_name().str();
-            s_bv = m_manager.mk_fresh_const(name.c_str(), bv_sort);
+            s_bv = m_manager.mk_fresh_const(n->get_decl()->get_name(), bv_sort);
             m_fmc->hide(s_bv);
             s_bv = m_bv.mk_bv2int(s_bv);
             if (low) {
@@ -275,9 +274,9 @@ class nla2bv_tactic : public tactic {
             bv_sort = m_bv.mk_sort(m_num_bits);
             set_satisfiability_preserving(false);
             std::string name = n->get_decl()->get_name().str();
-            s = m_manager.mk_fresh_const(name.c_str(), bv_sort);
+            s = m_manager.mk_fresh_const(name, bv_sort);
             name += "_r";
-            t = m_manager.mk_fresh_const(name.c_str(), bv_sort);
+            t = m_manager.mk_fresh_const(name, bv_sort);
             m_fmc->hide(s);
             m_fmc->hide(t);
             s_bv = m_bv2real.mk_bv2real(s, t);
diff --git a/src/tactic/smtlogics/qfaufbv_tactic.cpp b/src/tactic/smtlogics/qfaufbv_tactic.cpp
index e3d7ec95327..a0394d26663 100644
--- a/src/tactic/smtlogics/qfaufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfaufbv_tactic.cpp
@@ -24,6 +24,7 @@ Module Name:
 #include "tactic/bv/max_bv_sharing_tactic.h"
 #include "tactic/bv/bv_size_reduction_tactic.h"
 #include "tactic/core/ctx_simplify_tactic.h"
+#include "tactic/smtlogics/qfbv_tactic.h"
 #include "ackermannization/ackermannize_bv_tactic.h"
 #include "smt/tactic/smt_tactic.h"
 
@@ -56,7 +57,9 @@ tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) {
 
     tactic * preamble_st = mk_qfaufbv_preamble(m, p);
 
-    tactic * st = using_params(and_then(preamble_st, mk_smt_tactic(m)), main_p);
+    tactic * st = using_params(
+        and_then(preamble_st, 
+                 cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic(m))), main_p);
     
     st->updt_params(p);
     return st;