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