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.
Fixed in Linux distributions
Distributions backport fixes, so the version that fixes this vulnerability differs per release — upgrade to at least the version shown. From the distributions' security trackers and advisories.
Ubuntu
Security tracker ↗| Release | Package | Fixed in | Advisory |
|---|---|---|---|
| Ubuntu 26.10 | z3 | No fix yet | — |
| Ubuntu 26.04 LTS | z3 | No fix yet | — |
| Ubuntu 25.10 | z3 | No fix yet | — |
| Ubuntu 22.04 LTS | z3 | No fix yet | — |
| Ubuntu 20.04 LTS | z3 | No fix yet | — |
Show 2 more (older releases, extended support, other products)Fewer releases
| Release | Package | Fixed in | Advisory |
|---|---|---|---|
| Ubuntu 18.04 LTS | z3 | No fix yet | — |
| Ubuntu 16.04 LTS | z3 | No fix yet | — |
Azure Linux
| Release | Package | Fixed in | Advisory |
|---|---|---|---|
| Azure Linux 3 | z3 | 4.13.3-1 | — |
| Azure Linux 2 (CBL-Mariner) | z3 | No fix yet | — |