Bug in the inequality normalisation of the simplifier about cbmc HOT 2 CLOSED

Deactivating NORMALISE_CONSTANT_TESTS in util/simplify_expr_int.cpp:1907 makes the problem disappear

from cbmc.

I'm not convinced the claims about the models or the bug here are correct. I will assume that && has higher precedence than || (as is the case in C). With this in mind, and reordering operands a bit:

f.a <= -1 && -((signed __CPROVER_bitvector[33])f.a) <= 2147483648 ||
f.a <= 2147483646 && -((signed __CPROVER_bitvector[33])f.a) <= -1 ||
f.a <= 2147483647 && -((signed __CPROVER_bitvector[33])f.a) <= -2147483647 ||
FALSE && FALSE ||
FALSE && FALSE

vs.

!(f.a >= 0) && !(-((signed __CPROVER_bitvector[33])f.a) >= 2147483649) ||
!(f.a >= 2147483647) && !(-((signed __CPROVER_bitvector[33])f.a) >= 0) ||
!(-((signed __CPROVER_bitvector[33])f.a) >= -2147483646)

Note that f.a <= 2147483647 was removed by the simplifier, because it is trivially true for signed 32-bit integers. Then I'd conclude that both expressions evaluate to true for all values of f.a other than 0.

Resolving, but please feel free to reopen if my reasoning is flawed.

from cbmc.