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://github.com/microsoft/AzureLinuxVulnerabilityData/blob/main/osv/AZL-27991.json"