Skip to content

Z3

Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types. This module includes z3-solver, the Python interface of Z3.

homepage: https://github.com/Z3Prover/z3

Available installations

Z3 version Supported CPU targets Supported GPU targets EESSI version Module
4.15.1 generic: riscv64
Arm:
AMD:
Intel:
(none) 2025.06 Z3/4.15.1-GCCcore-14.3.0

Extensions

Overview of extensions included in Z3 installations

z3_solver

z3_solver version Z3 modules that include it
4.15.1.0 Z3/4.15.1-GCCcore-14.3.0