diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 125380930..28b726100 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -32,6 +32,7 @@ Revision History:
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/rewriter/var_subst.h"
+#include "ast/rewriter/recfun_rewriter.h"
 #include "model/model_smt2_pp.h"
 #include "model/model.h"
 #include "model/model_evaluator_params.hpp"
@@ -53,6 +54,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
     pb_rewriter                     m_pb_rw;
     fpa_rewriter                    m_f_rw;
     seq_rewriter                    m_seq_rw;
+    recfun_rewriter                 m_rec_rw;
     array_util                      m_ar;
     arith_util                      m_au;
     fpa_util                        m_fpau;
@@ -80,6 +82,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         m_pb_rw(m),
         m_f_rw(m),
         m_seq_rw(m),
+        m_rec_rw(m),
         m_ar(m),
         m_au(m),
         m_fpau(m),
@@ -283,6 +286,8 @@ 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_rec_rw.get_fid())
+            st = m_rec_rw.mk_app_core(f, num, args, result);
         else if (fid == m.get_label_family_id() && num == 1) {
             result = args[0];
             st = BR_DONE;