On 37e0d70 we are unsound on the following program:
// PARAM: --enable ana.int.interval --set ana.int.refinement once
#include <assert.h>
int main() {
for (unsigned long i = 0; i < 1000; i++) {
assert(1);
}
assert(1); // reachable
return 0;
}
We claim that the second assert is dead code. The abstract value for i at the loop head is def_exc:Unknown int([0,64]); intervals [0,255].
It's fine with unsigned int and just long.