CVE-2020-19725

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
Link Resource
https://github.com/Z3Prover/z3/issues/3363 Exploit Issue Tracking Patch Third Party Advisory
https://github.com/Z3Prover/z3/issues/3363 Exploit Issue Tracking Patch Third Party Advisory
Configurations

Configuration 1 (hide)

cpe:2.3:a:microsoft:z3:*:*:*:*:*:*:*:*

History

No history.

Information

Published : 2023-08-22 19:16

Updated : 2024-11-21 05:09


NVD link : CVE-2020-19725

Mitre link : CVE-2020-19725

CVE.ORG link : CVE-2020-19725


JSON object : View

Products Affected

microsoft

  • z3
CWE
CWE-416

Use After Free