[PATCH] D78457: [analyzer][Z3-refutation] Fix refutation BugReporterVisitor bug and refactor

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

In D78457#1991288 <https://reviews.llvm.org/D78457#1991288>, @xazax.hun wrote:

> > As turned out we don't even need a BugReporterVisitor for doing the crosscheck.
> >  We should simply use the constraints of the ErrorNode since that has all the necessary information.
>
> This should not be true. But we should definitely have a test case that proves this. The main idea is that unused symbols can be garbage collected. The problem is that the ErrorNode does not have any information about the symbols that were garbage collected earlier. This is why we need the visitor.


If a symbol is unused and garbage collected then that is not part of the path constraint that leads to the ErrorNode, is it? So why should we care about constraints on an unused symbol?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D78457/new/

https://reviews.llvm.org/D78457