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.
Advisories
| Source | ID | Title |
|---|---|---|
EUVD |
EUVD-2020-11623 | 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. |
Fixes
Solution
No solution given by the vendor.
Workaround
No workaround given by the vendor.
References
| Link | Providers |
|---|---|
| https://github.com/Z3Prover/z3/issues/3363 |
|
History
Fri, 04 Oct 2024 16:30:00 +0000
| Type | Values Removed | Values Added |
|---|---|---|
| Metrics |
ssvc
|
Projects
Sign in to view the affected projects.
Status: PUBLISHED
Assigner: mitre
Published:
Updated: 2024-10-04T16:07:10.602Z
Reserved: 2020-08-13T00:00:00
Link: CVE-2020-19725
Updated: 2024-08-04T14:15:28.571Z
Status : Modified
Published: 2023-08-22T19:16:04.567
Modified: 2024-11-21T05:09:22.383
Link: CVE-2020-19725
No data.
OpenCVE Enrichment
No data.
Weaknesses
EUVD