z3-floating-point-proofs

February 15, 2018 ยท View on GitHub

Proofs regarding properties of floating-point numbers using Z3 Solver written in Python.

List of proofs

  • Floating-point addition is not associative
  • Positive zero is not a right neutral element for addition