- Description
- 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.
- Source
- cve@mitre.org
- NVD status
- Modified
CVSS 3.1
- Type
- Primary
- Base score
- 7.8
- Impact score
- 5.9
- Exploitability score
- 1.8
- Vector string
- CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H
- Severity
- HIGH
- nvd@nist.gov
- CWE-416
- Hype score
- Not currently trending
[
{
"nodes": [
{
"negate": false,
"cpeMatch": [
{
"criteria": "cpe:2.3:a:microsoft:z3:*:*:*:*:*:*:*:*",
"vulnerable": true,
"matchCriteriaId": "6D8EF4B1-776B-4405-896B-9C0EC073D347",
"versionEndExcluding": "4.8.8"
}
],
"operator": "OR"
}
]
}
]