Open michael-schwarz opened 9 months ago
When minimized, this has nothing to do with affine equalities:
int main()
{
int CELLCOUNT;
int i;
int j;
for(i = 1; i <= CELLCOUNT/2; i++)
{
for(j = 2; j >= 1; j--)
{
}
}
return 1;
}
{
"ana": {
"sv-comp": {
"enabled": true,
"functions": true
}
},
"sem": {
"int": {
"signed_overflow": "assume_none"
}
},
"witness": {
"graphml": {
"enabled": true
}
}
}
Tracing shows exclusion sets growing without bound, e.g.
j -> (Not {-12, -11, -10, -9, -8, -7, -6, -5, -4, -3, -2, -1}([-31,31]))
For the program
with config
and property
unreach-call
, Goblint does not seem to terminate and consumes dubious amounts of memory. If I disable the generation ofgraphml
witnesses, it terminates without any issue.