what4-solvers

Multi-platform binary creation for solvers of the versions most suitable for use with What4, as well as tools built on top of What4, such as Cryptol, Crux, and SAW.

Binary distributions can be found at the releases page. Currently, what4-solvers offers the following solver versions:

• ABC - 99ab99bf
• Bitwuzla - 0.7.0
• Boolector - 3.2.2
• CVC4 - 1.8
• CVC5 - 1.3.1
• Yices - 2.7.0
• Z3 - 4.8.8 and 4.8.14

Built for the following operating systems:

• macOS Sequoia 15 (arm64 and x86-64)
• RedHat UBI9 (arm64 and x86-64)
• Ubuntu 22.04 (arm64 and x86-64)
• Ubuntu 24.04 (arm64 and x86-64)
• Windows Server 2022 (x86-64)

All of the binary distributions are built from CI.

Download solvers GitHub Action

For convenience, we provide a GitHub action that automatically detects OS and architecture, downloads the appropriate solver binaries from GitHub releases, and adds them to the PATH. Solvers are downloaded to the what4-solvers folder by default.

The simplest use is to add a step to your workflow:

- name: Setup what4-solvers
  uses: GaloisInc/what4-solvers@v1

To override the default values, use the with keyword:

- name: Setup what4-solvers with custom destination
  uses: GaloisInc/what4-solvers@v1
  with:
    dest: ${{ github.workspace }}/my-solvers

or

- name: Setup what4-solvers with specific release
  uses: GaloisInc/what4-solvers@main
    with:
    release: snapshot-20251112

Consult action.yml for more details.

FAQ

Why build for multiple Ubuntu versions?

We attempt to offer somewhat broad coverage of different Linux versions. To that end, we build each solver on the two most recent Ubuntu LTS releases, as well as the latest RedHat Linux. This ensures relatively complete coverage of different shared library dependencies (e.g., different glibc versions).

Why offer multiple Z3 versions?

We use Z3 as the default SMT solver in many different projects' CI, including the CI for Cryptol and SAW. Unfortunately, certain Z3 versions have been known to non-deterministically fail or time out on certain SMT queries. See, for example, this Cryptol issue regarding Z3 4.8.10 and this SAW issue regarding Z3 4.8.14. As a consequence, it is very difficult to find a single Z3 version that works reliably across all of our tools' CI.

As a compromise, we offer multiple Z3 versions so that tools can pick one that is known to work well for their particular needs. If we successfully identify a later version of Z3 that is known to work reliably across all CI configurations, we may reconsider this choice.