mk_bvashr method

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

\brief 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 \c t1 and \c t2 must have the same bit-vector sort.

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

Implementation

Z3_ast mk_bvashr(
  Z3_context c,
  Z3_ast t1,
  Z3_ast t2,
) {
  return _mk_bvashr(
    c,
    t1,
    t2,
  );
}