Function z3_sys::Z3_mk_int_sort [−][src]
pub unsafe extern "C" fn Z3_mk_int_sort(c: Z3_context) -> Z3_sort
Expand description
Create the integer type.
This type is not the int type found in programming languages.
A machine integer can be represented using bit-vectors. The function
Z3_mk_bv_sort
creates a bit-vector type.