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

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

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

// c::P3
// file mix135.c line 44
void * P3(void *);

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

// c::main
// file mix135.c line 52
int _main(void);

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

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

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

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

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

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

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

// c::__unbuffered_p2_r4
// file mix135.c line 8
int __unbuffered_p2_r4;

// c::__unbuffered_p2_r5
// file mix135.c line 9
int __unbuffered_p2_r5;

// c::__unbuffered_p3_r1
// file mix135.c line 10
int __unbuffered_p3_r1;

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

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

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

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

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

// c::z$w_buff0
// 
int czw_buff0;

// c::z$w_buff1
// 
int czw_buff1;

// c::z$w_buff0_used
// 
_Bool czw_buff0_used;

// c::z$w_buff1_used
// 
_Bool czw_buff1_used;

// c::z$mem_tmp
// 
int czmem_tmp;

// c::z$flush_delayed
// 
_Bool czflush_delayed;

// c::z$read_delayed
// 
_Bool czread_delayed;

// c::z$read_delayed_var
// 
int * czread_delayed_var;

// c::z$r_buff0_thd0
// 
_Bool czr_buff0_thd0;

// c::z$r_buff1_thd0
// 
_Bool czr_buff1_thd0;

// c::z$r_buff0_thd1
// 
_Bool czr_buff0_thd1;

// c::z$r_buff1_thd1
// 
_Bool czr_buff1_thd1;

// c::z$r_buff0_thd2
// 
_Bool czr_buff0_thd2;

// c::z$r_buff1_thd2
// 
_Bool czr_buff1_thd2;

// c::z$r_buff0_thd3
// 
_Bool czr_buff0_thd3;

// c::z$r_buff1_thd3
// 
_Bool czr_buff1_thd3;

// c::z$r_buff0_thd4
// 
_Bool czr_buff0_thd4;

// c::z$r_buff1_thd4
// 
_Bool czr_buff1_thd4;

// 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_p0_r1$r_buff0_thd3
// 
_Bool c__unbuffered_p0_r1r_buff0_thd3;

// c::__unbuffered_p0_r1$r_buff1_thd3
// 
_Bool c__unbuffered_p0_r1r_buff1_thd3;

// c::__unbuffered_p0_r1$r_buff0_thd4
// 
_Bool c__unbuffered_p0_r1r_buff0_thd4;

// c::__unbuffered_p0_r1$r_buff1_thd4
// 
_Bool c__unbuffered_p0_r1r_buff1_thd4;

// c::x$w_buff0
// 
int cxw_buff0;

// c::x$w_buff1
// 
int cxw_buff1;

// c::x$w_buff0_used
// 
_Bool cxw_buff0_used;

// c::x$w_buff1_used
// 
_Bool cxw_buff1_used;

// c::x$mem_tmp
// 
int cxmem_tmp;

// c::x$flush_delayed
// 
_Bool cxflush_delayed;

// c::x$read_delayed
// 
_Bool cxread_delayed;

// c::x$read_delayed_var
// 
int * cxread_delayed_var;

// c::x$r_buff0_thd0
// 
_Bool cxr_buff0_thd0;

// c::x$r_buff1_thd0
// 
_Bool cxr_buff1_thd0;

// c::x$r_buff0_thd1
// 
_Bool cxr_buff0_thd1;

// c::x$r_buff1_thd1
// 
_Bool cxr_buff1_thd1;

// c::x$r_buff0_thd2
// 
_Bool cxr_buff0_thd2;

// c::x$r_buff1_thd2
// 
_Bool cxr_buff1_thd2;

// c::x$r_buff0_thd3
// 
_Bool cxr_buff0_thd3;

// c::x$r_buff1_thd3
// 
_Bool cxr_buff1_thd3;

// c::x$r_buff0_thd4
// 
_Bool cxr_buff0_thd4;

// c::x$r_buff1_thd4
// 
_Bool cxr_buff1_thd4;

// c::__unbuffered_p1_r1$w_buff0
// 
int c__unbuffered_p1_r1w_buff0;

// c::__unbuffered_p1_r1$w_buff1
// 
int c__unbuffered_p1_r1w_buff1;

// c::__unbuffered_p1_r1$w_buff0_used
// 
_Bool c__unbuffered_p1_r1w_buff0_used;

// c::__unbuffered_p1_r1$w_buff1_used
// 
_Bool c__unbuffered_p1_r1w_buff1_used;

// c::__unbuffered_p1_r1$mem_tmp
// 
int c__unbuffered_p1_r1mem_tmp;

// c::__unbuffered_p1_r1$flush_delayed
// 
_Bool c__unbuffered_p1_r1flush_delayed;

// c::__unbuffered_p1_r1$read_delayed
// 
_Bool c__unbuffered_p1_r1read_delayed;

// c::__unbuffered_p1_r1$read_delayed_var
// 
int * c__unbuffered_p1_r1read_delayed_var;

// c::__unbuffered_p1_r1$r_buff0_thd0
// 
_Bool c__unbuffered_p1_r1r_buff0_thd0;

// c::__unbuffered_p1_r1$r_buff1_thd0
// 
_Bool c__unbuffered_p1_r1r_buff1_thd0;

// c::__unbuffered_p1_r1$r_buff0_thd1
// 
_Bool c__unbuffered_p1_r1r_buff0_thd1;

// c::__unbuffered_p1_r1$r_buff1_thd1
// 
_Bool c__unbuffered_p1_r1r_buff1_thd1;

// c::__unbuffered_p1_r1$r_buff0_thd2
// 
_Bool c__unbuffered_p1_r1r_buff0_thd2;

// c::__unbuffered_p1_r1$r_buff1_thd2
// 
_Bool c__unbuffered_p1_r1r_buff1_thd2;

// c::__unbuffered_p1_r1$r_buff0_thd3
// 
_Bool c__unbuffered_p1_r1r_buff0_thd3;

// c::__unbuffered_p1_r1$r_buff1_thd3
// 
_Bool c__unbuffered_p1_r1r_buff1_thd3;

// c::__unbuffered_p1_r1$r_buff0_thd4
// 
_Bool c__unbuffered_p1_r1r_buff0_thd4;

// c::__unbuffered_p1_r1$r_buff1_thd4
// 
_Bool c__unbuffered_p1_r1r_buff1_thd4;

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

// 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_buff0_thd3=false;
  c__unbuffered_p0_r1r_buff0_thd4=false;
  c__unbuffered_p0_r1r_buff1_thd0=false;
  c__unbuffered_p0_r1r_buff1_thd1=false;
  c__unbuffered_p0_r1r_buff1_thd2=false;
  c__unbuffered_p0_r1r_buff1_thd3=false;
  c__unbuffered_p0_r1r_buff1_thd4=false;
  c__unbuffered_p1_r1w_buff0_used=false;
  c__unbuffered_p1_r1w_buff1_used=false;
  c__unbuffered_p1_r1flush_delayed=false;
  c__unbuffered_p1_r1read_delayed=false;
  c__unbuffered_p1_r1read_delayed_var=0;
  c__unbuffered_p1_r1r_buff0_thd0=false;
  c__unbuffered_p1_r1r_buff0_thd1=false;
  c__unbuffered_p1_r1r_buff0_thd2=false;
  c__unbuffered_p1_r1r_buff0_thd3=false;
  c__unbuffered_p1_r1r_buff0_thd4=false;
  c__unbuffered_p1_r1r_buff1_thd0=false;
  c__unbuffered_p1_r1r_buff1_thd1=false;
  c__unbuffered_p1_r1r_buff1_thd2=false;
  c__unbuffered_p1_r1r_buff1_thd3=false;
  c__unbuffered_p1_r1r_buff1_thd4=false;
  cxw_buff0_used=false;
  cxw_buff1_used=false;
  cxflush_delayed=false;
  cxread_delayed=false;
  cxread_delayed_var=0;
  cxr_buff0_thd0=false;
  cxr_buff0_thd1=false;
  cxr_buff0_thd2=false;
  cxr_buff0_thd3=false;
  cxr_buff0_thd4=false;
  cxr_buff1_thd0=false;
  cxr_buff1_thd1=false;
  cxr_buff1_thd2=false;
  cxr_buff1_thd3=false;
  cxr_buff1_thd4=false;
  czw_buff0_used=false;
  czw_buff1_used=false;
  czflush_delayed=false;
  czread_delayed=false;
  czread_delayed_var=0;
  czr_buff0_thd0=false;
  czr_buff0_thd1=false;
  czr_buff0_thd2=false;
  czr_buff0_thd3=false;
  czr_buff0_thd4=false;
  czr_buff1_thd0=false;
  czr_buff1_thd1=false;
  czr_buff1_thd2=false;
  czr_buff1_thd3=false;
  czr_buff1_thd4=false;
  __CPROVER_initialize();
  _main();
}

// c::P0
// file mix135.c line 15
void * P0(void * arg)
{
  // file mix135.c line 16 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 16 function P0
  weakchoice0=nondet_bool();
  // file mix135.c line 16 function P0
  weakchoice2=nondet_bool();
  // file mix135.c line 16 function P0
  czflush_delayed=weakchoice2;
  // file mix135.c line 16 function P0
  czmem_tmp=z;
  // file mix135.c line 16 function P0
  weakchoice1=nondet_bool();
  // file mix135.c line 16 function P0
  z=((!czw_buff0_used)? z:((czw_buff0_used && czr_buff0_thd1)? czw_buff0:(((czw_buff0_used && (!czr_buff1_thd1)) && (czw_buff1_used && (!czr_buff0_thd1)))? (weakchoice0? z:(weakchoice1? czw_buff0:czw_buff1)):(((czw_buff0_used && czr_buff1_thd1) && (czw_buff1_used && (!czr_buff0_thd1)))? (weakchoice0? czw_buff1:czw_buff0):(weakchoice0? czw_buff0:z)))));
  // file mix135.c line 16 function P0
  czw_buff0=(weakchoice2? czw_buff0:((!czw_buff0_used)? czw_buff0:((czw_buff0_used && czr_buff0_thd1)? czw_buff0:(((czw_buff0_used && (!czr_buff1_thd1)) && (czw_buff1_used && (!czr_buff0_thd1)))? czw_buff0:(((czw_buff0_used && czr_buff1_thd1) && (czw_buff1_used && (!czr_buff0_thd1)))? czw_buff0:czw_buff0)))));
  // file mix135.c line 16 function P0
  czw_buff1=(weakchoice2? czw_buff1:((!czw_buff0_used)? czw_buff1:((czw_buff0_used && czr_buff0_thd1)? czw_buff1:(((czw_buff0_used && (!czr_buff1_thd1)) && (czw_buff1_used && (!czr_buff0_thd1)))? czw_buff1:(((czw_buff0_used && czr_buff1_thd1) && (czw_buff1_used && (!czr_buff0_thd1)))? czw_buff1:czw_buff1)))));
  // file mix135.c line 16 function P0
  czw_buff0_used=(weakchoice2? czw_buff0_used:((!czw_buff0_used)? czw_buff0_used:((czw_buff0_used && czr_buff0_thd1)? false:(((czw_buff0_used && (!czr_buff1_thd1)) && (czw_buff1_used && (!czr_buff0_thd1)))? (weakchoice0 || (!weakchoice1)):(((czw_buff0_used && czr_buff1_thd1) && (czw_buff1_used && (!czr_buff0_thd1)))? weakchoice0:weakchoice0)))));
  // file mix135.c line 16 function P0
  czw_buff1_used=(weakchoice2? czw_buff1_used:((!czw_buff0_used)? czw_buff1_used:((czw_buff0_used && czr_buff0_thd1)? false:(((czw_buff0_used && (!czr_buff1_thd1)) && (czw_buff1_used && (!czr_buff0_thd1)))? weakchoice0:(((czw_buff0_used && czr_buff1_thd1) && (czw_buff1_used && (!czr_buff0_thd1)))? false:false)))));
  // file mix135.c line 16 function P0
  czr_buff0_thd1=(weakchoice2? czr_buff0_thd1:((!czw_buff0_used)? czr_buff0_thd1:((czw_buff0_used && czr_buff0_thd1)? false:(((czw_buff0_used && (!czr_buff1_thd1)) && (czw_buff1_used && (!czr_buff0_thd1)))? czr_buff0_thd1:(((czw_buff0_used && czr_buff1_thd1) && (czw_buff1_used && (!czr_buff0_thd1)))? false:false)))));
  // file mix135.c line 16 function P0
  czr_buff1_thd1=(weakchoice2? czr_buff1_thd1:((!czw_buff0_used)? czr_buff1_thd1:((czw_buff0_used && czr_buff0_thd1)? false:(((czw_buff0_used && (!czr_buff1_thd1)) && (czw_buff1_used && (!czr_buff0_thd1)))? (weakchoice0? czr_buff1_thd1:false):(((czw_buff0_used && czr_buff1_thd1) && (czw_buff1_used && (!czr_buff0_thd1)))? false:false)))));
  // file mix135.c line 16 function P0
  c__unbuffered_p0_r1read_delayed=true;
  // file mix135.c line 16 function P0
  c__unbuffered_p0_r1read_delayed_var=(&z);
  // file mix135.c line 16 function P0
  __unbuffered_p0_r1=z;
  // file mix135.c line 16 function P0
  z=(czflush_delayed? czmem_tmp:z);
  // file mix135.c line 16 function P0
  czflush_delayed=false;
  // file mix135.c line 16 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 17 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 17 function P0
  __unbuffered_p0_r3=1;
  // file mix135.c line 17 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 18 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 18 function P0
  x=__unbuffered_p0_r3;
  // file mix135.c line 18 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 20 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 20 function P0
  x=((cxw_buff0_used && cxr_buff0_thd1)? cxw_buff0:((cxw_buff1_used && cxr_buff1_thd1)? cxw_buff1:x));
  // file mix135.c line 20 function P0
  cxw_buff0_used=((cxw_buff0_used && cxr_buff0_thd1)? false:cxw_buff0_used);
  // file mix135.c line 20 function P0
  cxw_buff1_used=(((cxw_buff0_used && cxr_buff0_thd1) || (cxw_buff1_used && cxr_buff1_thd1))? false:cxw_buff1_used);
  // file mix135.c line 20 function P0
  cxr_buff0_thd1=((cxw_buff0_used && cxr_buff0_thd1)? false:cxr_buff0_thd1);
  // file mix135.c line 20 function P0
  cxr_buff1_thd1=(((cxw_buff0_used && cxr_buff0_thd1) || (cxw_buff1_used && cxr_buff1_thd1))? false:cxr_buff1_thd1);
  // file mix135.c line 20 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 21 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 21 function P0
  __unbuffered_cnt=((__unbuffered_cnt+1));
  // file mix135.c line 21 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 22 function P0
  return nondet_ptr();
  // file mix135.c line 22 function P0
}

// c::P1
// file mix135.c line 24
void * P1(void * arg1)
{
  // file mix135.c line 25 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 25 function P1
  weakchoice0=nondet_bool();
  // file mix135.c line 25 function P1
  weakchoice2=nondet_bool();
  // file mix135.c line 25 function P1
  cxflush_delayed=weakchoice2;
  // file mix135.c line 25 function P1
  cxmem_tmp=x;
  // file mix135.c line 25 function P1
  weakchoice1=nondet_bool();
  // file mix135.c line 25 function P1
  x=((!cxw_buff0_used)? x:((cxw_buff0_used && cxr_buff0_thd2)? cxw_buff0:(((cxw_buff0_used && (!cxr_buff1_thd2)) && (cxw_buff1_used && (!cxr_buff0_thd2)))? (weakchoice0? x:(weakchoice1? cxw_buff0:cxw_buff1)):(((cxw_buff0_used && cxr_buff1_thd2) && (cxw_buff1_used && (!cxr_buff0_thd2)))? (weakchoice0? cxw_buff1:cxw_buff0):(weakchoice0? cxw_buff0:x)))));
  // file mix135.c line 25 function P1
  cxw_buff0=(weakchoice2? cxw_buff0:((!cxw_buff0_used)? cxw_buff0:((cxw_buff0_used && cxr_buff0_thd2)? cxw_buff0:(((cxw_buff0_used && (!cxr_buff1_thd2)) && (cxw_buff1_used && (!cxr_buff0_thd2)))? cxw_buff0:(((cxw_buff0_used && cxr_buff1_thd2) && (cxw_buff1_used && (!cxr_buff0_thd2)))? cxw_buff0:cxw_buff0)))));
  // file mix135.c line 25 function P1
  cxw_buff1=(weakchoice2? cxw_buff1:((!cxw_buff0_used)? cxw_buff1:((cxw_buff0_used && cxr_buff0_thd2)? cxw_buff1:(((cxw_buff0_used && (!cxr_buff1_thd2)) && (cxw_buff1_used && (!cxr_buff0_thd2)))? cxw_buff1:(((cxw_buff0_used && cxr_buff1_thd2) && (cxw_buff1_used && (!cxr_buff0_thd2)))? cxw_buff1:cxw_buff1)))));
  // file mix135.c line 25 function P1
  cxw_buff0_used=(weakchoice2? cxw_buff0_used:((!cxw_buff0_used)? cxw_buff0_used:((cxw_buff0_used && cxr_buff0_thd2)? false:(((cxw_buff0_used && (!cxr_buff1_thd2)) && (cxw_buff1_used && (!cxr_buff0_thd2)))? (weakchoice0 || (!weakchoice1)):(((cxw_buff0_used && cxr_buff1_thd2) && (cxw_buff1_used && (!cxr_buff0_thd2)))? weakchoice0:weakchoice0)))));
  // file mix135.c line 25 function P1
  cxw_buff1_used=(weakchoice2? cxw_buff1_used:((!cxw_buff0_used)? cxw_buff1_used:((cxw_buff0_used && cxr_buff0_thd2)? false:(((cxw_buff0_used && (!cxr_buff1_thd2)) && (cxw_buff1_used && (!cxr_buff0_thd2)))? weakchoice0:(((cxw_buff0_used && cxr_buff1_thd2) && (cxw_buff1_used && (!cxr_buff0_thd2)))? false:false)))));
  // file mix135.c line 25 function P1
  cxr_buff0_thd2=(weakchoice2? cxr_buff0_thd2:((!cxw_buff0_used)? cxr_buff0_thd2:((cxw_buff0_used && cxr_buff0_thd2)? false:(((cxw_buff0_used && (!cxr_buff1_thd2)) && (cxw_buff1_used && (!cxr_buff0_thd2)))? cxr_buff0_thd2:(((cxw_buff0_used && cxr_buff1_thd2) && (cxw_buff1_used && (!cxr_buff0_thd2)))? false:false)))));
  // file mix135.c line 25 function P1
  cxr_buff1_thd2=(weakchoice2? cxr_buff1_thd2:((!cxw_buff0_used)? cxr_buff1_thd2:((cxw_buff0_used && cxr_buff0_thd2)? false:(((cxw_buff0_used && (!cxr_buff1_thd2)) && (cxw_buff1_used && (!cxr_buff0_thd2)))? (weakchoice0? cxr_buff1_thd2:false):(((cxw_buff0_used && cxr_buff1_thd2) && (cxw_buff1_used && (!cxr_buff0_thd2)))? false:false)))));
  // file mix135.c line 25 function P1
  c__unbuffered_p1_r1read_delayed=true;
  // file mix135.c line 25 function P1
  c__unbuffered_p1_r1read_delayed_var=(&x);
  // file mix135.c line 25 function P1
  __unbuffered_p1_r1=x;
  // file mix135.c line 25 function P1
  x=(cxflush_delayed? cxmem_tmp:x);
  // file mix135.c line 25 function P1
  cxflush_delayed=false;
  // file mix135.c line 25 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 26 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 26 function P1
  __unbuffered_p1_r3=1;
  // file mix135.c line 26 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 27 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 27 function P1
  y=__unbuffered_p1_r3;
  // file mix135.c line 27 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 29 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 29 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 30 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 30 function P1
  __unbuffered_cnt=((__unbuffered_cnt+1));
  // file mix135.c line 30 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 31 function P1
  return nondet_ptr();
  // file mix135.c line 31 function P1
}

// c::P2
// file mix135.c line 33
void * P2(void * arg2)
{
  // file mix135.c line 34 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 34 function P2
  __unbuffered_p2_r1=2;
  // file mix135.c line 34 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 35 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 35 function P2
  y=__unbuffered_p2_r1;
  // file mix135.c line 35 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 36 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 36 function P2
  __unbuffered_p2_r3=y;
  // file mix135.c line 36 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 37 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 37 function P2
  __unbuffered_p2_r4=((__unbuffered_p2_r3 ^ __unbuffered_p2_r3));
  // file mix135.c line 37 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 38 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 38 function P2
  weakchoice0=nondet_bool();
  // file mix135.c line 38 function P2
  weakchoice2=nondet_bool();
  // file mix135.c line 38 function P2
  czflush_delayed=weakchoice2;
  // file mix135.c line 38 function P2
  czmem_tmp=z;
  // file mix135.c line 38 function P2
  z=(((!czw_buff0_used) || (((!czr_buff0_thd3) && (!czw_buff1_used)) || ((!czr_buff0_thd3) && (!czr_buff1_thd3))))? z:((czw_buff0_used && czr_buff0_thd3)? czw_buff0:czw_buff1));
  // file mix135.c line 38 function P2
  czw_buff0=(weakchoice2? czw_buff0:(((!czw_buff0_used) || (((!czr_buff0_thd3) && (!czw_buff1_used)) || ((!czr_buff0_thd3) && (!czr_buff1_thd3))))? czw_buff0:((czw_buff0_used && czr_buff0_thd3)? czw_buff0:czw_buff0)));
  // file mix135.c line 38 function P2
  czw_buff1=(weakchoice2? czw_buff1:(((!czw_buff0_used) || (((!czr_buff0_thd3) && (!czw_buff1_used)) || ((!czr_buff0_thd3) && (!czr_buff1_thd3))))? czw_buff1:((czw_buff0_used && czr_buff0_thd3)? czw_buff1:czw_buff1)));
  // file mix135.c line 38 function P2
  czw_buff0_used=(weakchoice2? czw_buff0_used:(((!czw_buff0_used) || (((!czr_buff0_thd3) && (!czw_buff1_used)) || ((!czr_buff0_thd3) && (!czr_buff1_thd3))))? czw_buff0_used:((czw_buff0_used && czr_buff0_thd3)? false:czw_buff0_used)));
  // file mix135.c line 38 function P2
  czw_buff1_used=(weakchoice2? czw_buff1_used:(((!czw_buff0_used) || (((!czr_buff0_thd3) && (!czw_buff1_used)) || ((!czr_buff0_thd3) && (!czr_buff1_thd3))))? czw_buff1_used:((czw_buff0_used && czr_buff0_thd3)? false:false)));
  // file mix135.c line 38 function P2
  czr_buff0_thd3=(weakchoice2? czr_buff0_thd3:(((!czw_buff0_used) || (((!czr_buff0_thd3) && (!czw_buff1_used)) || ((!czr_buff0_thd3) && (!czr_buff1_thd3))))? czr_buff0_thd3:((czw_buff0_used && czr_buff0_thd3)? false:czr_buff0_thd3)));
  // file mix135.c line 38 function P2
  czr_buff1_thd3=(weakchoice2? czr_buff1_thd3:(((!czw_buff0_used) || (((!czr_buff0_thd3) && (!czw_buff1_used)) || ((!czr_buff0_thd3) && (!czr_buff1_thd3))))? czr_buff1_thd3:((czw_buff0_used && czr_buff0_thd3)? false:false)));
  // file mix135.c line 38 function P2
  __unbuffered_p2_r5=(((int) z)+=__unbuffered_p2_r4);
  // file mix135.c line 38 function P2
  z=(czflush_delayed? czmem_tmp:z);
  // file mix135.c line 38 function P2
  czflush_delayed=false;
  // file mix135.c line 38 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 40 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 40 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 41 function P2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 41 function P2
  __unbuffered_cnt=((__unbuffered_cnt+1));
  // file mix135.c line 41 function P2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 42 function P2
  return nondet_ptr();
  // file mix135.c line 42 function P2
}

// c::P3
// file mix135.c line 44
void * P3(void * arg3)
{
  // file mix135.c line 45 function P3
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 45 function P3
  __unbuffered_p3_r1=1;
  // file mix135.c line 45 function P3
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 46 function P3
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 46 function P3
  z=__unbuffered_p3_r1;
  // file mix135.c line 46 function P3
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 48 function P3
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 48 function P3
  z=((czw_buff0_used && czr_buff0_thd4)? czw_buff0:((czw_buff1_used && czr_buff1_thd4)? czw_buff1:z));
  // file mix135.c line 48 function P3
  czw_buff0_used=((czw_buff0_used && czr_buff0_thd4)? false:czw_buff0_used);
  // file mix135.c line 48 function P3
  czw_buff1_used=(((czw_buff0_used && czr_buff0_thd4) || (czw_buff1_used && czr_buff1_thd4))? false:czw_buff1_used);
  // file mix135.c line 48 function P3
  czr_buff0_thd4=((czw_buff0_used && czr_buff0_thd4)? false:czr_buff0_thd4);
  // file mix135.c line 48 function P3
  czr_buff1_thd4=(((czw_buff0_used && czr_buff0_thd4) || (czw_buff1_used && czr_buff1_thd4))? false:czr_buff1_thd4);
  // file mix135.c line 48 function P3
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 49 function P3
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix135.c line 49 function P3
  __unbuffered_cnt=((__unbuffered_cnt+1));
  // file mix135.c line 49 function P3
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix135.c line 50 function P3
  return nondet_ptr();
  // file mix135.c line 50 function P3
}

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

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