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.
CVSS Details
- CVSS 3.1 Base Score: 7.8
- CVSS 3.1 Vector: (CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H)
Prioritise with Active Threat Intelligence
With curated Threat Intelligence, you can see which vulnerabilities truly put you at risk, prioritize what matters most, and act before attackers do.
Explore Intelligence Hub