extern int stuff[];

int main() {
  unsigned char idx;
  long val = *(long*)(stuff + idx);
  __CPROVER_assert(val == 13, "compare");
  return 0;
}