Function z3_sys::Z3_mk_int2bv [−][src]
pub unsafe extern "C" fn Z3_mk_int2bv(
c: Z3_context,
n: c_uint,
t1: Z3_ast
) -> Z3_ast
Expand description
Create an n
bit bit-vector from the integer argument t1
.
The resulting bit-vector has n
bits, where the i’th bit (counting
from 0
to n-1
) is 1
if (t1 div 2^i) mod 2
is 1
.
The node t1
must have integer sort.