mk_int_symbol method

Z3_symbol mk_int_symbol(
  1. Z3_context c,
  2. int i
)

\brief Create a Z3 symbol using an integer.

Symbols are used to name several term and type constructors.

NB. Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1.

\sa Z3_get_symbol_int \sa Z3_mk_string_symbol

def_API('Z3_mk_int_symbol', SYMBOL, (_in(CONTEXT), _in(INT)))

Implementation

Z3_symbol mk_int_symbol(
  Z3_context c,
  int i,
) {
  return _mk_int_symbol(
    c,
    i,
  );
}