[PATCH] D49536: [Analyzer] Quick Fix for exponential execution time when simpilifying complex additive expressions

[Artem Dergachev via Phabricator via llvm-commits]

NoQ added a comment.

The "Assuming..." diagnostic piece isn't the same as "Taking true/false branch" diagnostic piece. The former indicates that a constraint is added. The latter indicate how the path flows between program points.

The absence of "Assuming..." indicates that Z3 didn't need to make an assumption; it already knew that the condition is true.

I understand how Z3 could figure this out. Indeed, 5 + (y + 1) + (y + 1) = 2y+7 is an odd number, and therefore it cannot be equal to 0.

I don't understand how our rearrangement could figure this out. Might it have been an incorrect rearrangement?

In any case, it is clear that both behaviors are currently correct and the test needs to be updated to reflect the Z3's superpower. I suggest using FileCheck's `-check-prefixes=` to highlight the difference. See `cfg-rich-constructors.cpp` for an example of how to use those.


Repository:
  rL LLVM

https://reviews.llvm.org/D49536