xennygrimmato/z3-floating-point-proofs

Automated Proofs about floating-point numbers using Z3 Theorem Prover

z3-floating-point-proofs

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