From c9fa00aec1442464c9cc2ab6f3d2e5c749232b6e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 13 Apr 2022 11:22:43 +0200
Subject: [PATCH] expose recursive functions with own op-code over API

---
 src/api/api_ast.cpp | 3 +++
 src/api/z3_api.h    | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 7ee95afc8..9f9039378 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1329,6 +1329,9 @@ extern "C" {
             }
         }
 
+        if (mk_c(c)->recfun().get_family_id() == _d->get_family_id())
+            return Z3_OP_RECURSIVE;
+
         return Z3_OP_UNINTERPRETED;
         Z3_CATCH_RETURN(Z3_OP_UNINTERPRETED);
     }
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 8a610bc6d..1388d0ab1 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -996,6 +996,8 @@ typedef enum
         information is exposed. Tools may use the string representation of the
         function declaration to obtain more information.
 
+   - Z3_OP_RECURSIVE: function declared as recursive
+
    - Z3_OP_UNINTERPRETED: kind used for uninterpreted symbols.
 */
 typedef enum {
@@ -1320,6 +1322,7 @@ typedef enum {
     Z3_OP_FPA_BV2RM,
 
     Z3_OP_INTERNAL,
+    Z3_OP_RECURSIVE,
 
     Z3_OP_UNINTERPRETED
 } Z3_decl_kind;