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

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

In https://reviews.llvm.org/D28952#659728, @nlopes wrote:

> Let me give just 2 more Z3-related suggestions:
>
> - instead of re-creating the solver, it might be faster to do Z3_solver_reset
> - "once in a while" it might be helpful to delete everything (all solvers, asts, context) and call Z3_reset_memory.  Z3's small object pool is not very good and keeps growing /ad infinitum/, so cleaning it up once a while is a good thing (improves cache usage and reduces memory consumption).
>
>   BTW, you may want to call Z3_finalize_memory at exit to keep clang valgrind/asan-clean.  (Z3 keeps a lot of internal buffers otherwise)


Thanks, the most recent revision now reuses the solver object, and frees Z3 memory at exit. I'm skipping the reset memory part for now, because my understanding is that a new instance of `clang -cc1` will be spun up for each compilation unit anyway, and it'd be tricky to find a suitable point to do that while maintaining consistency.

On the testsuite, the runtime is now down to 185 secs, and a valgrind test is much cleaner.


https://reviews.llvm.org/D28952