mk_bv_sort method

Z3_sort mk_bv_sort(
  1. Z3_context c,
  2. int sz
)

\brief Create a bit-vector type of the given size.

This type can also be seen as a machine integer.

\remark The size of the bit-vector type must be greater than zero.

def_API('Z3_mk_bv_sort', SORT, (_in(CONTEXT), _in(UINT)))

Implementation

Z3_sort mk_bv_sort(
  Z3_context c,
  int sz,
) {
  return _mk_bv_sort(
    c,
    sz,
  );
}