mk
Create BitVec rotate right (rotateright) expression. The result expression is rotated right rotation times.
See also
for the rotation by a symbolic (any BitVec expression) number of bits.