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

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added a comment.

In https://reviews.llvm.org/D45517#1116734, @george.karpenkov wrote:

> @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.


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?
(Since the visitor is running backward we will add s > 20 constraint first, but this should be irrelevant for the deduplication I guess.)

> @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.

Seams reasonable.


https://reviews.llvm.org/D45517