{"id":"UBUNTU-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-05-20T16:04:15.308232608Z","published":"2023-08-22T19:16:00Z","upstream":["CVE-2020-19725"],"references":[{"type":"REPORT","url":"https://ubuntu.com/security/CVE-2020-19725"},{"type":"REPORT","url":"https://github.com/Z3Prover/z3/issues/3363"},{"type":"REPORT","url":"https://www.cve.org/CVERecord?id=CVE-2020-19725"}],"affected":[{"package":{"name":"z3","ecosystem":"Ubuntu:16.04:LTS","purl":"pkg:deb/ubuntu/z3?arch=source&distro=xenial"},"ranges":[{"type":"ECOSYSTEM","events":[{"introduced":"0"}]}],"versions":["4.4.0-2","4.4.0-3","4.4.0-3build1","4.4.0-5"],"ecosystem_specific":{"binaries":[{"binary_name":"libz3-cil","binary_version":"4.4.0-5"},{"binary_name":"libz3-java","binary_version":"4.4.0-5"},{"binary_version":"4.4.0-5","binary_name":"libz3-jni"},{"binary_name":"python-z3","binary_version":"4.4.0-5"},{"binary_name":"z3","binary_version":"4.4.0-5"}]},"database_specific":{"source":"https://github.com/canonical/ubuntu-security-notices/blob/main/osv/cve/2020/UBUNTU-CVE-2020-19725.json"}},{"package":{"name":"z3","ecosystem":"Ubuntu:18.04:LTS","purl":"pkg:deb/ubuntu/z3?arch=source&distro=bionic"},"ranges":[{"type":"ECOSYSTEM","events":[{"introduced":"0"}]}],"versions":["4.4.1-0.3build3","4.4.1-0.3build4"],"ecosystem_specific":{"binaries":[{"binary_name":"libz3-4","binary_version":"4.4.1-0.3build4"},{"binary_name":"libz3-cil","binary_version":"4.4.1-0.3build4"},{"binary_name":"libz3-java","binary_version":"4.4.1-0.3build4"},{"binary_name":"libz3-jni","binary_version":"4.4.1-0.3build4"},{"binary_name":"python-z3","binary_version":"4.4.1-0.3build4"},{"binary_name":"z3","binary_version":"4.4.1-0.3build4"}]},"database_specific":{"source":"https://github.com/canonical/ubuntu-security-notices/blob/main/osv/cve/2020/UBUNTU-CVE-2020-19725.json"}},{"package":{"name":"z3","ecosystem":"Ubuntu:20.04:LTS","purl":"pkg:deb/ubuntu/z3?arch=source&distro=focal"},"ranges":[{"type":"ECOSYSTEM","events":[{"introduced":"0"}]}],"versions":["4.8.4-1build1","4.8.7-3","4.8.7-4","4.8.7-4build1"],"ecosystem_specific":{"binaries":[{"binary_name":"libz3-4","binary_version":"4.8.7-4build1"},{"binary_name":"libz3-java","binary_version":"4.8.7-4build1"},{"binary_version":"4.8.7-4build1","binary_name":"libz3-jni"},{"binary_name":"python3-z3","binary_version":"4.8.7-4build1"},{"binary_name":"z3","binary_version":"4.8.7-4build1"}]},"database_specific":{"source":"https://github.com/canonical/ubuntu-security-notices/blob/main/osv/cve/2020/UBUNTU-CVE-2020-19725.json"}},{"package":{"name":"z3","ecosystem":"Ubuntu:22.04:LTS","purl":"pkg:deb/ubuntu/z3?arch=source&distro=jammy"},"ranges":[{"type":"ECOSYSTEM","events":[{"introduced":"0"}]}],"versions":["4.8.12-1"],"ecosystem_specific":{"binaries":[{"binary_name":"libz3-4","binary_version":"4.8.12-1"},{"binary_name":"libz3-java","binary_version":"4.8.12-1"},{"binary_name":"libz3-jni","binary_version":"4.8.12-1"},{"binary_name":"python3-z3","binary_version":"4.8.12-1"},{"binary_name":"z3","binary_version":"4.8.12-1"}]},"database_specific":{"source":"https://github.com/canonical/ubuntu-security-notices/blob/main/osv/cve/2020/UBUNTU-CVE-2020-19725.json"}},{"package":{"name":"z3","ecosystem":"Ubuntu:24.04:LTS","purl":"pkg:deb/ubuntu/z3?arch=source&distro=noble"},"ranges":[{"type":"ECOSYSTEM","events":[{"introduced":"0"}]}],"versions":["4.8.12-3.1","4.8.12-3.1build1"],"ecosystem_specific":{"binaries":[{"binary_name":"libz3-4","binary_version":"4.8.12-3.1build1"},{"binary_version":"4.8.12-3.1build1","binary_name":"libz3-java"},{"binary_name":"libz3-jni","binary_version":"4.8.12-3.1build1"},{"binary_name":"python3-z3","binary_version":"4.8.12-3.1build1"},{"binary_name":"z3","binary_version":"4.8.12-3.1build1"}]},"database_specific":{"source":"https://github.com/canonical/ubuntu-security-notices/blob/main/osv/cve/2020/UBUNTU-CVE-2020-19725.json"}},{"package":{"name":"z3","ecosystem":"Ubuntu:25.10","purl":"pkg:deb/ubuntu/z3?arch=source&distro=questing"},"ranges":[{"type":"ECOSYSTEM","events":[{"introduced":"0"}]}],"versions":["4.13.3-1"],"ecosystem_specific":{"binaries":[{"binary_name":"libz3-4","binary_version":"4.13.3-1"},{"binary_name":"libz3-java","binary_version":"4.13.3-1"},{"binary_version":"4.13.3-1","binary_name":"libz3-jni"},{"binary_name":"python3-z3","binary_version":"4.13.3-1"},{"binary_name":"z3","binary_version":"4.13.3-1"}]},"database_specific":{"source":"https://github.com/canonical/ubuntu-security-notices/blob/main/osv/cve/2020/UBUNTU-CVE-2020-19725.json"}},{"package":{"name":"z3","ecosystem":"Ubuntu:26.04:LTS","purl":"pkg:deb/ubuntu/z3?arch=source&distro=resolute"},"ranges":[{"type":"ECOSYSTEM","events":[{"introduced":"0"}]}],"versions":["4.13.3-1","4.13.3-1build1"],"ecosystem_specific":{"binaries":[{"binary_name":"libz3-4","binary_version":"4.13.3-1build1"},{"binary_version":"4.13.3-1build1","binary_name":"libz3-java"},{"binary_version":"4.13.3-1build1","binary_name":"libz3-jni"},{"binary_name":"python3-z3","binary_version":"4.13.3-1build1"},{"binary_version":"4.13.3-1build1","binary_name":"z3"}]},"database_specific":{"source":"https://github.com/canonical/ubuntu-security-notices/blob/main/osv/cve/2020/UBUNTU-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"},{"type":"Ubuntu","score":"medium"}]}