This will fail to verify since the verification does not assume the withinRange property, which is needed to prevent signed integer underflow or overflow.