Function z3_sys::Z3_mk_fpa_numeral_int

source · 
pub unsafe extern "C" fn Z3_mk_fpa_numeral_int(
    c: Z3_context,
    v: c_int,
    ty: Z3_sort
) -> Z3_ast
Expand description

Create a numeral of FloatingPoint sort from a signed integer.

  • c: logical context
  • v: value
  • ty: result sort

ty must be a FloatingPoint sort

See also: