From d30ba3f1adfb84d00b5db660d30da4748a28ff6a Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 11 May 2016 14:30:37 +0100 Subject: [PATCH] change Z3_get_decl_kind API to correctly identify OP_B*_I and OP_B*_NO_OVFL instead of returning Z3_OP_UNINTERPRETED --- src/api/api_ast.cpp | 17 ++++++++--------- src/api/z3_api.h | 9 +++++++++ 2 files changed, 17 insertions(+), 9 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 34dab3ed6..9aea9d6f4 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1066,15 +1066,14 @@ extern "C" { case OP_BV2INT: return Z3_OP_BV2INT; case OP_CARRY: return Z3_OP_CARRY; case OP_XOR3: return Z3_OP_XOR3; - case OP_BSMUL_NO_OVFL: - case OP_BUMUL_NO_OVFL: - case OP_BSMUL_NO_UDFL: - case OP_BSDIV_I: - case OP_BUDIV_I: - case OP_BSREM_I: - case OP_BUREM_I: - case OP_BSMOD_I: - return Z3_OP_UNINTERPRETED; + case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL; + case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL; + case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL; + case OP_BSDIV_I: return Z3_OP_BSDIV_I; + case OP_BUDIV_I: return Z3_OP_BUDIV_I; + case OP_BSREM_I: return Z3_OP_BSREM_I; + case OP_BUREM_I: return Z3_OP_BUREM_I; + case OP_BSMOD_I: return Z3_OP_BSMOD_I; default: UNREACHABLE(); return Z3_OP_UNINTERPRETED; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 7c846cc99..9d89bc957 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1060,6 +1060,15 @@ typedef enum { Z3_OP_CARRY, Z3_OP_XOR3, + Z3_OP_BSMUL_NO_OVFL, + Z3_OP_BUMUL_NO_OVFL, + Z3_OP_BSMUL_NO_UDFL, + Z3_OP_BSDIV_I, + Z3_OP_BUDIV_I, + Z3_OP_BSREM_I, + Z3_OP_BUREM_I, + Z3_OP_BSMOD_I, + // Proofs Z3_OP_PR_UNDEF = 0x500, Z3_OP_PR_TRUE,