mk_int64 method

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

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

This function can be used to create numerals that fit in a machine \c int64_t 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_int64', AST, (_in(CONTEXT), _in(INT64), _in(SORT)))

Implementation

Z3_ast mk_int64(
  Z3_context c,
  int v,
  Z3_sort ty,
) {
  return _mk_int64(
    c,
    v,
    ty,
  );
}