mk_int_sort method

Z3_sort mk_int_sort(
  1. Z3_context c
)

\brief 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.

\sa Z3_mk_bv_sort

def_API('Z3_mk_int_sort', SORT, (_in(CONTEXT), ))

Implementation

Z3_sort mk_int_sort(
  Z3_context c,
) {
  return _mk_int_sort(
    c,
  );
}