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

Fri, 04 Oct 2024 16:30:00 +0000

Type Values Removed Values Added
Metrics ssvc

{'options': {'Automatable': 'no', 'Exploitation': 'poc', 'Technical Impact': 'total'}, 'version': '2.0.3'}


cve-icon MITRE

Status: PUBLISHED

Assigner: mitre

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

Updated: 2024-10-04T16:07:10.602Z

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

Link: CVE-2020-19725

cve-icon Vulnrichment

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

cve-icon NVD

Status : Modified

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

Modified: 2024-11-21T05:09:22.383

Link: CVE-2020-19725

cve-icon Redhat

No data.