From c8a83749ddd0db0a4b54c7f5a20a0fffdedfd27e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 16 Aug 2021 11:19:22 -0700
Subject: [PATCH] #5484

---
 src/api/api_ast.cpp | 5 +++++
 src/ast/ast_pp.h    | 3 +++
 2 files changed, 8 insertions(+)

diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 0d9b00351..3a909bda6 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -137,6 +137,11 @@ extern "C" {
         func_decl* d = to_func_decl(f);
         ast_manager& m = mk_c(c)->m();
         recfun::decl::plugin& p = mk_c(c)->recfun().get_plugin();
+        if (!p.has_def(d)) {
+            std::string msg = "function " + mk_pp(d, m) + " needs to be defined using rec_func_decl";
+            SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
+            return;
+        }
         expr_ref abs_body(m);
         expr_ref_vector _args(m);
         var_ref_vector _vars(m);
diff --git a/src/ast/ast_pp.h b/src/ast/ast_pp.h
index 1b3ca4a81..7ccb8ec15 100644
--- a/src/ast/ast_pp.h
+++ b/src/ast/ast_pp.h
@@ -67,4 +67,7 @@ inline std::string operator+(std::string const& s, mk_pp const& pp) {
     return strm.str();
 }
 
+inline std::string& operator+=(std::string& s, mk_pp const& pp) {
+    return s = s + pp;
+}