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) {

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 https://en.m.wikipedia.org/wiki/Transitive_relation [2] https://github.com/gcc-mirror/gcc/commit/50ddbd0282e06614b29f0d3f3be5fbe70085a8bd https://github.com/gcc-mirror/gcc/commit/50ddbd0282e06614b29...