Refinement for unsigned long type not working properly #857
Description
In the course of #855, @jerhard came across some asserts Goblint cannot re-establish.
We initially suspected it might have to do with the CIL transformations for loops and a different widening strategy, but the issue seems simpler: The refinement for type unsigned long in this example does not work the same as for other types.
In the following programs, the assert about i succeeds, while the one about ul fails.
// PARAM: --enable ana.int.interval
int main() {
unsigned long ul;
if (! (ul > 0UL)) {
} else {
__goblint_check(ul != 0UL);
}
int i;
if (! (i > 0)) {
} else {
__goblint_check(i != 0);
}
return 0;
}