mk_bvlshr method

Z3_ast mk_bvlshr(
  1. Z3_context c,
  2. Z3_ast t1,
  3. Z3_ast t2
)

\brief Logical shift right.

It is equivalent to unsigned division by \ccode{2^x} where \c 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 \c t1 and \c t2 must have the same bit-vector sort.

def_API('Z3_mk_bvlshr', AST, (_in(CONTEXT), _in(AST), _in(AST)))

Implementation

Z3_ast mk_bvlshr(
  Z3_context c,
  Z3_ast t1,
  Z3_ast t2,
) {
  return _mk_bvlshr(
    c,
    t1,
    t2,
  );
}