This is a tangent to D59386, which got me thinking about the performance of this code...
We're already computing the known bits of the operands here. If the known bits of the operands can determine the sign bit of the result, we'll already catch this in the ripple logic. The only other way (and as the comment already indicates) we'll get new information from computing known bits on the whole add, is if there's an assumption on it.
As such, we change the code to only compute known bits from assumptions, instead of computing full known bits on the add (which would unnecessarily recompute the known bits of the operands as well).
Let's make this comment include more of the description/discussion from this review, so we have it inline in the code. So add something like:
We already calculated the known bits of each operand and checked for ripple. The only other way to improve on the known bits is from an assumption, so call that directly.