stp.BVAddNoUnderflow

stp.BVAddNoUnderflow(a, b)

The signed addition does not go below the minimum.