CVE-2020-19725
There is a use-after-free vulnerability in file pdd_simplifier.cpp in Z3 before 4.8.8. It occurs...
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.
Attack profile
How easy it is to exploit
- Attack vector
- Local
- Complexity
- Low
- Privileges needed
- None
- User interaction
- Required
What an attacker can affect
- Confidentiality
- High
- Integrity
- High
- Availability
- High
Exploit likelihood
What each source reports
NVD Score used
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.
- Record
CVE-2020-19725- CVSS 3.1
- 7.8 High
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H - Weakness
- CWE-416
- Updated
- 2026-11-02
CVE List No score
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.
- Record
CVE-2020-19725- Updated
- 2026-11-02
EUVDEUVD-2020-11623 No score
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.
- Record
EUVD-2020-11623- Updated
- 2026-11-03
GitHub AdvisoriesGHSA-whrm-xv93-8gvj
There is a use-after-free vulnerability in file pdd_simplifier.cpp in Z3 before 4.8.8. It occurs...
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.
- Record
GHSA-whrm-xv93-8gvj- CVSS 3.1
- 7.8 High
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H - Weakness
- CWE-416
- Updated
- 2026-11-02
OSVAZL-27991
CVE-2020-19725 affecting package z3 4.8.7-8
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.
- Record
AZL-27991- CVSS 3.1
- 7.8 High
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H - Updated
- 2026-11-02
OSVAZL-37067
CVE-2020-19725 affecting package z3 for versions less than 4.13.3-1
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.
- Record
AZL-37067- CVSS 3.1
- 7.8 High
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H - Updated
- 2026-11-02
OSV
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.
- Record
CVE-2020-19725- CVSS 3.1
- 7.8 High
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H - Updated
- 2026-11-02
OSVUBUNTU-CVE-2020-19725
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.
- Record
UBUNTU-CVE-2020-19725- CVSS 3.1
- 7.8 High
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H - Updated
- 2026-11-09
Affected products
Affected packages
| Package | Affected | Fixed |
|---|---|---|
z3Azure Linux:2 |
through 4.8.7-8 | None known |
z3Azure Linux:3 |
before 4.13.3-1 | 4.13.3-1 |
z3Ubuntu:16.04:LTS |
All versions, plus listed versions 4.4.0-24.4.0-34.4.0-3build14.4.0-5 |
None known |
z3Ubuntu:18.04:LTS |
All versions, plus listed versions 4.4.1-0.3build34.4.1-0.3build4 |
None known |
z3Ubuntu:20.04:LTS |
All versions, plus listed versions 4.8.4-1build14.8.7-34.8.7-44.8.7-4build1 |
None known |
z3Ubuntu:22.04:LTS |
All versions, plus listed versions 4.8.12-1 |
None known |
z3Ubuntu:25.10 |
All versions, plus listed versions 4.13.3-1 |
None known |
z3Ubuntu:26.10 |
All versions, plus listed versions 4.13.3-1build14.13.3-1.1 |
None known |
z3Ubuntu:26.04:LTS |
All versions, plus listed versions 4.13.3-14.13.3-1build1 |
None known |
History
| Recorded | Changed | Sources |
|---|---|---|
| affected, facts | OSV | |
| aliases | EUVD | |
| first indexed | CVE List, GitHub Advisories, NVD, OSV |
Dates are when Every CVE recorded each change. Upstream dates may differ.
In short
CVE-2020-19725 is a high vulnerability (CVSS 7.8) in Microsoft Z3, published August 22, 2023. No source lists public exploit code. EPSS puts the chance of exploitation in the next 30 days at 1.03%, the 64th percentile. Fixed in z3 4.13.3-1.