sorawee/bitwuzla

Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations. Its name is derived from an Austrian dialect expression that can be translated as “someone who tinkers with bits”.

Bitwuzla

Bitwuzla is a Satisfiability Modulo Theories (SMT) solvers for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays, uninterpreted functions and their combinations.

If you are using Bitwuzla in your work, or if you incorporate it into software of your own, we invite you to send us a description and link to your project/software, so that we can link it as third party application on bitwuzla.github.io.

Website

More information about Bitwuzla is available at: https://bitwuzla.github.io

Documentation

Documentation for Bitwuzla is available at: https://bitwuzla.github.io/docs

Download

The latest version of Bitwuzla is available on GitHub: https://github.com/bitwuzla/bitwuzla

Build and Installation Instructions

Bitwuzla can be built on Linux and macOS. Windows support is planned and WIP.

For detailed build and installation instructions see docs/install.rst.

Contributing

Please refer to our contributing guidelines.