CVE-2020-19725

high

Description

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.

References

https://github.com/Z3Prover/z3/issues/3363

Details

Source: Mitre, NVD

Published: 2023-08-22

Updated: 2023-08-25

Risk Information

CVSS v2

Base Score: 7.2

Vector: CVSS2#AV:L/AC:L/Au:N/C:C/I:C/A:C

Severity: High

CVSS v3

Base Score: 7.8

Vector: CVSS:3.0/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H