diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 3764089a9..266598467 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -37,7 +37,7 @@ Revision History:
 #include "model/model_v2_pp.h"
 
 
-namespace {
+namespace mev {
 
 struct evaluator_cfg : public default_rewriter_cfg {
     ast_manager &                   m;
@@ -144,13 +144,22 @@ struct evaluator_cfg : public default_rewriter_cfg {
         return th.reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr);
     }
 
-
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+        auto st = reduce_app_core(f, num, args, result, result_pr);
+        CTRACE("model_evaluator", st != BR_FAILED, 
+               tout << f->get_name() << " ";
+               for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << " ";
+               tout << "\n";
+               tout << result << "\n";);
+               
+        return st;
+    }
+
+    br_status reduce_app_core(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         result_pr = nullptr;
         family_id fid = f->get_family_id();
         bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
         br_status st = BR_FAILED;
-        TRACE("model_evaluator", tout << f->get_name() << " " << is_uninterp << "\n";);
         if (num == 0 && (fid == null_family_id || is_uninterp)) { // || m_ar.is_as_array(f)
             expr * val = m_model.get_const_interp(f);
             if (val != nullptr) {
@@ -197,15 +206,11 @@ struct evaluator_cfg : public default_rewriter_cfg {
                     result = m.mk_false();
                     st = BR_DONE;
                 }
-                TRACE("model_evaluator",
-                      tout << st << " " << mk_pp(s, m) << " " << s_fid << " " << m_ar_rw.get_fid() << " "
-                      << mk_pp(args[0], m) << " " << mk_pp(args[1], m) << " " << result << "\n";);
                 if (st != BR_FAILED)
                     return st;
             }
             return m_b_rw.mk_app_core(f, num, args, result);
         }
-        CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
         if (fid == m_a_rw.get_fid())
             st = m_a_rw.mk_app_core(f, num, args, result);
         else if (fid == m_bv_rw.get_fid())
@@ -227,10 +232,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
         else if (evaluate(f, num, args, result)) {
             st = BR_REWRITE1;
         }
-        CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
         if (st == BR_FAILED && !m.is_builtin_family_id(fid)) {
             st = evaluate_partial_theory_func(f, num, args, result, result_pr);
-            CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
         }
         if (st == BR_DONE && is_app(result)) {
             app* a = to_app(result);
@@ -256,7 +259,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
             }
         }
 
-        CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
         return st;
     }
 
@@ -576,10 +578,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
 };
 }
 
-struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
-    evaluator_cfg m_cfg;
+struct model_evaluator::imp : public rewriter_tpl<mev::evaluator_cfg> {
+    mev::evaluator_cfg m_cfg;
     imp(model_core & md, params_ref const & p):
-        rewriter_tpl<evaluator_cfg>(md.get_manager(),
+        rewriter_tpl<mev::evaluator_cfg>(md.get_manager(),
                                     false, // no proofs for evaluator
                                     m_cfg),
         m_cfg(md.get_manager(), md, p) {
@@ -587,7 +589,7 @@ struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
     }
     void expand_stores(expr_ref &val) {m_cfg.expand_stores(val);}
     void reset() {
-        rewriter_tpl<evaluator_cfg>::reset();
+        rewriter_tpl<mev::evaluator_cfg>::reset();
         m_cfg.reset();
         m_cfg.m_def_cache.reset();
     }