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

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

In https://reviews.llvm.org/D45517#1074422, @rnkovacs wrote:

> In https://reviews.llvm.org/D45517#1074057, @NoQ wrote:
>
> > 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.
>
>
> Won't collecting all constraints and solving a ~100ish equations at once take a long time? Maybe the timeout limit for Z3 will need to be slightly increased for refutation then.


Well, in the worst case we would still be able to split our full system of equations into smaller chunks, and it'd most likely still be better than solving roughly-the-same system of equations ~100ish times.


https://reviews.llvm.org/D45517