Vulnerability Details : 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.
Vulnerability category: Memory Corruption
Products affected by CVE-2020-19725
We don't have affected product information for this CVE yet
Exploit prediction scoring system (EPSS) score for CVE-2020-19725
0.09%
Probability of exploitation activity in the next 30 days
EPSS Score History
~ 40 %
Percentile, the proportion of vulnerabilities that are scored at or less
References for CVE-2020-19725
-
https://github.com/Z3Prover/z3/issues/3363
use after free in ../src/math/grobner/pdd_simplifier.cpp:131 · Issue #3363 · Z3Prover/z3 · GitHub
Jump to