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)))