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

[Ryan Govostes via Phabricator via cfe-commits]

rgov added a comment.

Do you think you could upload the patch omitting all of the test case changes for now? Maybe include one as an example but it seems to be just adding `%z3_cc1` so we don't need to see all of them right now.

The KLEE project has a useful abstraction layer around multiple bitvector solvers (Boolector, CVC4, STP, and Z3). It's also used by Souper, another LLVM-based project. I would encourage you to consider using that rather than interacting directly with a specific solver.

For what it's worth, here's my attempt <http://lists.llvm.org/pipermail/cfe-dev/attachments/20130307/f53766b7/attachment.obj> at integrating STP.


https://reviews.llvm.org/D28952