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.

Author: jberdine

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

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