mk
Create BitVec sub-no-overflow check expression. Determines that BitVec arithmetic subtraction does not overflow. An overflow occurs when the subtraction result value is greater than max supported value.
See also
for the underflow check.