{"resultsPerPage":1,"startIndex":0,"totalResults":1,"format":"NVD_CVE","version":"2.0","timestamp":"2026-05-08T16:31:54.379","vulnerabilities":[{"cve":{"id":"CVE-2020-19725","sourceIdentifier":"cve@mitre.org","published":"2023-08-22T19:16:04.567","lastModified":"2024-11-21T05:09:22.383","vulnStatus":"Modified","cveTags":[],"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. "}],"metrics":{"cvssMetricV31":[{"source":"nvd@nist.gov","type":"Primary","cvssData":{"version":"3.1","vectorString":"CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H","baseScore":7.8,"baseSeverity":"HIGH","attackVector":"LOCAL","attackComplexity":"LOW","privilegesRequired":"NONE","userInteraction":"REQUIRED","scope":"UNCHANGED","confidentialityImpact":"HIGH","integrityImpact":"HIGH","availabilityImpact":"HIGH"},"exploitabilityScore":1.8,"impactScore":5.9}]},"weaknesses":[{"source":"nvd@nist.gov","type":"Primary","description":[{"lang":"en","value":"CWE-416"}]}],"configurations":[{"nodes":[{"operator":"OR","negate":false,"cpeMatch":[{"vulnerable":true,"criteria":"cpe:2.3:a:microsoft:z3:*:*:*:*:*:*:*:*","versionEndExcluding":"4.8.8","matchCriteriaId":"6D8EF4B1-776B-4405-896B-9C0EC073D347"}]}]}],"references":[{"url":"https://github.com/Z3Prover/z3/issues/3363","source":"cve@mitre.org","tags":["Exploit","Issue Tracking","Patch","Third Party Advisory"]},{"url":"https://github.com/Z3Prover/z3/issues/3363","source":"af854a3a-2127-422b-91ae-364da2661108","tags":["Exploit","Issue Tracking","Patch","Third Party Advisory"]}]}}]}