Other answers have already considered the relative merits of your ideas. I propose another one: use basic flow analysis to determine whether a variable can be zero. Then you can simply disallow division by variables that are potentially zero.
x = ... y = ... if y ≠ 0: return x / y // In this block, y is known to be nonzero. else return x / y // This, however, is a compile-time error. Alternatively, have an intelligent assert function that establishes invariants:
x = ... require x ≠ 0, "Unexpected zero in calculation" // For the remainder of this scope, x is known to be nonzero. This can be done much like ordinary typechecking, by evaluating all branches of a program with nested typing environments for tracking and verifying invariants. It also extends naturally to range checking, null checking, &c. if your language has such features.