Int domain refinement causes fixpoint error

[sim642]

Given the following program:

// PARAM: --set ana.int.refinement fixpoint --enable ana.int.interval
// FIXPOINT
#include<assert.h>

int g = 0;

void main()
{
   int i = 0;
   while (1) {
      i++;
      for (int j=0; j < 10; j++) {
         if (i > 100) g = 1;
      }
      if (i>9) i=0;
   }
   return;
}

The verify phase fails with the fixpoint error due to

Map: g =
 (Unknown int([0,1]),[0,2147483647]) instead of (Unknown int([0,1]),[0,1]).

Although we implement interval refinement from exclusion range, this isn't applied here, probably because int domain refinement is disabled for join and widen. However, some refinement is required here because the two abstractions have the same concretization, so verification should succeed as it is sound.

There is possible need for int domain refinement in precise incremental benchmarks. Otherwise there are spurious precision comparisons due to similar reasons (exclusion range being more precise than interval).