[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference

[Balogh, Ádám via Phabricator via cfe-commits]

baloghadamsoftware added a comment.

Sorry, Artem, but it does not work this way. Even if the symbolic expressions are constrained to `[-MAX/4..MAX/4]`, after rearrangement the difference still uses the whole range, thus `m>n` becomes `m-n>0`, where in the false branch the range for `m-n` is `[MIN..0]`. Then if we check `n>=m` the range set is reversed to `[MIN..MIN]U[0..MAX]` which results `UNKNOWN` for `n-m`. It does not solve any of our problems and there is no remedy on the checker's side.


https://reviews.llvm.org/D35110