faq.md

FAQ

On which platforms has SMACK been tested?

Linux, OS X, and Windows/Cygwin. Based on our experience, wherever LLVM can be built, so can SMACK.

Which LLVM version is SMACK compatible with?

We note the LLVM release that the current version of SMACK has to be compiled against in our installation instructions. It is important to note that since the LLVM bitcode format is not backward compatible, SMACK is only able to process bitcode files generated using the specified LLVM release.

One of SMACK's dependencies fails to build on my system; what should I do?

You should contact the authors of that dependency (e.g., LLVM, Z3, Boogie, Corral). While some of these are only supported on certain systems (e.g., Boogie/Corral only on Windows), in practice, many, including us, have gotten them to work on other systems (e.g., Boogie/Corral on Linux & OS X).

OSX-specific Questions

Why is opt -load smack.dylib failing with an Undefined symbol error?

When LLVM is compiled and installed on OSX (with --enable-optimized), many symbols on which smack.dylib depends have been stripped from LLVM's opt executable. Configuring LLVM with --enable-keep-symbols resolves this problem.