// 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::y$w_buff0
// 
int cyw_buff0;

// c::y$w_buff1
// 
int cyw_buff1;

// c::y$w_buff0_used
// 
_Bool cyw_buff0_used;

// c::y$w_buff1_used
// 
_Bool cyw_buff1_used;

// c::y$mem_tmp
// 
int cymem_tmp;

// c::y$flush_delayed
// 
_Bool cyflush_delayed;

// c::y$read_delayed
// 
_Bool cyread_delayed;

// c::y$read_delayed_var
// 
int * cyread_delayed_var;

// c::y$r_buff0_thd0
// 
_Bool cyr_buff0_thd0;

// c::y$r_buff1_thd0
// 
_Bool cyr_buff1_thd0;

// c::y$r_buff0_thd1
// 
_Bool cyr_buff0_thd1;

// c::y$r_buff1_thd1
// 
_Bool cyr_buff1_thd1;

// c::y$r_buff0_thd2
// 
_Bool cyr_buff0_thd2;

// c::y$r_buff1_thd2
// 
_Bool cyr_buff1_thd2;

// weak::choice0
// 
_Bool weakchoice0;

// weak::choice2
// 
_Bool weakchoice2;

// weak::choice1
// 
_Bool weakchoice1;

// c::__unbuffered_p0_r1$w_buff0
// 
int c__unbuffered_p0_r1w_buff0;

// c::__unbuffered_p0_r1$w_buff1
// 
int c__unbuffered_p0_r1w_buff1;

// c::__unbuffered_p0_r1$w_buff0_used
// 
_Bool c__unbuffered_p0_r1w_buff0_used;

// c::__unbuffered_p0_r1$w_buff1_used
// 
_Bool c__unbuffered_p0_r1w_buff1_used;

// c::__unbuffered_p0_r1$mem_tmp
// 
int c__unbuffered_p0_r1mem_tmp;

// c::__unbuffered_p0_r1$flush_delayed
// 
_Bool c__unbuffered_p0_r1flush_delayed;

// c::__unbuffered_p0_r1$read_delayed
// 
_Bool c__unbuffered_p0_r1read_delayed;

// c::__unbuffered_p0_r1$read_delayed_var
// 
int * c__unbuffered_p0_r1read_delayed_var;

// c::__unbuffered_p0_r1$r_buff0_thd0
// 
_Bool c__unbuffered_p0_r1r_buff0_thd0;

// c::__unbuffered_p0_r1$r_buff1_thd0
// 
_Bool c__unbuffered_p0_r1r_buff1_thd0;

// c::__unbuffered_p0_r1$r_buff0_thd1
// 
_Bool c__unbuffered_p0_r1r_buff0_thd1;

// c::__unbuffered_p0_r1$r_buff1_thd1
// 
_Bool c__unbuffered_p0_r1r_buff1_thd1;

// c::__unbuffered_p0_r1$r_buff0_thd2
// 
_Bool c__unbuffered_p0_r1r_buff0_thd2;

// c::__unbuffered_p0_r1$r_buff1_thd2
// 
_Bool c__unbuffered_p0_r1r_buff1_thd2;

// 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)
{
  c__unbuffered_p0_r1w_buff0_used=false;
  c__unbuffered_p0_r1w_buff1_used=false;
  c__unbuffered_p0_r1flush_delayed=false;
  c__unbuffered_p0_r1read_delayed=false;
  c__unbuffered_p0_r1read_delayed_var=0;
  c__unbuffered_p0_r1r_buff0_thd0=false;
  c__unbuffered_p0_r1r_buff0_thd1=false;
  c__unbuffered_p0_r1r_buff0_thd2=false;
  c__unbuffered_p0_r1r_buff1_thd0=false;
  c__unbuffered_p0_r1r_buff1_thd1=false;
  c__unbuffered_p0_r1r_buff1_thd2=false;
  cyw_buff0_used=false;
  cyw_buff1_used=false;
  cyflush_delayed=false;
  cyread_delayed=false;
  cyread_delayed_var=0;
  cyr_buff0_thd0=false;
  cyr_buff0_thd1=false;
  cyr_buff0_thd2=false;
  cyr_buff1_thd0=false;
  cyr_buff1_thd1=false;
  cyr_buff1_thd2=false;
  __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
  weakchoice0=nondet_bool();
  // file mix149.c line 10 function P0
  weakchoice2=nondet_bool();
  // file mix149.c line 10 function P0
  cyflush_delayed=weakchoice2;
  // file mix149.c line 10 function P0
  cymem_tmp=y;
  // file mix149.c line 10 function P0
  weakchoice1=nondet_bool();
  // file mix149.c line 10 function P0
  y=((!cyw_buff0_used)? y:((cyw_buff0_used && cyr_buff0_thd1)? cyw_buff0:(((cyw_buff0_used && (!cyr_buff1_thd1)) && (cyw_buff1_used && (!cyr_buff0_thd1)))? (weakchoice0? y:(weakchoice1? cyw_buff0:cyw_buff1)):(((cyw_buff0_used && cyr_buff1_thd1) && (cyw_buff1_used && (!cyr_buff0_thd1)))? (weakchoice0? cyw_buff1:cyw_buff0):(weakchoice0? cyw_buff0:y)))));
  // file mix149.c line 10 function P0
  cyw_buff0=(weakchoice2? cyw_buff0:((!cyw_buff0_used)? cyw_buff0:((cyw_buff0_used && cyr_buff0_thd1)? cyw_buff0:(((cyw_buff0_used && (!cyr_buff1_thd1)) && (cyw_buff1_used && (!cyr_buff0_thd1)))? cyw_buff0:(((cyw_buff0_used && cyr_buff1_thd1) && (cyw_buff1_used && (!cyr_buff0_thd1)))? cyw_buff0:cyw_buff0)))));
  // file mix149.c line 10 function P0
  cyw_buff1=(weakchoice2? cyw_buff1:((!cyw_buff0_used)? cyw_buff1:((cyw_buff0_used && cyr_buff0_thd1)? cyw_buff1:(((cyw_buff0_used && (!cyr_buff1_thd1)) && (cyw_buff1_used && (!cyr_buff0_thd1)))? cyw_buff1:(((cyw_buff0_used && cyr_buff1_thd1) && (cyw_buff1_used && (!cyr_buff0_thd1)))? cyw_buff1:cyw_buff1)))));
  // file mix149.c line 10 function P0
  cyw_buff0_used=(weakchoice2? cyw_buff0_used:((!cyw_buff0_used)? cyw_buff0_used:((cyw_buff0_used && cyr_buff0_thd1)? false:(((cyw_buff0_used && (!cyr_buff1_thd1)) && (cyw_buff1_used && (!cyr_buff0_thd1)))? (weakchoice0 || (!weakchoice1)):(((cyw_buff0_used && cyr_buff1_thd1) && (cyw_buff1_used && (!cyr_buff0_thd1)))? weakchoice0:weakchoice0)))));
  // file mix149.c line 10 function P0
  cyw_buff1_used=(weakchoice2? cyw_buff1_used:((!cyw_buff0_used)? cyw_buff1_used:((cyw_buff0_used && cyr_buff0_thd1)? false:(((cyw_buff0_used && (!cyr_buff1_thd1)) && (cyw_buff1_used && (!cyr_buff0_thd1)))? weakchoice0:(((cyw_buff0_used && cyr_buff1_thd1) && (cyw_buff1_used && (!cyr_buff0_thd1)))? false:false)))));
  // file mix149.c line 10 function P0
  cyr_buff0_thd1=(weakchoice2? cyr_buff0_thd1:((!cyw_buff0_used)? cyr_buff0_thd1:((cyw_buff0_used && cyr_buff0_thd1)? false:(((cyw_buff0_used && (!cyr_buff1_thd1)) && (cyw_buff1_used && (!cyr_buff0_thd1)))? cyr_buff0_thd1:(((cyw_buff0_used && cyr_buff1_thd1) && (cyw_buff1_used && (!cyr_buff0_thd1)))? false:false)))));
  // file mix149.c line 10 function P0
  cyr_buff1_thd1=(weakchoice2? cyr_buff1_thd1:((!cyw_buff0_used)? cyr_buff1_thd1:((cyw_buff0_used && cyr_buff0_thd1)? false:(((cyw_buff0_used && (!cyr_buff1_thd1)) && (cyw_buff1_used && (!cyr_buff0_thd1)))? (weakchoice0? cyr_buff1_thd1:false):(((cyw_buff0_used && cyr_buff1_thd1) && (cyw_buff1_used && (!cyr_buff0_thd1)))? false:false)))));
  // file mix149.c line 10 function P0
  c__unbuffered_p0_r1read_delayed=true;
  // file mix149.c line 10 function P0
  c__unbuffered_p0_r1read_delayed_var=(&y);
  // file mix149.c line 10 function P0
  __unbuffered_p0_r1=y;
  // file mix149.c line 10 function P0
  y=(cyflush_delayed? cymem_tmp:y);
  // file mix149.c line 10 function P0
  cyflush_delayed=false;
  // 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
  y=((cyw_buff0_used && cyr_buff0_thd2)? cyw_buff0:((cyw_buff1_used && cyr_buff1_thd2)? cyw_buff1:y));
  // file mix149.c line 23 function P1
  cyw_buff0_used=((cyw_buff0_used && cyr_buff0_thd2)? false:cyw_buff0_used);
  // file mix149.c line 23 function P1
  cyw_buff1_used=(((cyw_buff0_used && cyr_buff0_thd2) || (cyw_buff1_used && cyr_buff1_thd2))? false:cyw_buff1_used);
  // file mix149.c line 23 function P1
  cyr_buff0_thd2=((cyw_buff0_used && cyr_buff0_thd2)? false:cyr_buff0_thd2);
  // file mix149.c line 23 function P1
  cyr_buff1_thd2=(((cyw_buff0_used && cyr_buff0_thd2) || (cyw_buff1_used && cyr_buff1_thd2))? false:cyr_buff1_thd2);
  // 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
  weakchoice1=nondet_bool();
  // file mix149.c line 31 function main
  __unbuffered_p0_r1=(c__unbuffered_p0_r1read_delayed? (weakchoice1? (*c__unbuffered_p0_r1read_delayed_var):__unbuffered_p0_r1):__unbuffered_p0_r1);
  // 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;
}