[PATCH] D45517: [analyzer] False positive refutation with Z3

[George Karpenkov via Phabricator via cfe-commits]

george.karpenkov added a comment.

> I am not not sure that I got the idea what are you suggesting here. If we have the constraint of for example a symbol s > 10 and later on a path we discover s > 20, will we also deduplicate this that way?

No. But I thought in your optimization atoms inside the constraints would be the same?
Could you give an example where they are not?


https://reviews.llvm.org/D45517