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

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

> The visitor currently checks states appearing as block edges in the exploded graph. The first idea was to filter states based on the shape of the exploded graph, by checking the number of successors of the parent node, but surprisingly, both `succ_size()` and `pred_size()` seemed to return 1 for each node in the graph (except for the root), even if there clearly were branchings in the code (and on the `.dot` picture). To my understanding, the exploded graph is fully constructed at the stage where visitors are run, so I must be missing something.

Aha, yep, that's probably because visitors are operating on the "trimmed" exploded graph. You can paint it via the `-trim-egraph` flag or by calling `ViewGraph(1)` in the debugger.

So, yeah, that's a good optimization that we're not invoking the solver on every node. But i don't think we should focus on improving this optimization further; instead, i think the next obvious step here is to implement it in such a way that we only needed to call the solver //once// for every report. We could simply collect all constraints from all states along the path and put them into the solver all together. This will work because symbols are not mutable and they don't reincarnate.

Apart from that, the patch seems to be going in the right direction. It should be possible to split up the `RangeSet` refactoring into a different review, for easier reviewing and better commit history.


https://reviews.llvm.org/D45517