Function z3_sys::Z3_mk_bvshl

pub unsafe extern "C" fn Z3_mk_bvshl(
    c: Z3_context, 
    t1: Z3_ast, 
    t2: Z3_ast
) -> Z3_ast

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.