Create BitVec rotate right (rotateright) expression. The result expression is rotated right rotation times.
rotateright
for the rotation by a known number of bits.