SMT API moved to from clang to LLVM

Hi all,

As of yesterday, the SMT API was moved to LLVM [0]. Currently, only the clang static analyzer is using it, but its new location under LLVM makes it easier to use it in other projects.

The SMT API only supports Z3 right now. I have a fork with other backends (Boolector, MathSAT, Yices, and CVC4) [0], but the 5 solvers performance was basically the same, so there was no real reason to upstream them. If someone needs a specific solver, we can discuss submitting its backend for review.

The SMT API is not enabled by default; you can enable it by setting the flag -DLLVM_ENABLE_Z3_SOLVER=ON and cmake will try to find the lib Z3 in your system. If it’s not in a default location, you can pass it using the flag LLVM_Z3_INSTALL_DIR. You also need Z3 >= 4.7.1.

The API is quite basic right now and only supports encoding bit-vectors, floating-points, and some casts given a clang AST [2]. If anyone is interested in using the API and needs help and/or extra features (arrays, quantifiers, etc.), I’m happy to help.

Thank you,

[0] llvm/include/llvm/Support/SMTAPI.h
[2] clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h