mk_int2bv method

Z3_ast mk_int2bv(
  1. Z3_context c,
  2. int n,
  3. Z3_ast t1
)

\brief Create an \c n bit bit-vector from the integer argument \c t1.

The resulting bit-vector has \c n bits, where the i'th bit (counting from 0 to \c n-1) is 1 if \c (t1 div 2^i) mod 2 is 1.

The node \c t1 must have integer sort.

def_API('Z3_mk_int2bv', AST, (_in(CONTEXT), _in(UINT), _in(AST)))

Implementation

Z3_ast mk_int2bv(
  Z3_context c,
  int n,
  Z3_ast t1,
) {
  return _mk_int2bv(
    c,
    n,
    t1,
  );
}