Home

ScalaZ3 is a library to use the Z3 SMT Solver with the Scala programming language. It is developed primarily at EPFL, but contributions from everyone are welcome.

The API for ScalaZ3 is available at http://lara.epfl.ch/~psuter/ScalaZ3/api/. Some older documentation is also hosted at EPFL on this page.

A paper (system description) describes some implementation details and was presented at CADE 2011. The reference is:

Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. Scala to the Power of Z3: Integrating SMT and Programming. CADE 2011, pp. 400-406.

A Java API binding has since been published in the [https://github.com/Z3Prover/z3](Z3 repository). This binding relies on Java finalizers to perform GC which is unfortunately unreliable for our use cases. ScalaZ3 3.0 tries to get the best of both worlds by relying on the automatically generated (and hopefully maintained) JNI binding provided by Z3 but relies on a free-buffer for more predictable GC.