From e2d3f39735388768f92f4e02b90c0ed42b82f1e3 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sat, 29 Mar 2025 12:57:14 +0000 Subject: [PATCH] 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/z3_api.h | 2 ++ 1 file changed, 2 insertions(+) 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)))