diff --git a/src/model/model.cpp b/src/model/model.cpp
index e6c7b74a0..9ac971afe 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -26,16 +26,15 @@ Revision History:
 #include "model/model_evaluator.h"
 
 model::model(ast_manager & m):
-    model_core(m) {
+    model_core(m),
+    m_mev(*this) {
 }
 
 model::~model() {
-    sort2universe::iterator it3  = m_usort2universe.begin();
-    sort2universe::iterator end3 = m_usort2universe.end();
-    for (; it3 != end3; ++it3) {
-        m_manager.dec_ref(it3->m_key);
-        m_manager.dec_array_ref(it3->m_value->size(), it3->m_value->c_ptr());
-        dealloc(it3->m_value);
+    for (auto & kv : m_usort2universe) {
+        m_manager.dec_ref(kv.m_key);
+        m_manager.dec_array_ref(kv.m_value->size(), kv.m_value->c_ptr());
+        dealloc(kv.m_value);
     }
 }
 
@@ -48,19 +47,13 @@ void model::copy_const_interps(model const & source) {
 }
 
 void model::copy_func_interps(model const & source) {
-    decl2finterp::iterator it2  = source.m_finterp.begin();
-    decl2finterp::iterator end2 = source.m_finterp.end();
-    for (; it2 != end2; ++it2) {
-        register_decl(it2->m_key, it2->m_value->copy());
-    }
+    for (auto const& kv : source.m_finterp) 
+        register_decl(kv.m_key, kv.m_value->copy());
 }
 
 void model::copy_usort_interps(model const & source) {
-    sort2universe::iterator it3  = source.m_usort2universe.begin();
-    sort2universe::iterator end3 = source.m_usort2universe.end();
-    for (; it3 != end3; ++it3) {
-        register_usort(it3->m_key, it3->m_value->size(), it3->m_value->c_ptr());
-    }
+    for (auto const& kv : source.m_usort2universe) 
+        register_usort(kv.m_key, kv.m_value->size(), kv.m_value->c_ptr());
 }
 
 model * model::copy() const {
@@ -151,28 +144,21 @@ model * model::translate(ast_translation & translator) const {
     model * res = alloc(model, translator.to());
 
     // Translate const interps
-    decl2expr::iterator it1  = m_interp.begin();
-    decl2expr::iterator end1 = m_interp.end();
-    for (; it1 != end1; ++it1) {
-        res->register_decl(translator(it1->m_key), translator(it1->m_value));
-    }
+    for (auto const& kv : m_interp) 
+        res->register_decl(translator(kv.m_key), translator(kv.m_value));
 
     // Translate func interps
-    decl2finterp::iterator it2  = m_finterp.begin();
-    decl2finterp::iterator end2 = m_finterp.end();
-    for (; it2 != end2; ++it2) {
-        func_interp * fi = it2->m_value;
-        res->register_decl(translator(it2->m_key), fi->translate(translator));
+    for (auto const& kv : m_finterp) {
+        func_interp * fi = kv.m_value;
+        res->register_decl(translator(kv.m_key), fi->translate(translator));
     }
 
     // Translate usort interps
-    sort2universe::iterator it3  = m_usort2universe.begin();
-    sort2universe::iterator end3 = m_usort2universe.end();
-    for (; it3 != end3; ++it3) {
+    for (auto const& kv : m_usort2universe) {
         ptr_vector<expr> new_universe;
-        for (unsigned i=0; i<it3->m_value->size(); i++)
-            new_universe.push_back(translator(it3->m_value->get(i)));
-        res->register_usort(translator(it3->m_key),
+        for (unsigned i=0; i < kv.m_value->size(); i++)
+            new_universe.push_back(translator(kv.m_value->get(i)));
+        res->register_usort(translator(kv.m_key),
                             new_universe.size(),
                             new_universe.c_ptr());
     }
@@ -180,3 +166,30 @@ model * model::translate(ast_translation & translator) const {
     return res;
 }
 
+expr_ref model::operator()(expr* t) {
+    return m_mev(t);
+}
+
+expr_ref_vector model::operator()(expr_ref_vector const& ts) {
+    expr_ref_vector rs(m());
+    for (expr* t : ts) rs.push_back((*this)(t));
+    return rs;
+}
+
+bool model::is_true(expr* t) {
+    return m().is_true((*this)(t));
+}
+
+bool model::is_false(expr* t) {
+    return m().is_false((*this)(t));
+}
+
+bool model::is_true(expr_ref_vector const& ts) {
+    for (expr* t : ts) if (!is_true(t)) return false;
+    return true;
+}
+
+void model::reset_eval_cache() {
+    m_mev.reset();
+}
+
diff --git a/src/model/model.h b/src/model/model.h
index 758d3d451..3fda2832f 100644
--- a/src/model/model.h
+++ b/src/model/model.h
@@ -20,6 +20,7 @@ Revision History:
 #define MODEL_H_
 
 #include "model/model_core.h"
+#include "model/model_evaluator.h"
 #include "util/ref.h"
 #include "ast/ast_translation.h"
 
@@ -29,6 +30,7 @@ protected:
     
     ptr_vector<sort>              m_usorts;
     sort2universe                 m_usort2universe;
+    model_evaluator               m_mev;
     struct value_proc;
 
 public:
@@ -58,6 +60,40 @@ public:
     // Model translation
     //
     model * translate(ast_translation & translator) const;
+
+    void set_model_completion(bool f) { m_mev.set_model_completion(f); }
+    void updt_params(params_ref const & p) { m_mev.updt_params(p); }
+
+    /**
+     * evaluation using the model evaluator. Caches results.
+     */
+    expr_ref operator()(expr* t);
+    expr_ref_vector operator()(expr_ref_vector const& ts);
+    bool is_true(expr* t);
+    bool is_false(expr* t);
+    bool is_true(expr_ref_vector const& ts);
+    void reset_eval_cache();
+
+    class scoped_model_completion {
+        bool   m_old_completion;
+        model& m_model;
+    public:
+        scoped_model_completion(model& m, bool c): 
+            m_old_completion(m.m_mev.get_model_completion()), m_model(m) {
+            m.set_model_completion(c);
+        }
+#if 0
+        scoped_model_completion(model_ref& m, bool c): 
+            m_old_completion(m->m_mev.get_model_completion()), m_model(*m.get()) {
+            m->set_model_completion(c);
+        }
+#endif
+        ~scoped_model_completion() {
+            m_model.set_model_completion(m_old_completion);
+        }
+    };
+
+    
 };
 
 typedef ref<model> model_ref;
diff --git a/src/model/model_core.h b/src/model/model_core.h
index ce211c0b8..400b2fcab 100644
--- a/src/model/model_core.h
+++ b/src/model/model_core.h
@@ -40,6 +40,7 @@ public:
     virtual ~model_core();
 
     ast_manager & get_manager() const { return m_manager; }
+    ast_manager& m() { return m_manager; }
 
     unsigned get_num_decls() const { return m_decls.size(); }
     func_decl * get_decl(unsigned i) const { return m_decls[i]; }
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 250b28ff2..f7c7fa74d 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -85,8 +85,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
         model_evaluator_params p(_p);
         m_max_memory       = megabytes_to_bytes(p.max_memory());
         m_max_steps        = p.max_steps();
-        m_model_completion = p.completion();
         m_cache            = p.cache();
+        m_model_completion = p.completion();
         m_array_equalities = p.array_equalities();
         m_array_as_stores  = p.array_as_stores();
     }
@@ -544,6 +544,10 @@ void model_evaluator::set_model_completion(bool f) {
     m_imp->cfg().m_model_completion = f;
 }
 
+bool model_evaluator::get_model_completion() const {
+    return m_imp->cfg().m_model_completion;
+}
+
 void model_evaluator::set_expand_array_equalities(bool f) {
     m_imp->cfg().m_array_equalities = f;
 }
diff --git a/src/model/model_evaluator.h b/src/model/model_evaluator.h
index d9bf3c375..8666e3519 100644
--- a/src/model/model_evaluator.h
+++ b/src/model/model_evaluator.h
@@ -37,6 +37,7 @@ public:
 
     ast_manager & m () const;
     void set_model_completion(bool f);
+    bool get_model_completion() const; 
     void set_expand_array_equalities(bool f);
 
     void updt_params(params_ref const & p);
diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index 679adb2dd..fc41f54a4 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -62,7 +62,7 @@ class fm_tactic : public tactic {
             return m.is_false(val);
         }
 
-        r_kind process(func_decl * x, expr * cls, arith_util & u, model_evaluator & ev, rational & r) {
+        r_kind process(func_decl * x, expr * cls, arith_util & u, model& ev, rational & r) {
             unsigned num_lits;
             expr * const * lits;
             if (m.is_or(cls)) {
@@ -80,9 +80,7 @@ class fm_tactic : public tactic {
                 expr * l = lits[i];
                 expr * atom;
                 if (is_uninterp_const(l) || (m.is_not(l, atom) && is_uninterp_const(atom))) {
-                    expr_ref val(m);
-                    ev(l, val);
-                    if (m.is_true(val))
+                    if (ev.is_true(l)) 
                         return NONE; // clause was satisfied
                 }
                 else {
@@ -131,7 +129,7 @@ class fm_tactic : public tactic {
                         }
                         else {
                             expr_ref val(m);
-                            ev(monomial, val);
+                            val = ev(monomial);
                             SASSERT(u.is_numeral(val));
                             rational tmp;
                             u.is_numeral(val, tmp);
@@ -184,8 +182,9 @@ class fm_tactic : public tactic {
 
         void operator()(model_ref & md) override {
             TRACE("fm_mc", model_v2_pp(tout, *md); display(tout););
-            model_evaluator ev(*(md.get()));
-            ev.set_model_completion(true);
+            model::scoped_model_completion _sc(*md, true);
+            //model_evaluator ev(*(md.get()));
+            //ev.set_model_completion(true);
             arith_util u(m);
             unsigned i = m_xs.size();
             while (i > 0) {
@@ -201,7 +200,7 @@ class fm_tactic : public tactic {
                 clauses::iterator end = m_clauses[i].end();
                 for (; it != end; ++it) {
                     if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg());
-                    switch (process(x, *it, u, ev, val)) {
+                    switch (process(x, *it, u, *md, val)) {
                     case NONE: 
                         TRACE("fm_mc", tout << "no bound for:\n" << mk_ismt2_pp(*it, m) << "\n";);
                         break;