Sorry, the old title didn't make sense.

You're right; there's a bug.

I proved, however, the correctness of two cases:

1) X - (0 -nuw A) -> X +nuw nsw A

2) X -nsw (0 -nsw A) -> X +nsw A

Not sure if the complexity of implementing this is worth the trouble, though.

Nuno

Thanks Nuno!

The first case is pretty rare. If (0 - a) does not unsigned overflow, then a must be 0. Right?

The second case is worth handling. I’ll send a patch soon.

Jingyue

Right! Ignore case 1); it's useless.

Nuno

Citando Jingyue Wu <jingyue@google.com>: