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.
Metrics
Affected Vendors & Products
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
|

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.