InvariantCPA incorrectly handles aliased pointers

For pointer-arithmetic_false-unreach-label.c, configurations that use the InvariantsCPA (e.g., -bmc-induction) give the wrong result TRUE.

Simplified program:

int main() {
  int tmp[1];
  int *p = tmp;
  *p = 0;
  tmp[0] = 39;
  if (*p == 39) {
ERROR:
    goto ERROR;
  }
  return 0;
}

Command line:

scripts/cpa.sh -invariantGeneration -spec default test.c

The aliasing between tmp and p is not detected and, the InvariantsState store the information *(main::p)={[0, 0]} even after the assignment to tmp[0].