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

[Nuno Lopes via Phabricator via cfe-commits]

nlopes added a comment.

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)


https://reviews.llvm.org/D28952