Function z3_sys::Z3_mk_bv2int [−][src]
pub unsafe extern "C" fn Z3_mk_bv2int(
c: Z3_context,
t1: Z3_ast,
is_signed: bool
) -> Z3_ast
Expand description
Create an integer from the bit-vector argument t1
.
If is_signed
is false, then the bit-vector t1
is treated as unsigned.
So the result is non-negative
and in the range [0..2^N-1]
, where N are the number of bits in t1
.
If is_signed
is true, t1
is treated as a signed bit-vector.
The node t1
must have a bit-vector sort.