diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp
index 2516aacfb..0073ef274 100644
--- a/src/api/api_qe.cpp
+++ b/src/api/api_qe.cpp
@@ -52,7 +52,7 @@ extern "C"
         Z3_TRY;
         LOG_Z3_qe_model_project (c, m, num_bounds, bound, body);
         RESET_ERROR_CODE();
-      
+
         app_ref_vector vars(mk_c(c)->m ());
         if (!to_apps(num_bounds, bound, vars)) {
             SET_ERROR_CODE (Z3_INVALID_ARG);
@@ -119,11 +119,8 @@ extern "C"
         facts.push_back (to_expr (fml));
         flatten_and (facts);
 
-        spacer::model_evaluator_util mev (mk_c(c)->m());
-        mev.set_model (*model);
-
         expr_ref_vector lits (mk_c(c)->m());
-        spacer::compute_implicant_literals (mev, facts, lits);
+        spacer::compute_implicant_literals (*model, facts, lits);
 
         expr_ref result (mk_c(c)->m ());
         result = mk_and (lits);
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 03093ab63..db1153de3 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -366,7 +366,7 @@ pob *derivation::create_next_child ()
     // get an implicant of the summary
     expr_ref_vector u(m), lits (m);
     u.push_back (rf->get ());
-    compute_implicant_literals (mev, u, lits);
+    compute_implicant_literals (*model, u, lits);
     expr_ref v(m);
     v = mk_and (lits);
 
@@ -1172,7 +1172,7 @@ expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev,
 
     // -- pick an implicant
     expr_ref_vector lits(m);
-    compute_implicant_literals (mev, summary, lits);
+    compute_implicant_literals (*mev.get_model(), summary, lits);
 
     return mk_and(lits);
 }
@@ -3599,7 +3599,7 @@ reach_fact *pred_transformer::mk_rf (pob& n, model_evaluator_util &mev,
     if (ctx.reach_dnf()) {
         expr_ref_vector u(m), lits(m);
         u.push_back (res);
-        compute_implicant_literals (mev, u, lits);
+        compute_implicant_literals (*mev.get_model(), u, lits);
         res = mk_and (lits);
     }
 
@@ -3670,7 +3670,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
     forms.push_back(pt.get_transition(r));
     forms.push_back(n.post());
 
-    compute_implicant_literals (mev, forms, lits);
+    compute_implicant_literals (*mev.get_model(), forms, lits);
     expr_ref phi = mk_and (lits);
 
     // primed variables of the head
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index f53577b5b..3eb18b0e5 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -405,67 +405,67 @@ namespace spacer {
 
 namespace {
     class implicant_picker {
-        model_evaluator_util &m_mev;
+        model &m_model;
         ast_manager &m;
         arith_util m_arith;
 
         expr_ref_vector m_todo;
         expr_mark m_visited;
 
+        // add literal to the implicant
+        // applies lightweight normalization
+        void add_literal(expr *e, expr_ref_vector &out) {
+            SASSERT(m.is_bool(e));
 
-        void add_literal (expr *e, expr_ref_vector &out) {
-            SASSERT (m.is_bool (e));
+            expr_ref res(m), v(m);
+            v = m_model(e);
+            // the literal must have a value
+            SASSERT(m.is_true(v) || m.is_false(v));
 
-            expr_ref res (m), v(m);
-            m_mev.eval (e, v, false);
-            SASSERT (m.is_true (v) || m.is_false (v));
+            res = m.is_false(v) ? m.mk_not(e) : e;
 
-            res = m.is_false (v) ? m.mk_not (e) : e;
-
-            if (m.is_distinct (res)) {
-                // -- (distinct a b) == (not (= a b))
+            if (m.is_distinct(res)) {
+                // --(distinct a b) == (not (= a b))
                 if (to_app(res)->get_num_args() == 2) {
-                    res = m.mk_eq (to_app(res)->get_arg(0), to_app(res)->get_arg(1));
-                    res = m.mk_not (res);
+                    res = m.mk_eq(to_app(res)->get_arg(0),
+                                  to_app(res)->get_arg(1));
+                    res = m.mk_not(res);
                 }
             }
 
             expr *nres, *f1, *f2;
             if (m.is_not(res, nres)) {
-                // -- (not (xor a b)) == (= a b)
+                // --(not (xor a b)) == (= a b)
                 if (m.is_xor(nres, f1, f2))
-                    { res = m.mk_eq(f1, f2); }
-
+                    res = m.mk_eq(f1, f2);
                 // -- split arithmetic inequality
-                else if (m.is_eq (nres, f1, f2) && m_arith.is_int_real (f1)) {
+                else if (m.is_eq(nres, f1, f2) && m_arith.is_int_real(f1)) {
                     expr_ref u(m);
                     u = m_arith.mk_lt(f1, f2);
-                    if (m_mev.eval (u, v, false) && m.is_true (v))
-                        { res = u; }
-                    else
-                        { res = m_arith.mk_lt(f2, f1); }
+                    res = m_model.is_true(u) ? u : m_arith.mk_lt(f2, f1);
                 }
             }
 
-            if (!m_mev.is_true (res)) {
-                verbose_stream() << "Bad literal: " << mk_pp(res, m) << "\n";
+            if (!m_model.is_true(res)) {
+                verbose_stream() << "Bad literal: " << res << "\n";
             }
-            SASSERT (m_mev.is_true (res));
-            out.push_back (res);
+            SASSERT(m_model.is_true(res));
+            out.push_back(res);
         }
 
         void process_app(app *a, expr_ref_vector &out)  {
-            if (m_visited.is_marked(a)) { return; }
-            SASSERT (m.is_bool (a));
+            if (m_visited.is_marked(a)) return;
+            SASSERT(m.is_bool(a));
             expr_ref v(m);
-            m_mev.eval (a, v, false);
+            v = m_model(a);
             bool is_true = m.is_true(v);
 
             if (!is_true && !m.is_false(v)) return;
 
             expr *na, *f1, *f2, *f3;
 
-            if (m.is_true(a) || m.is_false(a)) {
+            SASSERT(!m.is_false(a));
+            if (m.is_true(a)) {
                 // noop
             }
             else if (a->get_family_id() != m.get_basic_family_id()) {
@@ -479,14 +479,15 @@ namespace {
             }
             else if (m.is_distinct(a)) {
                 if (!is_true) {
-                    f1 = qe::project_plugin::pick_equality(m, *m_mev.get_model(), a);
+                    f1 = qe::project_plugin::pick_equality(m, m_model, a);
                     m_todo.push_back(f1);
                 }
                 else if (a->get_num_args() == 2) {
                     add_literal(a, out);
                 }
                 else {
-                    m_todo.push_back(m.mk_distinct_expanded(a->get_num_args(), a->get_args()));
+                    m_todo.push_back(m.mk_distinct_expanded(a->get_num_args(),
+                                                            a->get_args()));
                 }
             }
             else if (m.is_and(a)) {
@@ -494,8 +495,8 @@ namespace {
                     m_todo.append(a->get_num_args(), a->get_args());
                 }
                 else {
-                    for (expr* e : *a) {
-                        if (m_mev.is_false(e)) {
+                    for(expr* e : *a) {
+                        if (m_model.is_false(e)) {
                             m_todo.push_back(e);
                             break;
                         }
@@ -506,17 +507,19 @@ namespace {
                 if (!is_true)
                     m_todo.append(a->get_num_args(), a->get_args());
                 else {
-                    for (expr * e : *a) {
-                        if (m_mev.is_true(e)) {
+                    for(expr * e : *a) {
+                        if (m_model.is_true(e)) {
                             m_todo.push_back(e);
                             break;
                         }
                     }
                 }
             }
-            else if (m.is_eq(a, f1, f2) || (is_true && m.is_not(a, na) && m.is_xor (na, f1, f2))) {
+            else if (m.is_eq(a, f1, f2) ||
+                     (is_true && m.is_not(a, na) && m.is_xor(na, f1, f2))) {
                 if (!m.are_equal(f1, f2) && !m.are_distinct(f1, f2)) {
-                    if (m.is_bool(f1) && (!is_uninterp_const(f1) || !is_uninterp_const(f2)))
+                    if (m.is_bool(f1) &&
+                        (!is_uninterp_const(f1) || !is_uninterp_const(f2)))
                         m_todo.append(a->get_num_args(), a->get_args());
                     else
                         add_literal(a, out);
@@ -526,19 +529,19 @@ namespace {
                 if (m.are_equal(f2, f3)) {
                     m_todo.push_back(f2);
                 }
-                else if (m_mev.is_true (f2) && m_mev.is_true (f3)) {
+                else if (m_model.is_true(f2) && m_model.is_true(f3)) {
                     m_todo.push_back(f2);
                     m_todo.push_back(f3);
                 }
-                else if (m_mev.is_false(f2) && m_mev.is_false(f3)) {
+                else if (m_model.is_false(f2) && m_model.is_false(f3)) {
                     m_todo.push_back(f2);
                     m_todo.push_back(f3);
                 }
-                else if (m_mev.is_true(f1)) {
+                else if (m_model.is_true(f1)) {
                     m_todo.push_back(f1);
                     m_todo.push_back(f2);
                 }
-                else if (m_mev.is_false(f1)) {
+                else if (m_model.is_false(f1)) {
                     m_todo.push_back(f1);
                     m_todo.push_back(f3);
                 }
@@ -548,16 +551,18 @@ namespace {
             }
             else if (m.is_implies(a, f1, f2)) {
                 if (is_true) {
-                    if (m_mev.is_true(f2))
+                    if (m_model.is_true(f2))
                         m_todo.push_back(f2);
-                    else if (m_mev.is_false(f1))
+                    else if (m_model.is_false(f1))
                         m_todo.push_back(f1);
                 }
                 else
                     m_todo.append(a->get_num_args(), a->get_args());
             }
             else {
-                IF_VERBOSE(0, verbose_stream () << "Unexpected expression: " << mk_pp(a, m) << "\n");
+                IF_VERBOSE(0,
+                           verbose_stream() << "Unexpected expression: "
+                           << mk_pp(a, m) << "\n");
                 UNREACHABLE();
             }
         }
@@ -574,70 +579,72 @@ namespace {
                 m_todo.pop_back();
                 process_app(a, out);
                 m_visited.mark(a, true);
-            } while (!m_todo.empty());
+            } while(!m_todo.empty());
         }
 
         bool pick_implicant(const expr_ref_vector &in, expr_ref_vector &out) {
             m_visited.reset();
-            bool is_true = m_mev.is_true (in);
+            bool is_true = m_model.is_true(in);
 
-            for (expr* e : in) {
-                if (is_true || m_mev.is_true(e)) {
+            for(expr* e : in) {
+                if (is_true || m_model.is_true(e)) {
                     pick_literals(e, out);
                 }
             }
-            m_visited.reset ();
+            m_visited.reset();
             return is_true;
         }
 
     public:
 
-        implicant_picker (model_evaluator_util &mev) :
-            m_mev (mev), m (m_mev.get_ast_manager ()), m_arith(m), m_todo(m) {}
+        implicant_picker(model &mdl) :
+            m_model(mdl), m(m_model.get_manager()), m_arith(m), m_todo(m) {}
 
-        void operator() (expr_ref_vector &in, expr_ref_vector& out) {
-            pick_implicant (in, out);
+        void operator()(expr_ref_vector &in, expr_ref_vector& out) {
+            model::scoped_model_completion _sc_(m_model, false);
+            pick_implicant(in, out);
         }
     };
 }
 
-    void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula,
+    void compute_implicant_literals(model &mdl,
+                                     expr_ref_vector &formula,
                                      expr_ref_vector &res) {
         // flatten the formula and remove all trivial literals
 
-        // TBD: not clear why there is a dependence on it (other than
+        // TBD: not clear why there is a dependence on it(other than
         // not handling of Boolean constants by implicant_picker), however,
         // it was a source of a problem on a benchmark
         flatten_and(formula);
         if (formula.empty()) {return;}
 
-        implicant_picker ipick (mev);
-        ipick (formula, res);
+        implicant_picker ipick(mdl);
+        ipick(formula, res);
     }
 
     void simplify_bounds_old(expr_ref_vector& cube) {
         ast_manager& m = cube.m();
         scoped_no_proof _no_pf_(m);
         goal_ref g(alloc(goal, m, false, false, false));
-        for (expr* c : cube)
+        for(expr* c : cube)
             g->assert_expr(c);
 
         goal_ref_buffer result;
         tactic_ref simplifier = mk_arith_bounds_tactic(m);
-        (*simplifier)(g, result);
+       (*simplifier)(g, result);
         SASSERT(result.size() == 1);
         goal* r = result[0];
         cube.reset();
-        for (unsigned i = 0; i < r->size(); ++i) {
+        for(unsigned i = 0; i < r->size(); ++i) {
             cube.push_back(r->form(i));
         }
     }
 
-    void simplify_bounds_new (expr_ref_vector &cube) {
+    void simplify_bounds_new(expr_ref_vector &cube) {
         ast_manager &m = cube.m();
         scoped_no_proof _no_pf_(m);
         goal_ref g(alloc(goal, m, false, false, false));
-        for (expr* c : cube)
+        for(expr* c : cube)
             g->assert_expr(c);
 
         goal_ref_buffer goals;
@@ -645,12 +652,12 @@ namespace {
         tactic_ref prop_bounds = mk_propagate_ineqs_tactic(m);
         tactic_ref t = and_then(prop_values.get(), prop_bounds.get());
 
-        (*t)(g, goals);
+       (*t)(g, goals);
         SASSERT(goals.size() == 1);
 
         g = goals[0];
         cube.reset();
-        for (unsigned i = 0; i < g->size(); ++i) {
+        for(unsigned i = 0; i < g->size(); ++i) {
             cube.push_back(g->form(i));
         }
     }
@@ -664,86 +671,86 @@ namespace {
         ast_manager &m;
         arith_util m_util;
 
-        adhoc_rewriter_cfg (ast_manager &manager) : m(manager), m_util(m) {}
+        adhoc_rewriter_cfg(ast_manager &manager) : m(manager), m_util(m) {}
 
         bool is_le(func_decl const * n) const { return m_util.is_le(n); }
         bool is_ge(func_decl const * n) const { return m_util.is_ge(n); }
 
-        br_status reduce_app (func_decl * f, unsigned num, expr * const * args,
+        br_status reduce_app(func_decl * f, unsigned num, expr * const * args,
                               expr_ref & result, proof_ref & result_pr) {
             expr * e;
             if (is_le(f))
-                return mk_le_core (args[0], args[1], result);
+                return mk_le_core(args[0], args[1], result);
             if (is_ge(f))
-                return mk_ge_core (args[0], args[1], result);
-            if (m.is_not(f) && m.is_not (args[0], e)) {
+                return mk_ge_core(args[0], args[1], result);
+            if (m.is_not(f) && m.is_not(args[0], e)) {
                 result = e;
                 return BR_DONE;
             }
             return BR_FAILED;
         }
 
-        br_status mk_le_core (expr *arg1, expr * arg2, expr_ref & result) {
-            // t <= -1  ==> t < 0 ==> ! (t >= 0)
-            if (m_util.is_int (arg1) && m_util.is_minus_one (arg2)) {
-                result = m.mk_not (m_util.mk_ge (arg1, mk_zero ()));
+        br_status mk_le_core(expr *arg1, expr * arg2, expr_ref & result) {
+            // t <= -1  ==> t < 0 ==> !(t >= 0)
+            if (m_util.is_int(arg1) && m_util.is_minus_one(arg2)) {
+                result = m.mk_not(m_util.mk_ge(arg1, mk_zero()));
                 return BR_DONE;
             }
             return BR_FAILED;
         }
-        br_status mk_ge_core (expr * arg1, expr * arg2, expr_ref & result) {
-            // t >= 1 ==> t > 0 ==> ! (t <= 0)
-            if (m_util.is_int (arg1) && is_one (arg2)) {
+        br_status mk_ge_core(expr * arg1, expr * arg2, expr_ref & result) {
+            // t >= 1 ==> t > 0 ==> !(t <= 0)
+            if (m_util.is_int(arg1) && is_one(arg2)) {
 
-                result = m.mk_not (m_util.mk_le (arg1, mk_zero ()));
+                result = m.mk_not(m_util.mk_le(arg1, mk_zero()));
                 return BR_DONE;
             }
             return BR_FAILED;
         }
-        expr * mk_zero () {return m_util.mk_numeral (rational (0), true);}
-        bool is_one (expr const * n) const {
-            rational val; return m_util.is_numeral (n, val) && val.is_one ();
+        expr * mk_zero() {return m_util.mk_numeral(rational(0), true);}
+        bool is_one(expr const * n) const {
+            rational val; return m_util.is_numeral(n, val) && val.is_one();
         }
     };
 
-    void normalize (expr *e, expr_ref &out,
+    void normalize(expr *e, expr_ref &out,
                     bool use_simplify_bounds,
                     bool use_factor_eqs)
     {
 
         params_ref params;
         // arith_rewriter
-        params.set_bool ("sort_sums", true);
-        params.set_bool ("gcd_rounding", true);
-        params.set_bool ("arith_lhs", true);
+        params.set_bool("sort_sums", true);
+        params.set_bool("gcd_rounding", true);
+        params.set_bool("arith_lhs", true);
         // poly_rewriter
-        params.set_bool ("som", true);
-        params.set_bool ("flat", true);
+        params.set_bool("som", true);
+        params.set_bool("flat", true);
 
         // apply rewriter
         th_rewriter rw(out.m(), params);
-        rw (e, out);
+        rw(e, out);
 
-        adhoc_rewriter_cfg adhoc_cfg(out.m ());
-        rewriter_tpl<adhoc_rewriter_cfg> adhoc_rw (out.m (), false, adhoc_cfg);
-        adhoc_rw (out.get (), out);
+        adhoc_rewriter_cfg adhoc_cfg(out.m());
+        rewriter_tpl<adhoc_rewriter_cfg> adhoc_rw(out.m(), false, adhoc_cfg);
+        adhoc_rw(out.get(), out);
 
         if (out.m().is_and(out)) {
             expr_ref_vector v(out.m());
-            flatten_and (out, v);
+            flatten_and(out, v);
 
             if (v.size() > 1) {
                 // sort arguments of the top-level and
-                std::stable_sort (v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc());
+                std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc());
 
                 if (use_simplify_bounds) {
                     // remove redundant inequalities
-                    simplify_bounds (v);
+                    simplify_bounds(v);
                 }
                 if (use_factor_eqs) {
                     // -- refactor equivalence classes and choose a representative
                     qe::term_graph egraph(out.m());
-                    egraph.add_lits (v);
+                    egraph.add_lits(v);
                     v.reset();
                     egraph.to_lits(v);
                 }
@@ -755,10 +762,10 @@ namespace {
                       << mk_and(v) << "\n";);
                 TRACE("spacer_normalize",
                       qe::term_graph egraph(out.m());
-                      for (expr* e : v) egraph.add_lit (to_app(e));
+                      for(expr* e : v) egraph.add_lit(to_app(e));
                       tout << "Reduced app:\n"
                       << mk_pp(egraph.to_app(), out.m()) << "\n";);
-                out = mk_and (v);
+                out = mk_and(v);
             }
         }
     }
@@ -768,34 +775,34 @@ namespace {
         ast_manager &m;
         arith_util m_arith;
 
-        adhoc_rewriter_rpp (ast_manager &manager) : m(manager), m_arith(m) {}
+        adhoc_rewriter_rpp(ast_manager &manager) : m(manager), m_arith(m) {}
 
         bool is_le(func_decl const * n) const { return m_arith.is_le(n); }
         bool is_ge(func_decl const * n) const { return m_arith.is_ge(n); }
         bool is_lt(func_decl const * n) const { return m_arith.is_lt(n); }
         bool is_gt(func_decl const * n) const { return m_arith.is_gt(n); }
-        bool is_zero (expr const * n) const {rational val; return m_arith.is_numeral(n, val) && val.is_zero();}
+        bool is_zero(expr const * n) const {rational val; return m_arith.is_numeral(n, val) && val.is_zero();}
 
-        br_status reduce_app (func_decl * f, unsigned num, expr * const * args,
+        br_status reduce_app(func_decl * f, unsigned num, expr * const * args,
                               expr_ref & result, proof_ref & result_pr)
         {
             br_status st = BR_FAILED;
             expr *e1, *e2, *e3, *e4;
 
-            // rewrites (= (+ A (* -1 B)) 0) into (= A B)
-            if (m.is_eq (f) && is_zero (args [1]) &&
-                m_arith.is_add (args[0], e1, e2) &&
-                m_arith.is_mul (e2, e3, e4) && m_arith.is_minus_one (e3)) {
-                result = m.mk_eq (e1, e4);
+            // rewrites(=(+ A(* -1 B)) 0) into(= A B)
+            if (m.is_eq(f) && is_zero(args [1]) &&
+                m_arith.is_add(args[0], e1, e2) &&
+                m_arith.is_mul(e2, e3, e4) && m_arith.is_minus_one(e3)) {
+                result = m.mk_eq(e1, e4);
                 return BR_DONE;
             }
             // simplify normalized leq, where right side is different from 0
-            // rewrites (<= (+ A (* -1 B)) C) into (<= A B+C)
+            // rewrites(<=(+ A(* -1 B)) C) into(<= A B+C)
             else if ((is_le(f) || is_lt(f) || is_ge(f) || is_gt(f)) &&
-                     m_arith.is_add (args[0], e1, e2) &&
-                     m_arith.is_mul (e2, e3, e4) && m_arith.is_minus_one (e3)) {
+                     m_arith.is_add(args[0], e1, e2) &&
+                     m_arith.is_mul(e2, e3, e4) && m_arith.is_minus_one(e3)) {
                 expr_ref rhs(m);
-                rhs = is_zero (args[1]) ? e4 : m_arith.mk_add(e4, args[1]);
+                rhs = is_zero(args[1]) ? e4 : m_arith.mk_add(e4, args[1]);
 
                 if (is_le(f)) {
                     result = m_arith.mk_le(e1, rhs);
@@ -813,7 +820,7 @@ namespace {
                 { UNREACHABLE(); }
             }
             // simplify negation of ordering predicate
-            else if (m.is_not (f)) {
+            else if (m.is_not(f)) {
                 if (m_arith.is_lt(args[0], e1, e2)) {
                     result = m_arith.mk_ge(e1, e2);
                     st = BR_DONE;
@@ -834,11 +841,11 @@ namespace {
 
     mk_epp::mk_epp(ast *t, ast_manager &m, unsigned indent,
                    unsigned num_vars, char const * var_prefix) :
-        mk_pp (t, m, m_epp_params, indent, num_vars, var_prefix), m_epp_expr(m) {
+        mk_pp(t, m, m_epp_params, indent, num_vars, var_prefix), m_epp_expr(m) {
         m_epp_params.set_uint("min_alias_size", UINT_MAX);
         m_epp_params.set_uint("max_depth", UINT_MAX);
 
-        if (is_expr (m_ast)) {
+        if (is_expr(m_ast)) {
             rw(to_expr(m_ast), m_epp_expr);
             m_ast = m_epp_expr;
         }
@@ -858,11 +865,11 @@ namespace {
         if (vars.size() < fv.size()) {
             vars.resize(fv.size());
         }
-        for (unsigned i = 0, sz = fv.size(); i < sz; ++i) {
+        for(unsigned i = 0, sz = fv.size(); i < sz; ++i) {
             sort *s = fv[i] ? fv[i] : m.mk_bool_sort();
             vars[i] = mk_zk_const(m, i, s);
             var_subst vs(m, false);
-            vs(e, vars.size(), (expr * *) vars.c_ptr(), out);
+            vs(e, vars.size(),(expr * *) vars.c_ptr(), out);
         }
     }
 
@@ -872,75 +879,75 @@ namespace {
         app_ref          m_var;
         expr_ref_vector &m_res;
 
-        index_term_finder (ast_manager &mgr, app* v, expr_ref_vector &res) : m(mgr), m_array (m), m_var (v, m), m_res (res) {}
-        void operator() (var *n) {}
-        void operator() (quantifier *n) {}
-        void operator() (app *n) {
-            if (m_array.is_select (n) || m.is_eq(n)) {
+        index_term_finder(ast_manager &mgr, app* v, expr_ref_vector &res) : m(mgr), m_array(m), m_var(v, m), m_res(res) {}
+        void operator()(var *n) {}
+        void operator()(quantifier *n) {}
+        void operator()(app *n) {
+            if (m_array.is_select(n) || m.is_eq(n)) {
                 unsigned i = 0;
-                for (expr * arg : *n) {
-                    if ((m.is_eq(n) || i > 0) && m_var != arg) m_res.push_back (arg);
+                for(expr * arg : *n) {
+                    if ((m.is_eq(n) || i > 0) && m_var != arg) m_res.push_back(arg);
                     ++i;
                 }
             }
         }
     };
 
-    bool mbqi_project_var (model_evaluator_util &mev, app* var, expr_ref &fml) {
-        ast_manager &m = fml.get_manager ();
+    bool mbqi_project_var(model_evaluator_util &mev, app* var, expr_ref &fml) {
+        ast_manager &m = fml.get_manager();
 
         expr_ref val(m);
-        mev.eval (var, val, false);
+        mev.eval(var, val, false);
 
-        TRACE ("mbqi_project_verbose",
-               tout << "MBQI: var: " << mk_pp (var, m) << "\n"
+        TRACE("mbqi_project_verbose",
+               tout << "MBQI: var: " << mk_pp(var, m) << "\n"
                << "fml: " << fml << "\n";);
-        expr_ref_vector terms (m);
-        index_term_finder finder (m, var, terms);
-        for_each_expr (finder, fml);
+        expr_ref_vector terms(m);
+        index_term_finder finder(m, var, terms);
+        for_each_expr(finder, fml);
 
-        TRACE ("mbqi_project_verbose",
+        TRACE("mbqi_project_verbose",
                tout << "terms:\n" << terms << "\n";);
 
-        for (expr * term : terms) {
-            expr_ref tval (m);
-            mev.eval (term, tval, false);
+        for(expr * term : terms) {
+            expr_ref tval(m);
+            mev.eval(term, tval, false);
 
-            TRACE ("mbqi_project_verbose",
-                   tout << "term: " << mk_pp (term, m)
+            TRACE("mbqi_project_verbose",
+                   tout << "term: " << mk_pp(term, m)
                    << " tval: " << tval
-                   << " val: " << mk_pp (val, m) << "\n";);
+                   << " val: " << mk_pp(val, m) << "\n";);
 
             // -- if the term does not contain an occurrence of var
             // -- and is in the same equivalence class in the model
-            if (tval == val && !occurs (var, term)) {
-                TRACE ("mbqi_project",
-                       tout << "MBQI: replacing " << mk_pp (var, m) << " with " << mk_pp (term, m) << "\n";);
+            if (tval == val && !occurs(var, term)) {
+                TRACE("mbqi_project",
+                       tout << "MBQI: replacing " << mk_pp(var, m) << " with " << mk_pp(term, m) << "\n";);
                 expr_safe_replace sub(m);
-                sub.insert (var, term);
-                sub (fml);
+                sub.insert(var, term);
+                sub(fml);
                 return true;
             }
         }
 
-        TRACE ("mbqi_project",
-               tout << "MBQI: failed to eliminate " << mk_pp (var, m) << " from " << fml << "\n";);
+        TRACE("mbqi_project",
+               tout << "MBQI: failed to eliminate " << mk_pp(var, m) << " from " << fml << "\n";);
 
         return false;
     }
 
-    void mbqi_project (model &M, app_ref_vector &vars, expr_ref &fml) {
-        ast_manager &m = fml.get_manager ();
+    void mbqi_project(model &M, app_ref_vector &vars, expr_ref &fml) {
+        ast_manager &m = fml.get_manager();
         model_evaluator_util mev(m);
-        mev.set_model (M);
+        mev.set_model(M);
         expr_ref tmp(m);
         // -- evaluate to initialize mev cache
-        mev.eval (fml, tmp, false);
-        tmp.reset ();
+        mev.eval(fml, tmp, false);
+        tmp.reset();
 
         unsigned j = 0;
-        for (app* v : vars)
-            if (!mbqi_project_var (mev, v, fml))
+        for(app* v : vars)
+            if (!mbqi_project_var(mev, v, fml))
                 vars[j++] = v;
         vars.shrink(j);
     }
@@ -959,7 +966,7 @@ namespace {
             for_each_expr(cs, fml);
             return false;
         }
-        catch (found) {
+        catch(found) {
             return true;
         }
     }
@@ -970,8 +977,8 @@ namespace {
         collect_indices(app_ref_vector& indices): m_indices(indices), a(indices.get_manager()) {}
         void operator()(expr* n) {}
         void operator()(app* n) {
-            if (a.is_select (n))
-                for (unsigned i = 1; i < n->get_num_args(); ++i)
+            if (a.is_select(n))
+                for(unsigned i = 1; i < n->get_num_args(); ++i)
                     if (is_app(n->get_arg(i)))
                         m_indices.push_back(to_app(n->get_arg(i)));
         }
diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h
index f43195a97..a66d2dd5a 100644
--- a/src/muz/spacer/spacer_util.h
+++ b/src/muz/spacer/spacer_util.h
@@ -48,17 +48,17 @@ namespace spacer {
         return UINT_MAX;
     }
 
-    inline bool is_infty_level(unsigned lvl) { 
-        return lvl == infty_level (); 
+    inline bool is_infty_level(unsigned lvl) {
+        return lvl == infty_level ();
     }
 
-    inline unsigned next_level(unsigned lvl) { 
-        return is_infty_level(lvl)?lvl:(lvl+1); 
+    inline unsigned next_level(unsigned lvl) {
+        return is_infty_level(lvl)?lvl:(lvl+1);
     }
 
     inline unsigned prev_level (unsigned lvl) {
-        if (is_infty_level(lvl)) return infty_level(); 
-        if (lvl == 0) return 0; 
+        if (is_infty_level(lvl)) return infty_level();
+        if (lvl == 0) return 0;
         return lvl - 1;
     }
 
@@ -78,28 +78,28 @@ namespace spacer {
     typedef ptr_vector<app> app_vector;
     typedef ptr_vector<func_decl> decl_vector;
     typedef obj_hashtable<func_decl> func_decl_set;
-    
+
     // TBD: deprecate
     class model_evaluator_util {
         ast_manager&           m;
         model_ref              m_model;
         model_evaluator*       m_mev;
-        
+
         /// initialize with a given model. All previous state is lost. model can be NULL
         void reset (model *model);
     public:
         model_evaluator_util(ast_manager& m);
         ~model_evaluator_util();
-        
+
         void set_model(model &model) {reset (&model);}
         model_ref &get_model() {return m_model;}
         ast_manager& get_ast_manager() const {return m;}
-        
+
     public:
         bool is_true (const expr_ref_vector &v);
         bool is_false(expr* x);
         bool is_true(expr* x);
-        
+
         bool eval (const expr_ref_vector &v, expr_ref &result, bool model_completion);
         /// evaluates an expression
         bool eval (expr *e, expr_ref &result, bool model_completion);
@@ -109,10 +109,10 @@ namespace spacer {
     /**
        \brief hoist non-boolean if expressions.
     */
-    
+
     void to_mbp_benchmark(std::ostream &out, const expr* fml, const app_ref_vector &vars);
 
-    
+
     // TBD: deprecate by qe::mbp
     /**
      * do the following in sequence
@@ -126,27 +126,29 @@ namespace spacer {
                      bool dont_sub=false);
 
     void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, model_ref& M, expr_map& map);
-    
+
     // TBD: sort out
     void expand_literals(ast_manager &m, expr_ref_vector& conjs);
-    void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula, expr_ref_vector &res);
+    void compute_implicant_literals(model &mdl,
+                                    expr_ref_vector &formula,
+                                    expr_ref_vector &res);
     void simplify_bounds (expr_ref_vector &lemmas);
     void normalize(expr *e, expr_ref &out, bool use_simplify_bounds = true, bool factor_eqs = false);
-    
-    /** 
+
+    /**
      * Ground expression by replacing all free variables by skolem
      * constants. On return, out is the resulting expression, and vars is
      * a map from variable ids to corresponding skolem constants.
      */
     void ground_expr (expr *e, expr_ref &out, app_ref_vector &vars);
-        
+
     void mbqi_project (model &M, app_ref_vector &vars, expr_ref &fml);
-    
+
     bool contains_selects (expr* fml, ast_manager& m);
     void get_select_indices (expr* fml, app_ref_vector& indices, ast_manager& m);
-    
+
     void find_decls (expr* fml, app_ref_vector& decls, std::string& prefix);
-    
+
     /**
      * extended pretty-printer
      * used for debugging
@@ -156,7 +158,7 @@ namespace spacer {
         params_ref m_epp_params;
         expr_ref m_epp_expr;
     mk_epp(ast *t, ast_manager &m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = nullptr);
-        void rw(expr *e, expr_ref &out);        
+        void rw(expr *e, expr_ref &out);
     };
 }