Incorrect modeling of pointer arithmetic/comparison when `--integer-encoding=wrapped-integer`

[shaobo-he]

They should be wrapped.

[shaobo-he]

Merging the concrete repro from #682 here.

#682 shows a false alarm under --integer-encoding=wrapped-integer for GEP/pointer arithmetic with an unsigned 64-bit index:

#include "smack.h"
#include <stdlib.h>

int main() {
  int* arr = (int*)malloc(3*sizeof(int));
  unsigned long long idx = __VERIFIER_nondet_unsigned_long_long();
  assume(arr[0] < 4);
  assume(arr[1] < 5);
  assume(arr[2] < 6);
  assume(idx < 3);
  assert(arr[idx] <= 5);
}

Expected result: verified.

The root issue is that pointer arithmetic/comparison under wrapped integer encoding should consistently use wrapped semantics. #682 is the pointer-arithmetic/GEP subcase of this broader issue.