{"id":"CVE-2020-19725","details":"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.","modified":"2026-04-10T04:28:08.180768Z","published":"2023-08-22T19:16:04.567Z","references":[{"type":"FIX","url":"https://github.com/Z3Prover/z3/issues/3363"}],"affected":[{"ranges":[{"type":"GIT","repo":"https://github.com/z3prover/z3","events":[{"introduced":"0"},{"fixed":"ad55a1f1c617a7f0c3dd735c0780fc758424c7f1"}],"database_specific":{"versions":[{"introduced":"0"},{"fixed":"4.8.8"}]}}],"versions":["Z3-4.8.5","z3-4.1.1","z3-4.3.0","z3-4.3.1","z3-4.3.2","z3-4.4.0","z3-4.4.1","z3-4.6.0","z3-4.8.3","z3-4.8.6","z3-4.8.7"],"database_specific":{"source":"https://storage.googleapis.com/cve-osv-conversion/osv-output/CVE-2020-19725.json"}}],"schema_version":"1.7.5","severity":[{"type":"CVSS_V3","score":"CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H"}]}