Practical Sessions


Informations for Practical Sessions

SAT (Gilles Audemard / Armin Biere / Marijn Heule)

The SAT session requires a C programming environment (gcc / clang, make, standard command-line utilities) and will show how to encode problems to the Glucose and Picosat solvers. Both, the exercises and the solvers are available for download as zip archive and as tar.gz archive. The README contains detailed instructions but a simple “make” should suffice.

SMT (Aina Niemetz / Mathias Preiner)

In this session we will use PySMT ( Students are encouraged to install PySMT with support for various SMT solvers prior to the session. You can find installation instructions for PySMT at We recommend to install at least the solvers MathSAT (pysmt-install –msat), Boolector (pysmt-install –btor), CVC4 (pysmt-install –cvc4), and Z3 (pysmt-install –z3). For those who do not want to install PySMT locally the organizers have prepared this Virtualbox image (the username/password is satsmt/satsmt). Alternatively, if you prefer to use Docker, you can find instructions on how to build a docker image with the full PySMT environment here:

The login for the virtual machine is user satsmt with password satsmt .

Automated Reasoning (Martin Suda)

This session will use Vampire. From the website you can find both binaries and the GitHub page where you can download the source and run “make vampire_rel” to make Vampire. To compile with Z3 you will need to first install Z3. Again, we encourage students to install this themselves beforehand but it will also be included in the above virtual machine.