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
Link | Resource |
---|---|
https://github.com/Z3Prover/z3/issues/3363 | Exploit Issue Tracking Patch Third Party Advisory |
History
No history.
MITRE Information
Status: PUBLISHED
Assigner: mitre
Published: 2023-08-22T00:00:00
Updated: 2023-08-22T15:44:46.204301
Reserved: 2020-08-13T00:00:00
Link: CVE-2020-19725
JSON object: View
NVD Information
Status : Analyzed
Published: 2023-08-22T19:16:04.567
Modified: 2023-08-25T02:46:10.523
Link: CVE-2020-19725
JSON object: View
Redhat Information
No data.
CWE