The flag applies the transitive property[1] when propagating constraints. This gives more accurate results, but at the cost of analyzer speed.
if (4 < x) {
if (x < y) {
if (y == 0) {
// Unreachable since the above three conditions cannot
// all be true at the same time (without multithreading).
}
}
}
For a more detailed explanation, see [2]. (Also the inspiration for the above example.)
[1] https://en.m.wikipedia.org/wiki/Transitive_relation
[2] https://github.com/gcc-mirror/gcc/commit/50ddbd0282e06614b29...