Function z3_sys::Z3_mk_bv2int

pub unsafe extern "C" fn Z3_mk_bv2int(
    c: Z3_context,
    t1: Z3_ast,
    is_signed: Z3_bool
) -> Z3_ast

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.