Your verifier is probably lying to you about floats

Here is a promise that looks obviously true: fn add_twice(x: Float) -> Float ensures result...