[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

[Nuno Lopes via Phabricator via cfe-commits]

nlopes added a comment.

Regarding incremental solving with Z3 (or with most SMT solvers in general), let me just lower the expectations a bit:
In Z3, when you do push(), there are a few things that change immediately: 1) it uses a different SAT solver (one that supports incremental reasoning), and 2) some preprocessing steps are disabled completely.
The advantage of incremental solving is that it shares the state of the SAT solver between queries. On the other hand, Z3 disables a bunch of nice preprocessors, and also it switches to eager bit-blasting.  So whether going incremental pays off, it depends..  I've seen cases where it's faster to create a new solver for each query and cases where incremental is a good thing.
It's on our plans to "fix" Z3 to do better preprocessing in incremental mode, but there's no ETA at the moment to start this work..


https://reviews.llvm.org/D28952