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
History

No history.

cve-icon MITRE

Status: PUBLISHED

Assigner: mitre

Published: 2023-08-22T00:00:00

Updated: 2024-08-04T14:15:28.571Z

Reserved: 2020-08-13T00:00:00

Link: CVE-2020-19725

cve-icon Vulnrichment

No data.

cve-icon NVD

Status : Analyzed

Published: 2023-08-22T19:16:04.567

Modified: 2023-08-25T02:46:10.523

Link: CVE-2020-19725

cve-icon Redhat

No data.