CVE-2020-19725

Summary

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.

Affected Software

VendorProductVersion RangeStatus
n/an/an/aaffected

Weaknesses

  • n/a

ADP Enrichment

CVE Program Container

Additional References

CISA ADP Vulnrichment

  • SSVC:
  • Exploitation: poc
    • Automatable: no
    • Technical Impact: total

References