https://gcc.gnu.org/bugzilla/show_bug.cgi?id=109194
--- Comment #1 from David Malcolm <dmalcolm at gcc dot gnu.org> --- Well, strictly speaking not all of these are true; consider a == INT_MAX b == INT_MAX - 1 Then a > b, but: * a + 1 is, I believe, undefined, but we may want to treat it as INT_MIN * b + 1 is INT_MAX * with those semantics, a + 1 > b + 1 is INT_MIN > INT_MAX which is false ...and you can pick other values for b e.g. INT_MAX - 2 to get other results. The constraint manager code is playing rather fast-and-loose in places. I've been experimenting with adding an SMT solver (PR 104940) which would support figuring out such cases precisely based on bit-vectors.
