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.
                
            Metrics
Affected Vendors & Products
References
        | Link | Providers | 
|---|---|
| https://github.com/Z3Prover/z3/issues/3363 |     | 
History
                    Fri, 04 Oct 2024 16:30:00 +0000
| Type | Values Removed | Values Added | 
|---|---|---|
| Metrics | ssvc 
 | 
 MITRE
                        MITRE
                    Status: PUBLISHED
Assigner: mitre
Published: 2023-08-22T00:00:00
Updated: 2024-10-04T16:07:10.602Z
Reserved: 2020-08-13T00:00:00
Link: CVE-2020-19725
 Vulnrichment
                        Vulnrichment
                    Updated: 2024-08-04T14:15:28.571Z
 NVD
                        NVD
                    Status : Modified
Published: 2023-08-22T19:16:04.567
Modified: 2024-11-21T05:09:22.383
Link: CVE-2020-19725
 Redhat
                        Redhat
                    No data.