Security advisory

{
  "id": "d43dd356bc0242e84d7790a80003bc79ce5bd062983070d92db8c2c42940a370",
  "url": "https://osv.dev/vulnerability/CVE-2020-19725",
  "method": "structured",
  "payload": {
    "kind": "advisory",
    "title": "CVE-2020-19725",
    "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.",
    "evidence": "osv:CVE-2020-19725",
    "products": [],
    "severity": "high",
    "structured": {
      "id": "CVE-2020-19725",
      "aliases": [
        "CVE-2020-19725"
      ],
      "metrics": [
        {
          "type": "CVSS_V3",
          "score": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H"
        }
      ],
      "affected": [
        {
          "ranges": [
            {
              "repo": "https://github.com/z3prover/z3",
              "type": "GIT",
              "events": [
                {
                  "introduced": "0"
                },
                {
                  "fixed": "ad55a1f1c617a7f0c3dd735c0780fc758424c7f1"
                }
              ],
              "database_specific": {
                "extracted_events": [
                  {
                    "cpe": "cpe:2.3:a:microsoft:z3:*:*:*:*:*:*:*:*",
                    "range": [
                      {
                        "introduced": "0"
                      },
                      {
                        "fixed": "4.8.8"
                      }
                    ],
                    "source": "CPE_RANGE"
                  }
                ]
              }
            }
          ],
          "versions": [
            "z3-4.8.7",
            "z3-4.8.6",
            "Z3-4.8.5",
            "z3-4.8.3",
            "z3-4.6.0",
            "z3-4.4.1",
            "z3-4.4.0",
            "z3-4.3.2",
            "z3-4.3.1",
            "z3-4.3.0",
            "z3-4.1.1"
          ],
          "database_specific": {
            "source": "https://storage.googleapis.com/cve-osv-conversion/osv-output/CVE-2020-19725.json"
          }
        }
      ],
      "modified": "2026-10-20T10:52:23.521664779Z",
      "provider": "osv",
      "references": [
        "https://github.com/Z3Prover/z3/issues/3363"
      ],
      "provider_metadata": {}
    },
    "related_cves": [
      {
        "value": "CVE-2020-19725",
        "evidence": "/id"
      }
    ],
    "security_relevant": true,
    "severity_evidence": "/severity/0/score"
  },
  "source_id": "core-osv",
  "document_id": 383617,
  "published_at": "2023-08-22T19:16:04.567+00:00"
}