// c::P0
// file mix163.c line 15
void * P0(void *);

// c::P1
// file mix163.c line 24
void * P1(void *);

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

// c::P2
// file mix163.c line 33
void * P2(void *);

// c::P3
// file mix163.c line 43
void * P3(void *);

// c::main
// file mix163.c line 53
int _main(void);

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

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

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

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

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

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

// c::__unbuffered_p2_r3
// file mix163.c line 7
int __unbuffered_p2_r3;

// c::__unbuffered_p3_r1
// file mix163.c line 8
int __unbuffered_p3_r1;

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

// c::__unbuffered_p3_r3
// file mix163.c line 9
int __unbuffered_p3_r3;

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

// c::a
// file mix163.c line 10
int a;

// c::x
// file mix163.c line 11
int x;

// c::y
// file mix163.c line 12
int y;

// c::z
// file mix163.c line 13
int z;

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

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

// c::P0
// file mix163.c line 15
void * P0(void * arg)
{
  // file mix163.c line 16 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 16 function P0
  __unbuffered_p0_r1=a;
  // file mix163.c line 16 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 17 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 17 function P0
  __unbuffered_p0_r3=1;
  // file mix163.c line 17 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 18 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 18 function P0
  x=__unbuffered_p0_r3;
  // file mix163.c line 18 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 20 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 20 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 21 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 21 function P0
  __unbuffered_cnt=((__unbuffered_cnt+1));
  // file mix163.c line 21 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 22 function P0
  return nondet_ptr();
  // file mix163.c line 22 function P0
}

// c::P1
// file mix163.c line 24
void * P1(void * arg1)
{
  // file mix163.c line 25 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 25 function P1
  __unbuffered_p1_r1=x;
  // file mix163.c line 25 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 26 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 26 function P1
  __unbuffered_p1_r3=1;
  // file mix163.c line 26 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 27 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 27 function P1
  y=__unbuffered_p1_r3;
  // file mix163.c line 27 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 29 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 29 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 30 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 30 function P1
  __unbuffered_cnt=((__unbuffered_cnt+1));
  // file mix163.c line 30 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 31 function P1
  return nondet_ptr();
  // file mix163.c line 31 function P1
}

// 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 mix163.c line 1
  __unbuffered_cnt=0;
  // file mix163.c line 2
  __unbuffered_p0_r1=0;
  // file mix163.c line 3
  __unbuffered_p0_r3=0;
  // file mix163.c line 4
  __unbuffered_p1_r1=0;
  // file mix163.c line 5
  __unbuffered_p1_r3=0;
  // file mix163.c line 6
  __unbuffered_p2_r1=0;
  // file mix163.c line 7
  __unbuffered_p2_r3=0;
  // file mix163.c line 8
  __unbuffered_p3_r1=0;
  // file mix163.c line 9
  __unbuffered_p3_r3=0;
  // file mix163.c line 10
  a=0;
  // file mix163.c line 11
  x=0;
  // file mix163.c line 12
  y=0;
  // file mix163.c line 13
  z=0;
}

// c::P2
// file mix163.c line 33
void * P2(void * arg2)
{
  // file mix163.c line 34 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 34 function P2
  __unbuffered_p2_r1=2;
  // file mix163.c line 34 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 35 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 35 function P2
  y=__unbuffered_p2_r1;
  // file mix163.c line 35 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 36 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 36 function P2
  __unbuffered_p2_r3=1;
  // file mix163.c line 36 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 37 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 37 function P2
  z=__unbuffered_p2_r3;
  // file mix163.c line 37 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 39 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 39 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 40 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 40 function P2
  __unbuffered_cnt=((__unbuffered_cnt+1));
  // file mix163.c line 40 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 41 function P2
  return nondet_ptr();
  // file mix163.c line 41 function P2
}

// c::P3
// file mix163.c line 43
void * P3(void * arg3)
{
  // file mix163.c line 44 function P3
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 44 function P3
  __unbuffered_p3_r1=2;
  // file mix163.c line 44 function P3
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 45 function P3
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 45 function P3
  z=__unbuffered_p3_r1;
  // file mix163.c line 45 function P3
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 46 function P3
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 46 function P3
  __unbuffered_p3_r3=1;
  // file mix163.c line 46 function P3
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 47 function P3
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 47 function P3
  a=__unbuffered_p3_r3;
  // file mix163.c line 47 function P3
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 49 function P3
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 49 function P3
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 50 function P3
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 50 function P3
  __unbuffered_cnt=((__unbuffered_cnt+1));
  // file mix163.c line 50 function P3
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 51 function P3
  return nondet_ptr();
  // file mix163.c line 51 function P3
}

// c::main
// file mix163.c line 53
int _main(void)
{
  pthread_t __pt0;
  pthread_t __pt1;
  pthread_t __pt2;
  pthread_t __pt3;
  // file mix163.c line 54 function main
  // START_THREAD
  pthread_create(&__pt0, 0, P0, 0);
  // file mix163.c line 55 function main
L1:
  // START_THREAD
  pthread_create(&__pt1, 0, P1, 0);
  // file mix163.c line 56 function main
L2:
  // START_THREAD
  pthread_create(&__pt2, 0, P2, 0);
  // file mix163.c line 57 function main
L3:
  // START_THREAD
  pthread_create(&__pt3, 0, P3, 0);
  // file mix163.c line 58 function main
L4:
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 58 function main
  tmp_guard=(__unbuffered_cnt==4);
  // file mix163.c line 58 function main
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 58 function main
  __CPROVER_assume(tmp_guard);
  // file mix163.c line 59 function main
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix163.c line 59 function main
  tmp_guard1=(!((((y==2) && (z==2)) && (__unbuffered_p0_r1==1)) && (__unbuffered_p1_r1==1)));
  // file mix163.c line 59 function main
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix163.c line 59 function main
  assert(tmp_guard1);
  // file mix163.c line 60 function main
  return 0;
  // file mix163.c line 61 function main
}