Function z3_sys::Z3_get_numeral_small

pub unsafe extern "C" fn Z3_get_numeral_small(
    c: Z3_context, 
    a: Z3_ast, 
    num: *mut c_longlong, 
    den: *mut c_longlong
) -> Z3_bool

Return numeral value, as a pair of 64 bit numbers if the representation fits.

• c: logical context.
• a: term.
• num: numerator.
• den: denominator.

Return Z3_TRUE if the numeral value fits in 64 bit numerals, Z3_FALSE otherwise.

Precondition: Z3_get_ast_kind(a) == AstKind::Numeral