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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
