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.

cve-icon 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

cve-icon 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

cve-icon Redhat Information

No data.

CWE