CVE-2020-19725
HIGH 7.8EPSS 1.0%
There is a use-after-free vulnerability in file pdd_simplifier.cpp in Z3 before 4.8.8. It occurs when the solver attempt to simplify the constraints and causes unexpected memory access. It can cause segmentation faults or arbitrary code execution.
- CVSS v3.1 NVD
- 7.8 HIGH
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H - EPSS
- 1.03% chance of exploitation in the next 30 days, 63rd percentile
- Published
- 2023-08-22
- Updated
- 2024-10-04
Proof-of-concept exploits (1)
- Z3Prover/z3/issues/336312772★ · 2026-10-12