Read the docs
TI-2020-13694 Aliases CVE-2020-19725GHSA-whrm-xv93-8gvj

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

Priority HIGH 69CWE-416Published · Updated

Key facts

Attack vector
Local
Privileges required
None
User interaction
Required
Attack complexity
Low
Impact type
Code execution
Confidentiality · integrity · availability
High · High · High
Fix status
No fix listed

Attack profile from CVSS 3.1 · NVD. Fix status from CNA. Impact type from CWE-416 and the CVSS impact.

Summary

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.

Why it matters now

Exploitation Proof of concept CISA SSVC · not in CISA KEV
EPSS 0.01033 64th percentileScored 2026-11-07
Public exploit Yes 1 exploit referenceTagged by NVD
Fix No fix listed No fixed version in the sources yet

SSVC decision points

CISA ADP · SSVC 2.0.3

Exploitation
Poc
Automatable
No
Technical impact
Total

The decision (Track, Attend, Act) also depends on your mission and well-being impact; see CISA's SSVC guide.

Affected products

VendorProductAffected versionsFixed inStatusSource
——all versions—No fix listedCNA
  • — Vendor— Affected all versions Fixed in — No fix listed CNA

CPE configurations NVD · 1

CPEVersionsRoleVendor
cpe:2.3:a:microsoft:z3:*:*:*:*:*:*:*:*before 4.8.8VulnerableMicrosoft
  • cpe:2.3:a:microsoft:z3:*:*:*:*:*:*:*:* Versions before 4.8.8 Vulnerable ·Microsoft

Remediation

No fixed version listed by the sources yet.

Timeline

  1. 2026-10-02 Threatist record created from CVE-2020-19725
  2. 2026-10-03 Alias added: GHSA-whrm-xv93-8gvj

References

Exploit 1

Sources

This product uses the NVD API but is not endorsed or certified by the NVD. Sources and licences