mk
Create BitVec arithmetic signed mod (bvsmod) expression.
Computes remainder of a floor (round toward negative infinity) division. The result sign matches the arg1 sign.
For example: 47 bvsmod 13 = 8 47 bvsmod -13 = -5 -47 bvsmod 13 = 5 -47 bvsmod -13 = -8