https://gcc.gnu.org/bugzilla/show_bug.cgi?id=101254
--- Comment #6 from Jakub Jelinek <jakub at gcc dot gnu.org> --- Well, from x > y signed -fwrapv you can assume x - y to be ~[0, 0] (from x >= y nothing). It is similar to unsigned, though in that case there are no negative values and so for x >= y x - y [0, max] is the actually VARYING and for x > y x - y [1, max] is the same thing as ~[0, 0].