Function z3_sys::Z3_mk_bvlshr

source ·

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

Expand description

Logical shift right.

It is equivalent to unsigned division 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.