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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
