Function z3_sys::Z3_mk_bvashr

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

Arithmetic shift right.

It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.

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.