CVE-2020-19725

See a problem?
Please try reporting it to the source first.
Source
https://cve.org/CVERecord?id=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
Downstream
Published
2023-08-22T19:16:04.567Z
Modified
2026-04-10T04:28:08.180768Z
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
ad55a1f1c617a7f0c3dd735c0780fc758424c7f1
Database specific 
{
    "versions": [
        {
            "introduced": "0"
        },
        {
            "fixed": "4.8.8"
        }
    ]
}

Affected versions

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.6.0
z3-4.8.3
z3-4.8.6
z3-4.8.7

Database specific

source 
"https://storage.googleapis.com/cve-osv-conversion/osv-output/CVE-2020-19725.json"