‹ Back to list

CVE-2020-19725

Status: ModifiedHigh (7.8)—
Severity7.8High · CVSS 3.1
Exploitation probability1.03 %higher than 64% of CVEs
Active exploitationNonot in the CISA catalog
Public exploitNot knownno public code found

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.

CVSS

Base score
7.8
Version
3.1
Vector
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H

Exploitation probability (EPSS)

Probability of exploitation in the next 30 days
1.03 %
Percentile among all scored CVEs
64
Score date
10/22/2026

EPSS (Exploit Prediction Scoring System, FIRST) estimates how likely a vulnerability is to be exploited in the wild within 30 days. It complements CVSS (impact) and CISA KEV (confirmed exploitation).

Affected technologies (1)

Microsoft — Z3

CWEs

References

Show 2 references

Raw JSON (NVD)

Show
{
  "id": "CVE-2020-19725",
  "cveTags": [],
  "metrics": {
    "ssvcV203": [
      {
        "source": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
        "ssvcData": {
          "id": "CVE-2020-19725",
          "role": "CISA Coordinator",
          "options": [
            {
              "exploitation": "poc"
            },
            {
              "automatable": "no"
            },
            {
              "technicalImpact": "total"
            }
          ],
          "version": "2.0.3",
          "timestamp": "2024-10-04T16:06:49.362140Z"
        }
      }
    ],
    "cvssMetricV31": [
      {
        "type": "Primary",
        "source": "nvd@nist.gov",
        "cvssData": {
          "scope": "UNCHANGED",
          "version": "3.1",
          "baseScore": 7.8,
          "attackVector": "LOCAL",
          "baseSeverity": "HIGH",
          "vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H",
          "integrityImpact": "HIGH",
          "userInteraction": "REQUIRED",
          "attackComplexity": "LOW",
          "availabilityImpact": "HIGH",
          "privilegesRequired": "NONE",
          "confidentialityImpact": "HIGH"
        },
        "impactScore": 5.9,
        "exploitabilityScore": 1.8
      }
    ]
  },
  "affected": [
    {
      "source": "cve@mitre.org",
      "affectedData": [
        {
          "vendor": "n/a",
          "product": "n/a",
          "versions": [
            {
              "status": "affected",
              "version": "n/a"
            }
          ]
        }
      ]
    }
  ],
  "published": "2023-08-22T19:16:04.567",
  "references": [
    {
      "url": "https://github.com/Z3Prover/z3/issues/3363",
      "tags": [
        "Exploit",
        "Issue Tracking",
        "Patch",
        "Third Party Advisory"
      ],
      "source": "cve@mitre.org"
    },
    {
      "url": "https://github.com/Z3Prover/z3/issues/3363",
      "tags": [
        "Exploit",
        "Issue Tracking",
        "Patch",
        "Third Party Advisory"
      ],
      "source": "af854a3a-2127-422b-91ae-364da2661108"
    }
  ],
  "vulnStatus": "Modified",
  "weaknesses": [
    {
      "type": "Primary",
      "source": "nvd@nist.gov",
      "description": [
        {
          "lang": "en",
          "value": "CWE-416"
        }
      ]
    }
  ],
  "descriptions": [
    {
      "lang": "en",
      "value": "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."
    },
    {
      "lang": "es",
      "value": "Existe una vulnerabilidad use-after-free en el archivo pdd_simplifier.cpp en Z3 antes de la versión 4.8.8. Ocurre cuando el solucionador intenta simplificar las restricciones y provoca un acceso inesperado a la memoria. Puede causar fallos de segmentación o ejecución arbitraria de código. "
    }
  ],
  "lastModified": "2026-06-17T02:59:56.120",
  "configurations": [
    {
      "nodes": [
        {
          "negate": false,
          "cpeMatch": [
            {
              "criteria": "cpe:2.3:a:microsoft:z3:*:*:*:*:*:*:*:*",
              "vulnerable": true,
              "matchCriteriaId": "6D8EF4B1-776B-4405-896B-9C0EC073D347",
              "versionEndExcluding": "4.8.8"
            }
          ],
          "operator": "OR"
        }
      ]
    }
  ],
  "sourceIdentifier": "cve@mitre.org"
}