From 80731ef364cd7f89e98b3fc452c9cc453880b87d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 20 May 2016 19:40:45 +0100 Subject: [PATCH] Exposed OP_FPA_MIN/MAX_I to the API --- src/api/api_ast.cpp | 6 +++--- src/api/z3_api.h | 3 +++ 2 files changed, 6 insertions(+), 3 deletions(-) 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;