diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 7488e6b18..a565ea5ac 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -49,9 +49,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
     evaluator_cfg(ast_manager & m, model & md, params_ref const & p):
         m_model(md),
         m_b_rw(m),
-        // We must allow customers to set parameters for arithmetic rewriter/evaluator. 
+        // We must allow customers to set parameters for arithmetic rewriter/evaluator.
         // In particular, the maximum degree of algebraic numbers that will be evaluated.
-        m_a_rw(m, p), 
+        m_a_rw(m, p),
         m_bv_rw(m),
         // See comment above. We want to allow customers to set :sort-store
         m_ar_rw(m, p),
@@ -73,7 +73,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         m_model_completion = p.completion();
         m_cache            = p.cache();
     }
-        
+
     ast_manager & m() const { return m_model.get_manager(); }
 
     bool evaluate(func_decl* f, unsigned num, expr * const * args, expr_ref & result) {
@@ -89,11 +89,11 @@ struct evaluator_cfg : public default_rewriter_cfg {
         SASSERT(fi->get_arity() == num);
 
         bool actuals_are_values = true;
-    
+
         for (unsigned i = 0; actuals_are_values && i < num; i++) {
             actuals_are_values = m().is_value(args[i]);
         }
-        
+
         if (!actuals_are_values)
             return false; // let get_macro handle it
 
@@ -115,7 +115,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 result = val;
                 return BR_DONE;
             }
-            
+
             if (m_model_completion) {
                 sort * s   = f->get_range();
                 expr * val = m_model.get_some_value(s);
@@ -154,7 +154,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
             st = m_a_rw.mk_app_core(f, num, args, result);
         else if (fid == m_bv_rw.get_fid())
             st = m_bv_rw.mk_app_core(f, num, args, result);
-        else if (fid == m_ar_rw.get_fid()) 
+        else if (fid == m_ar_rw.get_fid())
             st = m_ar_rw.mk_app_core(f, num, args, result);
         else if (fid == m_dt_rw.get_fid())
             st = m_dt_rw.mk_app_core(f, num, args, result);
@@ -180,9 +180,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
         return st;
     }
 
-    bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { 
+    bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
 
-        func_interp * fi = m_model.get_func_interp(f);        
+        func_interp * fi = m_model.get_func_interp(f);
         if (fi != 0) {
             if (fi->is_partial()) {
                 if (m_model_completion) {
@@ -193,7 +193,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 else {
                     return false;
                 }
-            }            
+            }
             def    = fi->get_interp();
             SASSERT(def != 0);
             return true;
@@ -211,8 +211,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
         return false;
     }
 
-    
-    bool max_steps_exceeded(unsigned num_steps) const { 
+
+    bool max_steps_exceeded(unsigned num_steps) const {
         cooperate("model evaluator");
         if (memory::get_allocation_size() > m_max_memory)
             throw rewriter_exception(Z3_MAX_MEMORY_MSG);
@@ -228,7 +228,7 @@ template class rewriter_tpl<evaluator_cfg>;
 struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
     evaluator_cfg m_cfg;
     imp(model & md, params_ref const & p):
-        rewriter_tpl<evaluator_cfg>(md.get_manager(), 
+        rewriter_tpl<evaluator_cfg>(md.get_manager(),
                                     false, // no proofs for evaluator
                                     m_cfg),
         m_cfg(md.get_manager(), md, p) {