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

[George Karpenkov via Phabricator via cfe-commits]

george.karpenkov added a comment.

@xazax.hun

> So strictly speaking it is not a deduplication on the constraint level but on the symbol level.

Right, apologies, I was initially mistaken then.
That's not even deduplication, I would call it using the interval solver to guide the constraint selection for the SMT solver.

That makes sense, but I'm worried about tight coupling between different features, and classes of bugs which may arise due to that.
It would be great to have it in a separate patch then.


https://reviews.llvm.org/D45517