From fa1197a78f0469ca7eeacc904c95d6bbbf695369 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Apr 2020 13:51:25 -0700
Subject: [PATCH] fix #4155

---
 src/ast/recfun_decl_plugin.h         | 6 +++++-
 src/ast/rewriter/recfun_rewriter.cpp | 2 ++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index 4536f5f99..dec589bd1 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/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);
         }
 
diff --git a/src/ast/rewriter/recfun_rewriter.cpp b/src/ast/rewriter/recfun_rewriter.cpp
index b639bea0f..f22830e80 100644
--- a/src/ast/rewriter/recfun_rewriter.cpp
+++ b/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;