There is a use-after-free vulnerability in file pdd_simplifier.cpp in Z3 before 4.8.8.

published 2023-08-22 3 y ago modified 2026-06-17 4 mo ago also EUVD-2020-11623

cvss: 7.8; version 3.1, NVD
cisa kev: Not listed; not in CISA's catalog
epss: 1.0%; EPSS 1.0% chance of exploitation in 30 days, percentile 64%
public exploits: 0; none known

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.

Patch / fix

fixed in 1 distros 1 links 1

microsoft z3 4.8.8

z3 Azure Linux 3.0 4.13.3-1

azure linux advisories AZL-37067

Azure Linux vulnerability data, Copyright (c) Microsoft Corporation, from https://github.com/microsoft/AzureLinuxVulnerabilityData via OSV, under the MIT licence; changed: normalised to fixed package versions per release. MIT

github.com/Z3Prover/z3/issues/3363 advisory

CISA SSVC

Exploitation: Proof of concept is public
Automatable: no
Technical impact: total
Assessed: 2 y ago (2024-10-04)

Exploit prediction

1.03% chance of exploitation in the next 30 days, higher than 64% of all scored CVEs (FIRST EPSS, 2026-11-08).

Exploits and checks

github.com https://github.com/Z3Prover/z3/issues/3363 referenced PoC, tagged "exploit" by a source, unverified

CVSS scores

assigned by	version	score	vector
NVD	3.1	7.8	CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H

Classification

Weakness

CWE-416 Use After Free

References

github.com /Z3Prover/z3/issues/3363
exploit, issue-tracking, patch, third-party-advisory

Sources

CVE List CVE-2020-19725
NVD CVE-2020-19725

Fencer Vulns keeps one entry per vulnerability: the CVE id wins, then GHSA, and records that alias each other are merged, except that two CVEs always keep separate entries. The same data is available as JSON.

Summary