Avoiding Overflow Bugs in Fixed-Point Arithmetic with Formal Verification