diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 9aea9d6f4..1e421cb2e 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1183,10 +1183,10 @@ extern "C" { case OP_FPA_TO_SBV: return Z3_OP_FPA_TO_SBV; case OP_FPA_TO_REAL: return Z3_OP_FPA_TO_REAL; case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV; + case OP_FPA_INTERNAL_MIN_I: return Z3_OP_FPA_MIN_I; + case OP_FPA_INTERNAL_MAX_I: return Z3_OP_FPA_MAX_I; + case OP_FPA_INTERNAL_RM_BVWRAP: case OP_FPA_INTERNAL_BVWRAP: - case OP_FPA_INTERNAL_BVUNWRAP: - case OP_FPA_INTERNAL_MIN_I: - case OP_FPA_INTERNAL_MAX_I: case OP_FPA_INTERNAL_MIN_UNSPECIFIED: case OP_FPA_INTERNAL_MAX_UNSPECIFIED: case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 9d89bc957..114490015 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1214,6 +1214,9 @@ typedef enum { Z3_OP_FPA_TO_IEEE_BV, + Z3_OP_FPA_MIN_I, + Z3_OP_FPA_MAX_I, + Z3_OP_UNINTERPRETED } Z3_decl_kind;