// c::P0 // file mix045.c line 15 void * P0(void *); // c::P1 // file mix045.c line 24 void * P1(void *); // c::P2 // file mix045.c line 32 void * P2(void *); // c::P3 // file mix045.c line 40 void * P3(void *); // c::__CPROVER_initialize // file line 14 void __CPROVER_initialize(void); // c::main // file mix045.c line 52 int _main(void); #include #include // c::__unbuffered_p0_r1 // file mix045.c line 2 int __unbuffered_p0_r1; // c::__unbuffered_p0_r3 // file mix045.c line 3 int __unbuffered_p0_r3; // c::__unbuffered_p1_r1 // file mix045.c line 4 int __unbuffered_p1_r1; // c::__unbuffered_p2_r1 // file mix045.c line 5 int __unbuffered_p2_r1; // c::__unbuffered_p2_r3 // file mix045.c line 6 int __unbuffered_p2_r3; // c::__unbuffered_p3_r1 // file mix045.c line 7 int __unbuffered_p3_r1; // c::__unbuffered_p3_r3 // file mix045.c line 8 int __unbuffered_p3_r3; // c::__unbuffered_p3_r4 // file mix045.c line 9 int __unbuffered_p3_r4; // c::__unbuffered_p3_r5 // file mix045.c line 10 int __unbuffered_p3_r5; // c::x // file mix045.c line 11 int x; // c::y // file mix045.c line 12 int y; // c::z // file mix045.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::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; // c::y$r_buff0_thd3 // _Bool cyr_buff0_thd3; // c::y$r_buff1_thd3 // _Bool cyr_buff1_thd3; // c::y$r_buff0_thd4 // _Bool cyr_buff0_thd4; // c::y$r_buff1_thd4 // _Bool cyr_buff1_thd4; // c::__unbuffered_cnt // file mix045.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; 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_buff0_thd3=false; cyr_buff0_thd4=false; cyr_buff1_thd0=false; cyr_buff1_thd1=false; cyr_buff1_thd2=false; cyr_buff1_thd3=false; cyr_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 mix045.c line 15 void * P0(void * arg) { // file mix045.c line 16 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 16 function P0 weakchoice0=nondet_bool(); // file mix045.c line 16 function P0 weakchoice2=nondet_bool(); // file mix045.c line 16 function P0 czflush_delayed=weakchoice2; // file mix045.c line 16 function P0 czmem_tmp=z; // file mix045.c line 16 function P0 weakchoice1=nondet_bool(); // file mix045.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 mix045.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 mix045.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 mix045.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 mix045.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 mix045.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 mix045.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 mix045.c line 16 function P0 c__unbuffered_p0_r1read_delayed=true; // file mix045.c line 16 function P0 c__unbuffered_p0_r1read_delayed_var=(&z); // file mix045.c line 16 function P0 __unbuffered_p0_r1=z; // file mix045.c line 16 function P0 z=(czflush_delayed? czmem_tmp:z); // file mix045.c line 16 function P0 czflush_delayed=false; // file mix045.c line 16 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 17 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 17 function P0 __unbuffered_p0_r3=1; // file mix045.c line 17 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 18 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 18 function P0 x=__unbuffered_p0_r3; // file mix045.c line 18 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 20 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 20 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 21 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 21 function P0 __unbuffered_cnt=((__unbuffered_cnt+1)); // file mix045.c line 21 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 22 function P0 return nondet_ptr(); // file mix045.c line 22 function P0 } // c::P1 // file mix045.c line 24 void * P1(void * arg1) { // file mix045.c line 25 function P1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 25 function P1 __unbuffered_p1_r1=2; // file mix045.c line 25 function P1 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 26 function P1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 26 function P1 x=__unbuffered_p1_r1; // file mix045.c line 26 function P1 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 28 function P1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 28 function P1 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 29 function P1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 29 function P1 __unbuffered_cnt=((__unbuffered_cnt+1)); // file mix045.c line 29 function P1 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 30 function P1 return nondet_ptr(); // file mix045.c line 30 function P1 } // c::P2 // file mix045.c line 32 void * P2(void * arg2) { // file mix045.c line 33 function P2 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 33 function P2 __unbuffered_p2_r1=x; // file mix045.c line 33 function P2 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 34 function P2 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 34 function P2 weakchoice0=nondet_bool(); // file mix045.c line 34 function P2 weakchoice2=nondet_bool(); // file mix045.c line 34 function P2 cyflush_delayed=weakchoice2; // file mix045.c line 34 function P2 cymem_tmp=y; // file mix045.c line 34 function P2 y=(((!cyw_buff0_used) || (((!cyr_buff0_thd3) && (!cyw_buff1_used)) || ((!cyr_buff0_thd3) && (!cyr_buff1_thd3))))? y:((cyw_buff0_used && cyr_buff0_thd3)? cyw_buff0:cyw_buff1)); // file mix045.c line 34 function P2 cyw_buff0=(weakchoice2? cyw_buff0:(((!cyw_buff0_used) || (((!cyr_buff0_thd3) && (!cyw_buff1_used)) || ((!cyr_buff0_thd3) && (!cyr_buff1_thd3))))? cyw_buff0:((cyw_buff0_used && cyr_buff0_thd3)? cyw_buff0:cyw_buff0))); // file mix045.c line 34 function P2 cyw_buff1=(weakchoice2? cyw_buff1:(((!cyw_buff0_used) || (((!cyr_buff0_thd3) && (!cyw_buff1_used)) || ((!cyr_buff0_thd3) && (!cyr_buff1_thd3))))? cyw_buff1:((cyw_buff0_used && cyr_buff0_thd3)? cyw_buff1:cyw_buff1))); // file mix045.c line 34 function P2 cyw_buff0_used=(weakchoice2? cyw_buff0_used:(((!cyw_buff0_used) || (((!cyr_buff0_thd3) && (!cyw_buff1_used)) || ((!cyr_buff0_thd3) && (!cyr_buff1_thd3))))? cyw_buff0_used:((cyw_buff0_used && cyr_buff0_thd3)? false:cyw_buff0_used))); // file mix045.c line 34 function P2 cyw_buff1_used=(weakchoice2? cyw_buff1_used:(((!cyw_buff0_used) || (((!cyr_buff0_thd3) && (!cyw_buff1_used)) || ((!cyr_buff0_thd3) && (!cyr_buff1_thd3))))? cyw_buff1_used:((cyw_buff0_used && cyr_buff0_thd3)? false:false))); // file mix045.c line 34 function P2 cyr_buff0_thd3=(weakchoice2? cyr_buff0_thd3:(((!cyw_buff0_used) || (((!cyr_buff0_thd3) && (!cyw_buff1_used)) || ((!cyr_buff0_thd3) && (!cyr_buff1_thd3))))? cyr_buff0_thd3:((cyw_buff0_used && cyr_buff0_thd3)? false:cyr_buff0_thd3))); // file mix045.c line 34 function P2 cyr_buff1_thd3=(weakchoice2? cyr_buff1_thd3:(((!cyw_buff0_used) || (((!cyr_buff0_thd3) && (!cyw_buff1_used)) || ((!cyr_buff0_thd3) && (!cyr_buff1_thd3))))? cyr_buff1_thd3:((cyw_buff0_used && cyr_buff0_thd3)? false:false))); // file mix045.c line 34 function P2 __unbuffered_p2_r3=y; // file mix045.c line 34 function P2 y=(cyflush_delayed? cymem_tmp:y); // file mix045.c line 34 function P2 cyflush_delayed=false; // file mix045.c line 34 function P2 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 36 function P2 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 36 function P2 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 37 function P2 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 37 function P2 __unbuffered_cnt=((__unbuffered_cnt+1)); // file mix045.c line 37 function P2 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 38 function P2 return nondet_ptr(); // file mix045.c line 38 function P2 } // c::P3 // file mix045.c line 40 void * P3(void * arg3) { // file mix045.c line 41 function P3 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 41 function P3 __unbuffered_p3_r1=1; // file mix045.c line 41 function P3 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 42 function P3 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 42 function P3 cyw_buff1=cyw_buff0; // file mix045.c line 42 function P3 cyw_buff0=__unbuffered_p3_r1; // file mix045.c line 42 function P3 cyw_buff1_used=cyw_buff0_used; // file mix045.c line 42 function P3 cyw_buff0_used=true; // file mix045.c line 42 function P3 assert((!(cyw_buff1_used && cyw_buff0_used))); // file mix045.c line 42 function P3 cyr_buff1_thd0=cyr_buff0_thd0; // file mix045.c line 42 function P3 cyr_buff1_thd1=cyr_buff0_thd1; // file mix045.c line 42 function P3 cyr_buff1_thd2=cyr_buff0_thd2; // file mix045.c line 42 function P3 cyr_buff1_thd3=cyr_buff0_thd3; // file mix045.c line 42 function P3 cyr_buff1_thd4=cyr_buff0_thd4; // file mix045.c line 42 function P3 cyr_buff0_thd4=true; // file mix045.c line 42 function P3 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 43 function P3 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 43 function P3 weakchoice0=nondet_bool(); // file mix045.c line 43 function P3 weakchoice2=nondet_bool(); // file mix045.c line 43 function P3 cyflush_delayed=weakchoice2; // file mix045.c line 43 function P3 cymem_tmp=y; // file mix045.c line 43 function P3 y=(((!cyw_buff0_used) || (((!cyr_buff0_thd4) && (!cyw_buff1_used)) || ((!cyr_buff0_thd4) && (!cyr_buff1_thd4))))? y:((cyw_buff0_used && cyr_buff0_thd4)? cyw_buff0:cyw_buff1)); // file mix045.c line 43 function P3 cyw_buff0=(weakchoice2? cyw_buff0:(((!cyw_buff0_used) || (((!cyr_buff0_thd4) && (!cyw_buff1_used)) || ((!cyr_buff0_thd4) && (!cyr_buff1_thd4))))? cyw_buff0:((cyw_buff0_used && cyr_buff0_thd4)? cyw_buff0:cyw_buff0))); // file mix045.c line 43 function P3 cyw_buff1=(weakchoice2? cyw_buff1:(((!cyw_buff0_used) || (((!cyr_buff0_thd4) && (!cyw_buff1_used)) || ((!cyr_buff0_thd4) && (!cyr_buff1_thd4))))? cyw_buff1:((cyw_buff0_used && cyr_buff0_thd4)? cyw_buff1:cyw_buff1))); // file mix045.c line 43 function P3 cyw_buff0_used=(weakchoice2? cyw_buff0_used:(((!cyw_buff0_used) || (((!cyr_buff0_thd4) && (!cyw_buff1_used)) || ((!cyr_buff0_thd4) && (!cyr_buff1_thd4))))? cyw_buff0_used:((cyw_buff0_used && cyr_buff0_thd4)? false:cyw_buff0_used))); // file mix045.c line 43 function P3 cyw_buff1_used=(weakchoice2? cyw_buff1_used:(((!cyw_buff0_used) || (((!cyr_buff0_thd4) && (!cyw_buff1_used)) || ((!cyr_buff0_thd4) && (!cyr_buff1_thd4))))? cyw_buff1_used:((cyw_buff0_used && cyr_buff0_thd4)? false:false))); // file mix045.c line 43 function P3 cyr_buff0_thd4=(weakchoice2? cyr_buff0_thd4:(((!cyw_buff0_used) || (((!cyr_buff0_thd4) && (!cyw_buff1_used)) || ((!cyr_buff0_thd4) && (!cyr_buff1_thd4))))? cyr_buff0_thd4:((cyw_buff0_used && cyr_buff0_thd4)? false:cyr_buff0_thd4))); // file mix045.c line 43 function P3 cyr_buff1_thd4=(weakchoice2? cyr_buff1_thd4:(((!cyw_buff0_used) || (((!cyr_buff0_thd4) && (!cyw_buff1_used)) || ((!cyr_buff0_thd4) && (!cyr_buff1_thd4))))? cyr_buff1_thd4:((cyw_buff0_used && cyr_buff0_thd4)? false:false))); // file mix045.c line 43 function P3 __unbuffered_p3_r3=y; // file mix045.c line 43 function P3 y=(cyflush_delayed? cymem_tmp:y); // file mix045.c line 43 function P3 cyflush_delayed=false; // file mix045.c line 43 function P3 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 44 function P3 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 44 function P3 __unbuffered_p3_r4=((__unbuffered_p3_r3 ^ __unbuffered_p3_r3)); // file mix045.c line 44 function P3 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 45 function P3 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 45 function P3 __unbuffered_p3_r5=1; // file mix045.c line 45 function P3 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 46 function P3 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 46 function P3 z=((__unbuffered_p3_r5+__unbuffered_p3_r4)); // file mix045.c line 46 function P3 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 48 function P3 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 48 function P3 y=((cyw_buff0_used && cyr_buff0_thd4)? cyw_buff0:((cyw_buff1_used && cyr_buff1_thd4)? cyw_buff1:y)); // file mix045.c line 48 function P3 cyw_buff0_used=((cyw_buff0_used && cyr_buff0_thd4)? false:cyw_buff0_used); // file mix045.c line 48 function P3 cyw_buff1_used=(((cyw_buff0_used && cyr_buff0_thd4) || (cyw_buff1_used && cyr_buff1_thd4))? false:cyw_buff1_used); // file mix045.c line 48 function P3 cyr_buff0_thd4=((cyw_buff0_used && cyr_buff0_thd4)? false:cyr_buff0_thd4); // file mix045.c line 48 function P3 cyr_buff1_thd4=(((cyw_buff0_used && cyr_buff0_thd4) || (cyw_buff1_used && cyr_buff1_thd4))? false:cyr_buff1_thd4); // file mix045.c line 48 function P3 z=((czw_buff0_used && czr_buff0_thd4)? czw_buff0:((czw_buff1_used && czr_buff1_thd4)? czw_buff1:z)); // file mix045.c line 48 function P3 czw_buff0_used=((czw_buff0_used && czr_buff0_thd4)? false:czw_buff0_used); // file mix045.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 mix045.c line 48 function P3 czr_buff0_thd4=((czw_buff0_used && czr_buff0_thd4)? false:czr_buff0_thd4); // file mix045.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 mix045.c line 48 function P3 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 49 function P3 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 49 function P3 __unbuffered_cnt=((__unbuffered_cnt+1)); // file mix045.c line 49 function P3 // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 50 function P3 return nondet_ptr(); // file mix045.c line 50 function P3 } // c::__CPROVER_initialize // file line 14 void __CPROVER_initialize(void) { // file line 26 // file line 27 // file line 28 // file line 29 // file line 38 // file mix045.c line 1 __unbuffered_cnt=0; // file mix045.c line 2 __unbuffered_p0_r1=0; // file mix045.c line 3 __unbuffered_p0_r3=0; // file mix045.c line 4 __unbuffered_p1_r1=0; // file mix045.c line 5 __unbuffered_p2_r1=0; // file mix045.c line 6 __unbuffered_p2_r3=0; // file mix045.c line 7 __unbuffered_p3_r1=0; // file mix045.c line 8 __unbuffered_p3_r3=0; // file mix045.c line 9 __unbuffered_p3_r4=0; // file mix045.c line 10 __unbuffered_p3_r5=0; // file mix045.c line 11 x=0; // file mix045.c line 12 y=0; // file mix045.c line 13 z=0; } // c::main // file mix045.c line 52 int _main(void) { pthread_t __pt0; pthread_t __pt1; pthread_t __pt2; pthread_t __pt3; // file mix045.c line 53 function main // START_THREAD pthread_create(&__pt0, 0, P0, 0); // file mix045.c line 54 function main L1: // START_THREAD pthread_create(&__pt1, 0, P1, 0); // file mix045.c line 55 function main L2: // START_THREAD pthread_create(&__pt2, 0, P2, 0); // file mix045.c line 56 function main L3: // START_THREAD pthread_create(&__pt3, 0, P3, 0); // file mix045.c line 57 function main L4: // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 57 function main tmp_guard=(__unbuffered_cnt==4); // file mix045.c line 57 function main // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 57 function main __CPROVER_assume(tmp_guard); // file mix045.c line 58 function main // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix045.c line 58 function main weakchoice1=nondet_bool(); // file mix045.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 mix045.c line 58 function main tmp_guard1=(!(((((x==2) && (__unbuffered_p0_r1==1)) && (__unbuffered_p2_r1==2)) && (__unbuffered_p2_r3==0)) && (__unbuffered_p3_r3==1))); // file mix045.c line 58 function main // ATOMIC_END __CPROVER_atomic_end(); // file mix045.c line 58 function main assert(tmp_guard1); // file mix045.c line 59 function main return 0; // file mix045.c line 60 function main }