mk_int method

Z3_ast mk_int(
  1. Z3_context c,
  2. int v,
  3. Z3_sort ty
)

\brief Create a numeral of an int, bit-vector, or finite-domain sort.

This function can be used to create numerals that fit in a machine integer. It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.

\sa Z3_mk_numeral

def_API('Z3_mk_int', AST, (_in(CONTEXT), _in(INT), _in(SORT)))

Implementation

Z3_ast mk_int(
  Z3_context c,
  int v,
  Z3_sort ty,
) {
  return _mk_int(
    c,
    v,
    ty,
  );
}