CVE-2020-19725

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.
ProviderTypeBase ScoreAtk. VectorAtk. ComplexityPriv. RequiredVector
NISTNIST
7.8 HIGH
LOCAL
LOW
NONE
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H
mitreCNA
---
---
CVEADP
---
---
CISA-ADPADP
---
---
Base Score
CVSS 3.x
EPSS Score
Percentile: 59%
VendorProductVersion
microsoftz3
𝑥
< 4.8.8
𝑥
= Vulnerable software versions
Ubuntu logo
Ubuntu Releases
Ubuntu Product
Codename
z3
noble
needs-triage
mantic
ignored
lunar
ignored
jammy
needs-triage
focal
needs-triage
bionic
needs-triage
xenial
needs-triage
trusty
ignored
Common Weakness Enumeration
References
https://github.com/Z3Prover/z3/issues/3363
https://github.com/Z3Prover/z3/issues/3363