Function z3_sys::Z3_mk_fpa_numeral_int_uint

pub unsafe extern "C" fn Z3_mk_fpa_numeral_int_uint(
    c: Z3_context,
    sgn: Z3_bool,
    exp: c_int,
    sig: c_uint,
    ty: Z3_sort
) -> Z3_ast

Create a numeral of FloatingPoint sort from a sign bit and two integers.

• c: logical context
• sgn: sign bit (true == negative)
• sig: significand
• exp: exponent
• ty: result sort

ty must be a FloatingPoint sort

See also:

• Z3_mk_numeral