diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 2b8f8abd6..32ed1e236 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -33,9 +33,11 @@ Revision History:
 #include "ast/ast_pp.h"
 #include "ast/ast_util.h"
 #include "model/model_smt2_pp.h"
+#include "ast/rewriter/var_subst.h"
 
 
 struct evaluator_cfg : public default_rewriter_cfg {
+    ast_manager &                   m;
     model_core &                    m_model;
     bool_rewriter                   m_b_rw;
     arith_rewriter                  m_a_rw;
@@ -53,6 +55,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
     bool                            m_array_equalities;
 
     evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p):
+        m(m),
         m_model(md),
         m_b_rw(m),
         // We must allow customers to set parameters for arithmetic rewriter/evaluator.
@@ -74,6 +77,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         m_ar_rw.set_expand_select_store(true);
         m_ar_rw.set_expand_select_ite(true);
         updt_params(p);
+        //add_unspecified_function_models(md);
     }
 
     void updt_params(params_ref const & _p) {
@@ -85,10 +89,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
         m_array_equalities = p.array_equalities();
     }
 
-    ast_manager & m() const { return m_model.get_manager(); }
-
-    bool evaluate(func_decl* f, unsigned num, expr * const * args, expr_ref & result) {
-        func_interp* fi = m_model.get_func_interp(f);
+    bool evaluate(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+        func_interp * fi = m_model.get_func_interp(f);
         return (fi != 0) && eval_fi(fi, num, args, result);
     }
 
@@ -101,9 +103,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
         bool actuals_are_values = true;
 
-        for (unsigned i = 0; actuals_are_values && i < num; i++) {
-            actuals_are_values = m().is_value(args[i]);
-        }
+        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
@@ -120,7 +121,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         result_pr = 0;
         family_id fid = f->get_family_id();
-        bool is_uninterp = fid != null_family_id && m().get_plugin(fid)->is_considered_uninterpreted(f);
+        bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
         if (num == 0 && (fid == null_family_id || is_uninterp)) {
             expr * val = m_model.get_const_interp(f);
             if (val != 0) {
@@ -145,7 +146,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
             if (k == OP_EQ) {
                 // theory dispatch for =
                 SASSERT(num == 2);
-                family_id s_fid = m().get_sort(args[0])->get_family_id();
+                family_id s_fid = m.get_sort(args[0])->get_family_id();
                 if (s_fid == m_a_rw.get_fid())
                     st = m_a_rw.mk_eq_core(args[0], args[1], result);
                 else if (s_fid == m_bv_rw.get_fid())
@@ -178,16 +179,18 @@ struct evaluator_cfg : public default_rewriter_cfg {
             st = m_f_rw.mk_app_core(f, num, args, result);
         else if (fid == m_seq_rw.get_fid())
             st = m_seq_rw.mk_app_core(f, num, args, result);
-        else if (fid == m().get_label_family_id() && num == 1) {
+        else if (fid == m.get_label_family_id() && num == 1) {
             result = args[0];
             st = BR_DONE;
         }
         else if (evaluate(f, num, args, result)) {
             TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
-                  for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
-                  tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";);
+                  for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m) << "\n";
+                  tout << "---->\n" << mk_ismt2_pp(result, m) << "\n";);
             return BR_DONE;
         }
+        if (st == BR_FAILED && !m.is_builtin_family_id(fid))
+            st = evaluate_partial_theory_func(f, num, args, result, result_pr);
         if (st == BR_DONE && is_app(result)) {
             app* a = to_app(result);
             if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) {
@@ -200,14 +203,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
     void expand_value(expr_ref& val) {
         vector<expr_ref_vector> stores;
-        expr_ref else_case(m());
+        expr_ref else_case(m);
         bool _unused;
         if (m_ar.is_array(val) && extract_array_func_interp(val, stores, else_case, _unused)) {
-            sort* srt = m().get_sort(val);
+            sort* srt = m.get_sort(val);
             val = m_ar.mk_const_array(srt, else_case);
             for (unsigned i = stores.size(); i > 0; ) {
                 --i;
-                expr_ref_vector args(m());
+                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());
@@ -220,6 +223,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
 #define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
 
         func_interp * fi = m_model.get_func_interp(f);
+
         if (fi != 0) {
             TRACE_MACRO;
             if (fi->is_partial()) {
@@ -228,31 +232,52 @@ struct evaluator_cfg : public default_rewriter_cfg {
                     expr * val = m_model.get_some_value(s);
                     fi->set_else(val);
                 }
-                else {
+                else
                     return false;
-                }
             }
-            def    = fi->get_interp();
+            def = fi->get_interp();
             SASSERT(def != 0);
             return true;
         }
 
         if (m_model_completion &&
             (f->get_family_id() == null_family_id ||
-             m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f)))
+             m.get_plugin(f->get_family_id())->is_considered_uninterpreted(f)))
         {
             TRACE_MACRO;
             sort * s   = f->get_range();
             expr * val = m_model.get_some_value(s);
-            func_interp * new_fi = alloc(func_interp, m(), f->get_arity());
+            func_interp * new_fi = alloc(func_interp, m, f->get_arity());
             new_fi->set_else(val);
             m_model.register_decl(f, new_fi);
             def = val;
             return true;
         }
+
         return false;
     }
 
+    br_status evaluate_partial_theory_func(func_decl * f,
+                                           unsigned num, expr * const * args,
+                                           expr_ref & result, proof_ref & result_pr) {
+        SASSERT(f != 0);
+        SASSERT(!m.is_builtin_family_id(f->get_family_id()));
+        result = 0;
+        result_pr = 0;
+
+        func_interp * fi = m_model.get_func_interp(f);
+        if (fi) {
+            if (fi->is_partial())
+                fi->set_else(m.get_some_value(f->get_range()));
+
+            var_subst vs(m, false);
+            vs(fi->get_interp(), num, args, result);
+            return BR_REWRITE_FULL;
+        }
+
+        return BR_FAILED;
+    }
+
 
     bool max_steps_exceeded(unsigned num_steps) const {
         cooperate("model evaluator");
@@ -266,7 +291,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
     br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
         if (a == b) {
-            result = m().mk_true();
+            result = m.mk_true();
             return BR_DONE;
         }
         if (!m_array_equalities) {
@@ -275,19 +300,19 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
         vector<expr_ref_vector> stores1, stores2;
         bool args_are_unique1, args_are_unique2;
-        expr_ref else1(m()), else2(m());
+        expr_ref else1(m), else2(m);
         if (extract_array_func_interp(a, stores1, else1, args_are_unique1) &&
             extract_array_func_interp(b, stores2, else2, args_are_unique2)) {
-            expr_ref_vector conj(m()), args1(m()), args2(m());
-            if (m().are_equal(else1, else2)) {
+            expr_ref_vector conj(m), args1(m), args2(m);
+            if (m.are_equal(else1, else2)) {
                 // no op
             }
-            else if (m().are_distinct(else1, else2) && !(m().get_sort(else1)->get_info()->get_num_elements().is_finite())) {
-                result = m().mk_false();
+            else if (m.are_distinct(else1, else2) && !(m.get_sort(else1)->get_info()->get_num_elements().is_finite())) {
+                result = m.mk_false();
                 return BR_DONE;
             }
             else {
-                conj.push_back(m().mk_eq(else1, else2));
+                conj.push_back(m.mk_eq(else1, else2));
             }
             if (args_are_unique1 && args_are_unique2 && !stores1.empty()) {
                 return mk_array_eq_core(stores1, else1, stores2, else2, conj, result);
@@ -300,11 +325,11 @@ struct evaluator_cfg : public default_rewriter_cfg {
             for (unsigned i = 0; i < stores1.size(); ++i) {
                 args1.resize(1); args1.append(stores1[i].size() - 1, stores1[i].c_ptr());
                 args2.resize(1); args2.append(stores1[i].size() - 1, stores1[i].c_ptr());
-                expr_ref s1(m_ar.mk_select(args1.size(), args1.c_ptr()), m());
-                expr_ref s2(m_ar.mk_select(args2.size(), args2.c_ptr()), m());
-                conj.push_back(m().mk_eq(s1, s2));
+                expr_ref s1(m_ar.mk_select(args1.size(), args1.c_ptr()), m);
+                expr_ref s2(m_ar.mk_select(args2.size(), args2.c_ptr()), m);
+                conj.push_back(m.mk_eq(s1, s2));
             }
-            result = m().mk_and(conj.size(), conj.c_ptr());
+            result = m.mk_and(conj.size(), conj.c_ptr());
             return BR_REWRITE_FULL;
         }
         return BR_FAILED;
@@ -362,15 +387,15 @@ struct evaluator_cfg : public default_rewriter_cfg {
             if (table1.find(stores2[i].c_ptr(), args)) {
                 switch (compare(args[arity], val)) {
                 case l_true: table1.remove(args); break;
-                case l_false: result = m().mk_false(); return BR_DONE;
-                default: conj.push_back(m().mk_eq(val, args[arity])); break;
+                case l_false: result = m.mk_false(); return BR_DONE;
+                default: conj.push_back(m.mk_eq(val, args[arity])); break;
                 }
             }
             else {
                 switch (compare(else1, val)) {
                 case l_true: break;
-                case l_false: result = m().mk_false(); return BR_DONE;
-                default: conj.push_back(m().mk_eq(else1, val)); break;
+                case l_false: result = m.mk_false(); return BR_DONE;
+                default: conj.push_back(m.mk_eq(else1, val)); break;
                 }
             }
         }
@@ -378,8 +403,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
         for (; it != end; ++it) {
             switch (compare((*it)[arity], else2)) {
             case l_true: break;
-            case l_false: result = m().mk_false(); return BR_DONE;
-            default: conj.push_back(m().mk_eq((*it)[arity], else2)); break;
+            case l_false: result = m.mk_false(); return BR_DONE;
+            default: conj.push_back(m.mk_eq((*it)[arity], else2)); break;
             }
         }
         result = mk_and(conj);
@@ -387,8 +412,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
     }
 
     lbool compare(expr* a, expr* b) {
-        if (m().are_equal(a, b)) return l_true;
-        if (m().are_distinct(a, b)) return l_false;
+        if (m.are_equal(a, b)) return l_true;
+        if (m.are_distinct(a, b)) return l_false;
         return l_undef;
     }
 
@@ -396,8 +421,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
     bool args_are_values(expr_ref_vector const& store, bool& are_unique) {
         bool are_values = true;
         for (unsigned j = 0; are_values && j + 1 < store.size(); ++j) {
-            are_values = m().is_value(store[j]);
-            are_unique &= m().is_unique_value(store[j]);
+            are_values = m.is_value(store[j]);
+            are_unique &= m.is_unique_value(store[j]);
         }
         SASSERT(!are_unique || are_values);
         return are_values;
@@ -408,10 +433,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
         SASSERT(m_ar.is_array(a));
         bool are_values = true;
         are_unique = true;
-        TRACE("model_evaluator", tout << mk_pp(a, m()) << "\n";);
+        TRACE("model_evaluator", tout << mk_pp(a, m) << "\n";);
 
         while (m_ar.is_store(a)) {
-            expr_ref_vector store(m());
+            expr_ref_vector store(m);
             store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
             are_values &= args_are_values(store, are_unique);
             stores.push_back(store);
@@ -424,7 +449,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         }
 
         if (!m_ar.is_as_array(a)) {
-            TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";);
+            TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m) << "\n";);
             return false;
         }
 
@@ -434,13 +459,13 @@ struct evaluator_cfg : public default_rewriter_cfg {
         unsigned arity = f->get_arity();
         unsigned base_sz = stores.size();
         for (unsigned i = 0; i < sz; ++i) {
-            expr_ref_vector store(m());
+            expr_ref_vector store(m);
             func_entry const* fe = g->get_entry(i);
             store.append(arity, fe->get_args());
             store.push_back(fe->get_result());
             for (unsigned j = 0; j < store.size(); ++j) {
                 if (!is_ground(store[j].get())) {
-                    TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m()) << "\n" << mk_pp(store[j].get(), m()) << "\n";);
+                    TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m) << "\n" << mk_pp(store[j].get(), m) << "\n";);
                     return false;
                 }
             }
@@ -448,18 +473,18 @@ struct evaluator_cfg : public default_rewriter_cfg {
         }
         else_case = g->get_else();
         if (!else_case) {
-            TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m()) << "\n";
-                  /*model_smt2_pp(tout, m(), m_model, 0);*/
+            TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m) << "\n";
+                  /*model_smt2_pp(tout, m, m_model, 0);*/
                   );
             return false;
         }
         if (!is_ground(else_case)) {
-            TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << else_case << "\n";);
+            TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m) << "\n" << else_case << "\n";);
             return false;
         }
         for (unsigned i = stores.size(); are_values && i > base_sz; ) {
             --i;
-            if (m().are_equal(else_case, stores[i].back())) {
+            if (m.are_equal(else_case, stores[i].back())) {
                 for (unsigned j = i + 1; j < stores.size(); ++j) {
                     stores[j-1].reset();
                     stores[j-1].append(stores[j]);
@@ -469,7 +494,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
             }
             are_values &= args_are_values(stores[i], are_unique);
         }
-        TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m()) << "\n";);
+        TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m) << "\n";);
         return true;
     }