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

Dan Liew via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Fri Mar 31 07:37:30 PDT 2017


delcypher added inline comments.


================
Comment at: CMakeLists.txt:188
 
+find_package(Z3 4.5)
+
----------------
ddcc wrote:
> delcypher wrote:
> > delcypher wrote:
> > > @ddcc It is of course up to you but I recently [[ added support for using `libz3` directly | added support for using `libz3` directly ]] from CMake. via it's own CMake config package. You only get this if Z3 was built with CMake so you might not want this restriction.  This feature has only just landed though and might not be sufficient for your needs.  If you take a look at Z3's example projects they are now built with this mechanism when building with CMake.
> > > 
> > > If you are interested I'd be more than happy to work with you to get this feature ready for your needs in upstream Z3 so you can use it here.
> > Sorry that URL should be https://github.com/Z3Prover/z3/pull/926
> I think this is useful, and upstream z3 has been in need of better packaging. But until it's used by default over the current python script and the z3 folks actively maintain it, I'm a little hesitant to depend on it.
@ddcc Sure your reasoning makes sense.


https://reviews.llvm.org/D28952





More information about the cfe-commits mailing list