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;