Description
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 (1)
Core 1
Core References
Exploit, Issue Tracking, Patch, Third Party Advisory
https://github.com/Z3Prover/z3/issues/3363
Scores
CVSS v3
7.8
EPSS
0.0089
EPSS Percentile
55.0%
Attack Vector
LOCAL
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H
CISA SSVC
Vulnrichment
Exploitation
poc
Automatable
no
Technical Impact
total
Details
CWE
CWE-416
Status
published
Products (1)
microsoft/z3
< 4.8.8
Published
Aug 22, 2023
Tracked Since
Feb 18, 2026