CVE-2020-19725

https://notcve.org/view.php?id=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. Existe una vulnerabilidad use-after-free en el archivo pdd_simplifier.cpp en Z3 antes de la versión 4.8.8. Ocurre cuando el solucionador intenta simplificar las restricciones y provoca un acceso inesperado a la memoria. • https://github.com/Z3Prover/z3/issues/3363 • CWE-416: Use After Free •