source: CIVL/mods/dev.civl.com/examples/svcomp17/int2pointerOnSymConst.cvl@ cb4d4f4

int foo(void *p) {
  void * q[5];

  q[0] = p;  // where bug happens
  
 return  (int*)q[0] - (int*)p; // ignore this, just for not pruning

}

int main() {
  int a;
  
  $havoc(&a);
  return  foo((void*)a);
}