fix #8109

default behavior is conservative: if the body of a recursive function contains uninterpreted variables they are not rewritten.
Model evaluation will bind values to uninterpreted variables so the filter should not apply here.

src/ast/rewriter/recfun_rewriter.cpp

@@ -21,6 +21,12 @@ Author:
 #include "ast/rewriter/var_subst.h"
 #include "ast/datatype_decl_plugin.h"
 #include "ast/for_each_expr.h"
+#include "params/rewriter_params.hpp"
+
+void recfun_rewriter::updt_params(params_ref const &p) {
+    rewriter_params rp(p);
+    m_recfun_unfold = rp.unfold_recursive_functions();
+}
     
 br_status recfun_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
     if (m_rec.is_defined(f) && num_args > 0) {
@@ -34,9 +40,11 @@ br_status recfun_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr *
         for (unsigned i = 0; i < num_args; ++i) 
             if (!m.is_value(args[i]))
                 safe_to_subst = false;
-        for (auto t : subterms::all(expr_ref(r, m)))
+        if (!m_recfun_unfold) {
-            if (is_uninterp(t))
+            for (auto t : subterms::all(expr_ref(r, m)))
-                return BR_FAILED;
+                if (is_uninterp(t))
+                    return BR_FAILED;
+        }            
 
         // check if there is an argument that is a constructor
         // such that the recursive function can be partially evaluated.

src/ast/rewriter/recfun_rewriter.h

@@ -24,6 +24,8 @@ Author:
 class recfun_rewriter {
     ast_manager& m;
     recfun::util  m_rec;
+    bool m_recfun_unfold = false;
+
 public:
     recfun_rewriter(ast_manager& m): m(m), m_rec(m) {}
     
@@ -31,5 +33,7 @@ public:
 
     family_id get_fid() const { return m_rec.get_family_id(); }
 
+    void updt_params(params_ref const &p);
+
 };
 

src/ast/rewriter/th_rewriter.cpp

@@ -108,6 +108,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_ar_rw.updt_params(p);
         m_f_rw.updt_params(p);
         m_seq_rw.updt_params(p);
+        m_rec_rw.updt_params(p);
         updt_local_params(p);
     }
 

src/model/model_evaluator.cpp

@@ -96,6 +96,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
         m_bv_rw.set_mkbv2num(true);
         m_ar_rw.set_expand_select_store(true);
         m_ar_rw.set_expand_select_ite(true);
+        params_ref rp;
+        rp.set_bool("unfold_recursive_functions", true);
+        m_rec_rw.updt_params(rp);
         updt_params(p);
         //add_unspecified_function_models(md);
     }

src/params/rewriter_params.pyg

@@ -7,6 +7,7 @@ def_module_params('rewriter',
                           ("push_ite_bv", BOOL, False, "push if-then-else over bit-vector terms."),
                           ("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."),
                           ("bv_ineq_consistency_test_max", UINT, 0, "max size of conjunctions on which to perform consistency test based on inequalities on bitvectors."),
+                          ("unfold_recursive_functions", BOOL, False, "apply simplification recursively on recursive functions."),
                           ("cache_all", BOOL, False, "cache all intermediate results."),
 			  ("enable_der", BOOL, True, "enable destructive equality resolution to quantifiers."),
                           ("rewrite_patterns", BOOL, False, "rewrite patterns."),