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.


https://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2020-19725
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.
2023-08-22T19:16:04Z

Source: CVEAnnouncements
Source Link: https://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2020-19725