Function z3_sys::Z3_mk_bvshl
source · pub unsafe extern "C" fn Z3_mk_bvshl(
c: Z3_context,
t1: Z3_ast,
t2: Z3_ast
) -> Z3_ast
Expand description
Shift left.
It is equivalent to multiplication by 2^x
where x
is the value of the
third argument.
NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.
The nodes t1
and t2
must have the same bit-vector sort.