CVE-2020-19725

Source
https://nvd.nist.gov/vuln/detail/CVE-2020-19725
Import Source
https://storage.googleapis.com/cve-osv-conversion/osv-output/CVE-2020-19725.json
JSON Data
https://api.osv.dev/v1/vulns/CVE-2020-19725
Related
Published
2023-08-22T19:16:04Z
Modified
2025-01-14T08:37:26.188248Z
Severity
  • 7.8 (High) CVSS_V3 - CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H CVSS Calculator
Summary
[none]
Details

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.

References

Affected packages

Git / github.com/z3prover/z3

Affected ranges

Type
GIT
Repo
https://github.com/z3prover/z3
Events
Introduced
0 Unknown introduced commit / All previous commits are affected
Fixed

Affected versions

Other

Nightly
last-pure-pure
last-pure-unstable

Z3-4.*

Z3-4.8.5

z3-4.*

z3-4.1.1
z3-4.3.0
z3-4.3.1
z3-4.3.2
z3-4.4.0
z3-4.4.1
z3-4.5.0
z3-4.6.0
z3-4.7.1
z3-4.8.1
z3-4.8.3
z3-4.8.4
z3-4.8.6
z3-4.8.7