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.

CVSS v3.1

7.8 HIGHCVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H

EPSS

1.03% chance of exploitation in the next 30 days, 61th percentile

Published

2023-08-22

Updated

2024-10-04

Proof-of-concept exploits (1)

• Z3Prover/z3/issues/3363

References

• CVE Record
• NVD entry

Related

• CVE-2020-19724
• CVE-2020-19726
• CVE-2020-19722
• CVE-2020-19752
• CVE-2020-19721
• CVE-2020-19762