#pragma CIVL ACSL
int a;

/*@ assigns a + (0 .. 9);
  @*/
int f() {
  return 0;
}