int __unbuffered_cnt=0;
int __unbuffered_p0_EAX=0;
int __unbuffered_p1_EAX=0;
int x=0;
int y=0;

void * P0(void * arg) {
  __unbuffered_p0_EAX = y;
  x = 1;
  // Instrumentation for CPROVER
  fence;
  __unbuffered_cnt++;
}

void * P1(void * arg) {
  __unbuffered_p1_EAX = x;
  y = 1;
  // Instrumentation for CPROVER
  fence;
  __unbuffered_cnt++;
}

int main() {
  __CPROVER_ASYNC_0: P0(0);
  __CPROVER_ASYNC_1: P1(0);
  __CPROVER_assume(__unbuffered_cnt==2);
  assert(!(__unbuffered_p0_EAX==1 && __unbuffered_p1_EAX==1));
  return 0;
}