z3
Version: 4.16.0The Z3 Theorem Prover
What is z3?
The Z3 Theorem Prover
How to use this package
Quick install
Installs the package into the current environment for this session. Use --build or --runtime to persist it as a build-time or runtime dependency.
min add z3Declare as a task dependency in minimal.toml
Listing the package under tasks.<name>.packages makes it available inside that task’s sandbox.
[tasks.dev]
packages = ["z3"]Build-time vs runtime
Choose build-time for tools needed during compilation, runtime for dynamic libraries loaded at runtime.
min add --build z3
min add --runtime z3No direct advisories
This package inherits 4 transitive advisories from its dependencies.
Showing 4 transitive advisories via z3's dependencies
No advisories match the current filters.
| Status | IDs | Package | Severity | |||
|---|---|---|---|---|---|---|
| Critical ( 0 ) | ||||||
| High ( 3 ) | ||||||
| Affected: 2.42 | glibc | High: 7.5 | ||||
SummaryNo summary published for this advisory. Via: glibc Affected ranges
CVSS vector:
References | ||||||
| Affected: 2.42 | glibc | High: 7.5 | ||||
SummaryNo summary published for this advisory. Via: glibc Affected ranges
CVSS vector:
References | ||||||
| Affected: 2.42 | glibc | High: 8.4 | ||||
SummaryNo summary published for this advisory. Via: glibc Affected ranges
CVSS vector:
| ||||||
| Medium ( 1 ) | ||||||
| Affected: 15.2.0 | gcc | Medium: 4.8 | ||||
Summary**DISPUTED**A failure in the -fstack-protector feature in GCC-based toolchains that target AArch64 allows an attacker to exploit an existing buffer overflow in dynamically-sized local variables in your application without this being detected. This stack-protector failure only applies to C99-style dynamically-sized local variables or those created using alloca(). The stack-protector operates as intended for statically-sized local variables. The default behavior when the stack-protector detects an overflow is to terminate your application, resulting in controlled loss of availability. An attacker who can exploit a buffer overflow without triggering the stack-protector might be able to change program flow control to cause an uncontrolled loss of availability or to go further and affect confidentiality or integrity. NOTE: The GCC project argues that this is a missed hardening bug and not a vulnerability by itself. Via: gcc Affected ranges
CVSS vector:
| ||||||
| Low ( 0 ) | ||||||
| Unknown ( 0 ) | ||||||
56 components
No components match your filter.
| Packages | Version |
|---|---|
| z3 ROOT | 4.16.0 |
| acl | 2.3.2 |
| attr | 2.5.2 |
| autoconf | 2.73 |
| automake | 1.18.1 |
| bash | 5.3 |
| bash-bootstrap | 5.3 |
| binutils | 2.46.1 |
| bison | 3.8.2 |
| bzip2 | 1.0.8 |
| cmake | 4.2.3 |
| coreutils | 9.11 |
| curl | 8.20.0 |
| diffutils | 3.12 |
| expat | 2.7.5 |
| file | 5.47 |
| findutils | 4.10.0 |
| flex | 2.6.4 |
| gawk | 5.4.0 |
| gawk-bootstrap | 5.3.2 |
| gcc | 15.2.0 |
| gdbm | 1.26 |
| glibc | 2.42 |
| gmp | 6.3.0 |
| grep | 3.12 |
| gzip | 1.14 |
| libcap | 2.78 |
| libffi | 3.5.2 |
| libidn2 | 2.3.8 |
| libpsl | 0.21.5 |
| libtool | 2.5.4 |
| libunistring | 1.4.1 |
| libuv | 1.52.1 |
| linux_headers | 6.12.43 |
| lz4 | 1.10.0 |
| m4 | 1.4.21 |
| make | 4.4.1 |
| meson | 1.10.1 |
| mpc | 1.4.0 |
| mpfr | 4.2.2 |
| ncurses | 6.5-20250830 |
| ninja | 1.13.2 |
| openssl | 3.6.2 |
| pcre2 | 10.47 |
| perl | 5.42.0 |
| pkgconf | 2.5.1 |
| python | 3.14.5 |
| readline | 8.3 |
| sed | 4.9 |
| setuptools | 82.0.1 |
| sqlite | 3.50.4 |
| tar | 1.35 |
| util-linux | 2.42.1 |
| xz | 5.8.3 |
| zlib | 1.3.2 |
| zstd | 1.5.7 |