// c::P0
// file mix149.c line 9
void * P0(void *);

// c::P1
// file mix149.c line 17
void * P1(void *);

// c::main
// file mix149.c line 27
int _main(void);

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

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

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

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

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

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

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

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

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

// c::x
// file mix149.c line 6
int x;

// c::y
// file mix149.c line 7
int y;

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

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

// c::P1
// file mix149.c line 17
void * P1(void * arg1)
{
  // file mix149.c line 18 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix149.c line 18 function P1
  __unbuffered_p1_r1=1;
  // file mix149.c line 18 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix149.c line 19 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix149.c line 19 function P1
  x=__unbuffered_p1_r1;
  // file mix149.c line 19 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix149.c line 20 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix149.c line 20 function P1
  __unbuffered_p1_r3=1;
  // file mix149.c line 20 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix149.c line 21 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix149.c line 21 function P1
  y=__unbuffered_p1_r3;
  // file mix149.c line 21 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix149.c line 23 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix149.c line 23 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix149.c line 24 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix149.c line 24 function P1
  __unbuffered_cnt=((__unbuffered_cnt+1));
  // file mix149.c line 24 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix149.c line 25 function P1
  return nondet_ptr();
  // file mix149.c line 25 function P1
}

// c::main
// file mix149.c line 27
int _main(void)
{
  pthread_t __pt0;
  pthread_t __pt1;
  // file mix149.c line 28 function main
  // START_THREAD
  pthread_create(&__pt0, 0, P0, 0);
  // file mix149.c line 29 function main
L1:
  // START_THREAD
  pthread_create(&__pt1, 0, P1, 0);
  // file mix149.c line 30 function main
L2:
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix149.c line 30 function main
  tmp_guard=(__unbuffered_cnt==2);
  // file mix149.c line 30 function main
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix149.c line 30 function main
  __CPROVER_assume(tmp_guard);
  // file mix149.c line 31 function main
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix149.c line 31 function main
  tmp_guard1=(!((__unbuffered_p0_r1==1) && (__unbuffered_p0_r3==0)));
  // file mix149.c line 31 function main
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix149.c line 31 function main
  assert(tmp_guard1);
  // file mix149.c line 32 function main
  return 0;
  // file mix149.c line 33 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 mix149.c line 1
  __unbuffered_cnt=0;
  // file mix149.c line 2
  __unbuffered_p0_r1=0;
  // file mix149.c line 3
  __unbuffered_p0_r3=0;
  // file mix149.c line 4
  __unbuffered_p1_r1=0;
  // file mix149.c line 5
  __unbuffered_p1_r3=0;
  // file mix149.c line 6
  x=0;
  // file mix149.c line 7
  y=0;
}