mk
Create BitVec add-no-underflow check expression. Determines that BitVec arithmetic addition does not underflow. An underflow occurs when the addition result value is lower than min supported value.
See also
for the overflow check.