// c::P0
// file mix194.c line 10
void * P0(void *);

// c::P1
// file mix194.c line 19
void * P1(void *);

// c::P2
// file mix194.c line 29
void * P2(void *);

// c::main
// file mix194.c line 37
int _main(void);

// c::__CPROVER_initialize
// file <built-in> line 14
void __CPROVER_initialize(void);

#include <assert.h>
#include <pthread.h>

// c::__unbuffered_p2_r1
// file mix194.c line 6
int __unbuffered_p2_r1;

// c::x
// file mix194.c line 7
int x;

// c::y
// file mix194.c line 8
int y;

// c::main$tmp_guard0
// 
_Bool tmp_guard;

// c::main$tmp_guard1
// 
_Bool tmp_guard1;

// c::__unbuffered_cnt
// file mix194.c line 1
int __unbuffered_cnt;

// c::__unbuffered_p0_r1
// file mix194.c line 2
int __unbuffered_p0_r1;

// c::__unbuffered_p0_r3
// file mix194.c line 3
int __unbuffered_p0_r3;

// c::__unbuffered_p1_r1
// file mix194.c line 4
int __unbuffered_p1_r1;

// c::__unbuffered_p1_r3
// file mix194.c line 5
int __unbuffered_p1_r3;

// main
// 
int main(void)
{
  __CPROVER_initialize();
  _main();
}

// c::P0
// file mix194.c line 10
void * P0(void * arg)
{
  // file mix194.c line 11 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 11 function P0
  __unbuffered_p0_r1=y;
  // file mix194.c line 11 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 12 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 12 function P0
  __unbuffered_p0_r3=1;
  // file mix194.c line 12 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 13 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 13 function P0
  x=__unbuffered_p0_r3;
  // file mix194.c line 13 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 15 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 15 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 16 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 16 function P0
  __unbuffered_cnt=((__unbuffered_cnt+1));
  // file mix194.c line 16 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 17 function P0
  return nondet_ptr();
  // file mix194.c line 17 function P0
}

// c::P1
// file mix194.c line 19
void * P1(void * arg1)
{
  // file mix194.c line 20 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 20 function P1
  __unbuffered_p1_r1=2;
  // file mix194.c line 20 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 21 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 21 function P1
  x=__unbuffered_p1_r1;
  // file mix194.c line 21 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 22 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 22 function P1
  __unbuffered_p1_r3=1;
  // file mix194.c line 22 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 23 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 23 function P1
  y=__unbuffered_p1_r3;
  // file mix194.c line 23 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 25 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 25 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 26 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 26 function P1
  __unbuffered_cnt=((__unbuffered_cnt+1));
  // file mix194.c line 26 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 27 function P1
  return nondet_ptr();
  // file mix194.c line 27 function P1
}

// c::P2
// file mix194.c line 29
void * P2(void * arg2)
{
  // file mix194.c line 30 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 30 function P2
  __unbuffered_p2_r1=2;
  // file mix194.c line 30 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 31 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 31 function P2
  y=__unbuffered_p2_r1;
  // file mix194.c line 31 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 33 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 33 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 34 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 34 function P2
  __unbuffered_cnt=((__unbuffered_cnt+1));
  // file mix194.c line 34 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 35 function P2
  return nondet_ptr();
  // file mix194.c line 35 function P2
}

// c::main
// file mix194.c line 37
int _main(void)
{
  pthread_t __pt0;
  pthread_t __pt1;
  pthread_t __pt2;
  // file mix194.c line 38 function main
  // START_THREAD
  pthread_create(&__pt0, 0, P0, 0);
  // file mix194.c line 39 function main
L1:
  // START_THREAD
  pthread_create(&__pt1, 0, P1, 0);
  // file mix194.c line 40 function main
L2:
  // START_THREAD
  pthread_create(&__pt2, 0, P2, 0);
  // file mix194.c line 41 function main
L3:
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 41 function main
  tmp_guard=(__unbuffered_cnt==3);
  // file mix194.c line 41 function main
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 41 function main
  __CPROVER_assume(tmp_guard);
  // file mix194.c line 42 function main
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix194.c line 42 function main
  tmp_guard1=(!(((x==2) && (y==2)) && (__unbuffered_p0_r1==2)));
  // file mix194.c line 42 function main
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix194.c line 42 function main
  assert(tmp_guard1);
  // file mix194.c line 43 function main
  return 0;
  // file mix194.c line 44 function main
}

// c::__CPROVER_initialize
// file <built-in> line 14
void __CPROVER_initialize(void)
{
  // file <built-in> line 26
  // file <built-in> line 27
  // file <built-in> line 28
  // file <built-in> line 29
  // file <built-in> line 38
  // file mix194.c line 1
  __unbuffered_cnt=0;
  // file mix194.c line 2
  __unbuffered_p0_r1=0;
  // file mix194.c line 3
  __unbuffered_p0_r3=0;
  // file mix194.c line 4
  __unbuffered_p1_r1=0;
  // file mix194.c line 5
  __unbuffered_p1_r3=0;
  // file mix194.c line 6
  __unbuffered_p2_r1=0;
  // file mix194.c line 7
  x=0;
  // file mix194.c line 8
  y=0;
}