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

[George Karpenkov via Phabricator via cfe-commits]

george.karpenkov added a comment.

@xazax.hun (I'll reply here to avoid scattering the conversation across many subtrees)

I was thinking about the optimization for not adding redundant constraints some more, and I've decided I'm still against it ---
we are creating a higher potential for bugs, and we are tightly coupling the visitor to an internal implementation detail (all formulas are eventually purged at purge locations),
which creates a more fragile code.

The proper way to do this would be to have a set of constraints, and then add all constraints there as we iterate through the states (and through constraints inside the state).
If we use the hashing function provided by Z3, the simple act of construction of a set would implicitly drop all redundant constraints.

@mikhail.ramalho  In any case, the discussion here just further highlights that this optimization should be dropped from the initial patch, and if anything applied in a subsequent revision.


https://reviews.llvm.org/D45517