fix #4155

Author: NikolajBjorner

src/ast/recfun_decl_plugin.h

@@ -236,8 +236,12 @@ namespace recfun {
         //<! add a function declaration
         def * decl_fun(symbol const & s, unsigned n_args, sort *const * args, sort * range, bool is_generated);
 
+        bool has_def(func_decl* f) const {
+            return m_plugin->has_def(f);
+        }
+
         def& get_def(func_decl* f) {
-            SASSERT(m_plugin->has_def(f));
+            SASSERT(has_def(f));
             return m_plugin->get_def(f);
         }
 

src/ast/rewriter/recfun_rewriter.cpp

@@ -26,6 +26,8 @@ br_status recfun_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr *
             if (!m.is_value(args[i]))
                 return BR_FAILED;
         }
+        if (!m_rec.has_def(f))
+            return BR_FAILED;
         recfun::def const& d = m_rec.get_def(f);
         if (!d.get_rhs())
             return BR_FAILED;