Function z3_sys::Z3_mk_extract
source · pub unsafe extern "C" fn Z3_mk_extract(
c: Z3_context,
high: c_uint,
low: c_uint,
t1: Z3_ast
) -> Z3_ast
Expand description
Extract the bits high
down to low
from a bit-vector of
size m
to yield a new bit-vector of size n
, where n = high - low + 1
.
The node t1
must have a bit-vector sort.