Postconditions on floating point types always fail

[PeterBindels-TomTom]

Reproducer:

double f() post(r: r <= 5) {
    return 0;
}

int main() {
    f();
}```

with optimization turned to at least -O1, turns the function into a "contract always fails". Inverting the condition (making it always fail) results in the same result (but the opposite operator in the IR). 

[EricWF]

Fun fun! Thanks.