mk
open fun <T : KBvSort> mkBvRotateRightIndexedExprNoSimplify(rotation: Int, value: KExpr<T>): KBvRotateRightIndexedExpr<T>
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.