Z3¶
Z3 is a theorem prover from Microsoft Research.
homepage: https://github.com/Z3Prover/z3
Available installations¶
| Z3 version | Supported CPU targets | Supported GPU targets | EESSI version | Module |
|---|---|---|---|---|
| 4.12.2 | generic: aarch64, x86_64Arm: a64fx, neoverse_n1, neoverse_v1, nvidia/graceAMD: zen2, zen3, zen4Intel: haswell, skylake_avx512, sapphirerapids, icelake, cascadelake |
(none) | 2023.06 | Z3/4.12.2-GCCcore-12.2.0 |
| 4.12.2 | generic: aarch64, x86_64Arm: a64fx, neoverse_n1, neoverse_v1, nvidia/graceAMD: zen2, zen3, zen4Intel: haswell, skylake_avx512, sapphirerapids, icelake, cascadelake |
(none) | 2023.06 | Z3/4.12.2-GCCcore-12.3.0-Python-3.11.3 |
| 4.12.2 | generic: aarch64, x86_64Arm: a64fx, neoverse_n1, neoverse_v1, nvidia/graceAMD: zen2, zen3, zen4Intel: haswell, skylake_avx512, sapphirerapids, icelake, cascadelake |
(none) | 2023.06 | Z3/4.12.2-GCCcore-12.3.0 |
| 4.13.0 | generic: aarch64, x86_64Arm: a64fx, neoverse_n1, neoverse_v1, nvidia/graceAMD: zen2, zen3, zen4Intel: haswell, skylake_avx512, sapphirerapids, icelake, cascadelake |
(none) | 2025.06 | Z3/4.13.0-GCCcore-13.3.0 |
| 4.13.4 | generic: aarch64, x86_64Arm: a64fx, neoverse_n1, neoverse_v1, nvidia/graceAMD: zen2, zen3, zen4Intel: haswell, skylake_avx512, sapphirerapids, icelake, cascadelake |
(none) | 2025.06 | Z3/4.13.4-GCCcore-14.2.0 |
| 4.15.1 | generic: aarch64, x86_64Arm: a64fx, neoverse_n1, neoverse_v1, nvidia/graceAMD: zen2, zen3, zen4Intel: haswell, skylake_avx512, sapphirerapids, icelake, cascadelake |
(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.12.2.0 | Z3/4.12.2-GCCcore-12.3.0Z3/4.12.2-GCCcore-12.3.0-Python-3.11.3 |
| 4.13.0.0 | Z3/4.13.0-GCCcore-13.3.0 |
z3_solver¶
z3_solver version |
Z3 modules that include it |
|---|---|
| 4.13.4.0 | Z3/4.13.4-GCCcore-14.2.0 |
| 4.15.1.0 | Z3/4.15.1-GCCcore-14.3.0 |