From 8d81a2dcaf4de007ce587f396f1b48fbc29646dd Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sat, 29 Mar 2025 17:02:32 +0000 Subject: [PATCH] Note that Z3_get_numeral_small is essentially redundant (#7599) * Check that Z3_get_numeral_small is given non-null out params Analogous to other Z3_get_numeral_* functions with out params. * Note that Z3_get_numeral_small is essentially redundant The error behavior of Z3_get_numeral_small does not follow the pattern of the other functions. The functions that have out params and return a bool indicating success (such as Z3_get_numeral_rational_int64) return false rather than signaling an error when given an unsupported expression argument (such as a rounding mode value). The functions that do not have out params signal an error in such cases. Z3_get_numeral_small is the odd one out in that it signals errors and returns a status bool. This error handling is the only difference between Z3_get_numeral_small and Z3_get_numeral_rational_int64, so this patch adds a comment to the documentation. --- src/api/api_numeral.cpp | 4 ++++ src/api/z3_api.h | 2 ++ 2 files changed, 6 insertions(+) diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 614395240..cee60272e 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -318,6 +318,10 @@ extern "C" { LOG_Z3_get_numeral_small(c, a, num, den); RESET_ERROR_CODE(); CHECK_IS_EXPR(a, false); + if (!num || !den) { + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); + return false; + } rational r; bool ok = Z3_get_numeral_rational(c, a, r); if (ok) { diff --git a/src/api/z3_api.h b/src/api/z3_api.h index daf14ae71..dafc26881 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5109,6 +5109,8 @@ extern "C" { Return \c true if the numeral value fits in 64 bit numerals, \c false otherwise. + Equivalent to \c Z3_get_numeral_rational_int64 except that for unsupported expression arguments \c Z3_get_numeral_small signals an error while \c Z3_get_numeral_rational_int64 returns \c false. + \pre Z3_get_ast_kind(a) == Z3_NUMERAL_AST def_API('Z3_get_numeral_small', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _out(INT64)))