<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">Hi all,<div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><div><br></div><div>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.</div><div><br></div><div>Thank you,</div><div><br></div><div>[0] <span class="gmail-gr_ gmail-gr_1871 gmail-gr-alert gmail-gr_spell gmail-gr_inline_cards gmail-gr_run_anim gmail-ContextualSpelling" id="gmail-1871" style="display:inline;border-bottom:2px solid transparent;background-repeat:no-repeat">llvm</span>/include/<span class="gmail-gr_ gmail-gr_122 gmail-gr-alert gmail-gr_spell gmail-gr_inline_cards gmail-gr_disable_anim_appear gmail-ContextualSpelling" id="gmail-122" style="display:inline;border-bottom:2px solid transparent;background-repeat:no-repeat">llvm</span>/Support/SMTAPI.h</div><div>[1] <a href="https://github.com/mikhailramalho/clang">https://github.com/mikhailramalho/clang</a></div><div>[2] clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h</div><div><br></div>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div></div></div></div></div></div></div></div>