// c::P0 // file mix050.c line 17 void * P0(void *); // c::P1 // file mix050.c line 31 void * P1(void *); // c::main // file mix050.c line 45 int _main(void); // c::__CPROVER_initialize // file line 14 void __CPROVER_initialize(void); #include #include // c::__unbuffered_p1_r1 // file mix050.c line 7 int __unbuffered_p1_r1; // c::__unbuffered_p1_r3 // file mix050.c line 8 int __unbuffered_p1_r3; // c::__unbuffered_p1_r4 // file mix050.c line 9 int __unbuffered_p1_r4; // c::__unbuffered_p1_r5 // file mix050.c line 10 int __unbuffered_p1_r5; // c::__unbuffered_p1_r7 // file mix050.c line 11 int __unbuffered_p1_r7; // c::a // file mix050.c line 12 int a; // c::x // file mix050.c line 13 int x; // c::y // file mix050.c line 14 int y; // c::z // file mix050.c line 15 int z; // c::main$tmp_guard0 // _Bool tmp_guard; // c::main$tmp_guard1 // _Bool tmp_guard1; // 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; // weak::choice0 // _Bool weakchoice0; // weak::choice2 // _Bool weakchoice2; // weak::choice1 // _Bool weakchoice1; // c::__unbuffered_p0_r3$w_buff0 // int c__unbuffered_p0_r3w_buff0; // c::__unbuffered_p0_r3$w_buff1 // int c__unbuffered_p0_r3w_buff1; // c::__unbuffered_p0_r3$w_buff0_used // _Bool c__unbuffered_p0_r3w_buff0_used; // c::__unbuffered_p0_r3$w_buff1_used // _Bool c__unbuffered_p0_r3w_buff1_used; // c::__unbuffered_p0_r3$mem_tmp // int c__unbuffered_p0_r3mem_tmp; // c::__unbuffered_p0_r3$flush_delayed // _Bool c__unbuffered_p0_r3flush_delayed; // c::__unbuffered_p0_r3$read_delayed // _Bool c__unbuffered_p0_r3read_delayed; // c::__unbuffered_p0_r3$read_delayed_var // int * c__unbuffered_p0_r3read_delayed_var; // c::__unbuffered_p0_r3$r_buff0_thd0 // _Bool c__unbuffered_p0_r3r_buff0_thd0; // c::__unbuffered_p0_r3$r_buff1_thd0 // _Bool c__unbuffered_p0_r3r_buff1_thd0; // c::__unbuffered_p0_r3$r_buff0_thd1 // _Bool c__unbuffered_p0_r3r_buff0_thd1; // c::__unbuffered_p0_r3$r_buff1_thd1 // _Bool c__unbuffered_p0_r3r_buff1_thd1; // c::__unbuffered_p0_r3$r_buff0_thd2 // _Bool c__unbuffered_p0_r3r_buff0_thd2; // c::__unbuffered_p0_r3$r_buff1_thd2 // _Bool c__unbuffered_p0_r3r_buff1_thd2; // 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::__unbuffered_p1_r3$w_buff0 // int c__unbuffered_p1_r3w_buff0; // c::__unbuffered_p1_r3$w_buff1 // int c__unbuffered_p1_r3w_buff1; // c::__unbuffered_p1_r3$w_buff0_used // _Bool c__unbuffered_p1_r3w_buff0_used; // c::__unbuffered_p1_r3$w_buff1_used // _Bool c__unbuffered_p1_r3w_buff1_used; // c::__unbuffered_p1_r3$mem_tmp // int c__unbuffered_p1_r3mem_tmp; // c::__unbuffered_p1_r3$flush_delayed // _Bool c__unbuffered_p1_r3flush_delayed; // c::__unbuffered_p1_r3$read_delayed // _Bool c__unbuffered_p1_r3read_delayed; // c::__unbuffered_p1_r3$read_delayed_var // int * c__unbuffered_p1_r3read_delayed_var; // c::__unbuffered_p1_r3$r_buff0_thd0 // _Bool c__unbuffered_p1_r3r_buff0_thd0; // c::__unbuffered_p1_r3$r_buff1_thd0 // _Bool c__unbuffered_p1_r3r_buff1_thd0; // c::__unbuffered_p1_r3$r_buff0_thd1 // _Bool c__unbuffered_p1_r3r_buff0_thd1; // c::__unbuffered_p1_r3$r_buff1_thd1 // _Bool c__unbuffered_p1_r3r_buff1_thd1; // c::__unbuffered_p1_r3$r_buff0_thd2 // _Bool c__unbuffered_p1_r3r_buff0_thd2; // c::__unbuffered_p1_r3$r_buff1_thd2 // _Bool c__unbuffered_p1_r3r_buff1_thd2; // c::__unbuffered_cnt // file mix050.c line 1 int __unbuffered_cnt; // c::__unbuffered_p0_r1 // file mix050.c line 2 int __unbuffered_p0_r1; // c::__unbuffered_p0_r3 // file mix050.c line 3 int __unbuffered_p0_r3; // c::__unbuffered_p0_r4 // file mix050.c line 4 int __unbuffered_p0_r4; // c::__unbuffered_p0_r5 // file mix050.c line 5 int __unbuffered_p0_r5; // c::__unbuffered_p0_r7 // file mix050.c line 6 int __unbuffered_p0_r7; // main // int main(void) { c__unbuffered_p0_r3w_buff0_used=false; c__unbuffered_p0_r3w_buff1_used=false; c__unbuffered_p0_r3flush_delayed=false; c__unbuffered_p0_r3read_delayed=false; c__unbuffered_p0_r3read_delayed_var=0; c__unbuffered_p0_r3r_buff0_thd0=false; c__unbuffered_p0_r3r_buff0_thd1=false; c__unbuffered_p0_r3r_buff0_thd2=false; c__unbuffered_p0_r3r_buff1_thd0=false; c__unbuffered_p0_r3r_buff1_thd1=false; c__unbuffered_p0_r3r_buff1_thd2=false; c__unbuffered_p1_r3w_buff0_used=false; c__unbuffered_p1_r3w_buff1_used=false; c__unbuffered_p1_r3flush_delayed=false; c__unbuffered_p1_r3read_delayed=false; c__unbuffered_p1_r3read_delayed_var=0; c__unbuffered_p1_r3r_buff0_thd0=false; c__unbuffered_p1_r3r_buff0_thd1=false; c__unbuffered_p1_r3r_buff0_thd2=false; c__unbuffered_p1_r3r_buff1_thd0=false; c__unbuffered_p1_r3r_buff1_thd1=false; c__unbuffered_p1_r3r_buff1_thd2=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_buff1_thd0=false; cxr_buff1_thd1=false; cxr_buff1_thd2=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_buff1_thd0=false; czr_buff1_thd1=false; czr_buff1_thd2=false; __CPROVER_initialize(); _main(); } // c::P0 // file mix050.c line 17 void * P0(void * arg) { // file mix050.c line 18 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 18 function P0 __unbuffered_p0_r1=2; // file mix050.c line 18 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 19 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 19 function P0 cxw_buff1=cxw_buff0; // file mix050.c line 19 function P0 cxw_buff0=__unbuffered_p0_r1; // file mix050.c line 19 function P0 cxw_buff1_used=cxw_buff0_used; // file mix050.c line 19 function P0 cxw_buff0_used=true; // file mix050.c line 19 function P0 assert((!(cxw_buff1_used && cxw_buff0_used))); // file mix050.c line 19 function P0 cxr_buff1_thd0=cxr_buff0_thd0; // file mix050.c line 19 function P0 cxr_buff1_thd1=cxr_buff0_thd1; // file mix050.c line 19 function P0 cxr_buff1_thd2=cxr_buff0_thd2; // file mix050.c line 19 function P0 cxr_buff0_thd1=true; // file mix050.c line 19 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 20 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 20 function P0 weakchoice0=nondet_bool(); // file mix050.c line 20 function P0 weakchoice2=nondet_bool(); // file mix050.c line 20 function P0 cxflush_delayed=weakchoice2; // file mix050.c line 20 function P0 cxmem_tmp=x; // file mix050.c line 20 function P0 weakchoice1=nondet_bool(); // file mix050.c line 20 function P0 x=((!cxw_buff0_used)? x:((cxw_buff0_used && cxr_buff0_thd1)? cxw_buff0:(((cxw_buff0_used && (!cxr_buff1_thd1)) && (cxw_buff1_used && (!cxr_buff0_thd1)))? (weakchoice0? x:(weakchoice1? cxw_buff0:cxw_buff1)):(((cxw_buff0_used && cxr_buff1_thd1) && (cxw_buff1_used && (!cxr_buff0_thd1)))? (weakchoice0? cxw_buff1:cxw_buff0):(weakchoice0? cxw_buff0:x))))); // file mix050.c line 20 function P0 cxw_buff0=(weakchoice2? cxw_buff0:((!cxw_buff0_used)? cxw_buff0:((cxw_buff0_used && cxr_buff0_thd1)? cxw_buff0:(((cxw_buff0_used && (!cxr_buff1_thd1)) && (cxw_buff1_used && (!cxr_buff0_thd1)))? cxw_buff0:(((cxw_buff0_used && cxr_buff1_thd1) && (cxw_buff1_used && (!cxr_buff0_thd1)))? cxw_buff0:cxw_buff0))))); // file mix050.c line 20 function P0 cxw_buff1=(weakchoice2? cxw_buff1:((!cxw_buff0_used)? cxw_buff1:((cxw_buff0_used && cxr_buff0_thd1)? cxw_buff1:(((cxw_buff0_used && (!cxr_buff1_thd1)) && (cxw_buff1_used && (!cxr_buff0_thd1)))? cxw_buff1:(((cxw_buff0_used && cxr_buff1_thd1) && (cxw_buff1_used && (!cxr_buff0_thd1)))? cxw_buff1:cxw_buff1))))); // file mix050.c line 20 function P0 cxw_buff0_used=(weakchoice2? cxw_buff0_used:((!cxw_buff0_used)? cxw_buff0_used:((cxw_buff0_used && cxr_buff0_thd1)? false:(((cxw_buff0_used && (!cxr_buff1_thd1)) && (cxw_buff1_used && (!cxr_buff0_thd1)))? (weakchoice0 || (!weakchoice1)):(((cxw_buff0_used && cxr_buff1_thd1) && (cxw_buff1_used && (!cxr_buff0_thd1)))? weakchoice0:weakchoice0))))); // file mix050.c line 20 function P0 cxw_buff1_used=(weakchoice2? cxw_buff1_used:((!cxw_buff0_used)? cxw_buff1_used:((cxw_buff0_used && cxr_buff0_thd1)? false:(((cxw_buff0_used && (!cxr_buff1_thd1)) && (cxw_buff1_used && (!cxr_buff0_thd1)))? weakchoice0:(((cxw_buff0_used && cxr_buff1_thd1) && (cxw_buff1_used && (!cxr_buff0_thd1)))? false:false))))); // file mix050.c line 20 function P0 cxr_buff0_thd1=(weakchoice2? cxr_buff0_thd1:((!cxw_buff0_used)? cxr_buff0_thd1:((cxw_buff0_used && cxr_buff0_thd1)? false:(((cxw_buff0_used && (!cxr_buff1_thd1)) && (cxw_buff1_used && (!cxr_buff0_thd1)))? cxr_buff0_thd1:(((cxw_buff0_used && cxr_buff1_thd1) && (cxw_buff1_used && (!cxr_buff0_thd1)))? false:false))))); // file mix050.c line 20 function P0 cxr_buff1_thd1=(weakchoice2? cxr_buff1_thd1:((!cxw_buff0_used)? cxr_buff1_thd1:((cxw_buff0_used && cxr_buff0_thd1)? false:(((cxw_buff0_used && (!cxr_buff1_thd1)) && (cxw_buff1_used && (!cxr_buff0_thd1)))? (weakchoice0? cxr_buff1_thd1:false):(((cxw_buff0_used && cxr_buff1_thd1) && (cxw_buff1_used && (!cxr_buff0_thd1)))? false:false))))); // file mix050.c line 20 function P0 c__unbuffered_p0_r3read_delayed=true; // file mix050.c line 20 function P0 c__unbuffered_p0_r3read_delayed_var=(&x); // file mix050.c line 20 function P0 __unbuffered_p0_r3=x; // file mix050.c line 20 function P0 x=(cxflush_delayed? cxmem_tmp:x); // file mix050.c line 20 function P0 cxflush_delayed=false; // file mix050.c line 20 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 21 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 21 function P0 weakchoice1=nondet_bool(); // file mix050.c line 21 function P0 __unbuffered_p0_r3=(c__unbuffered_p0_r3read_delayed? (weakchoice1? (*c__unbuffered_p0_r3read_delayed_var):__unbuffered_p0_r3):__unbuffered_p0_r3); // file mix050.c line 21 function P0 __unbuffered_p0_r4=((__unbuffered_p0_r3 ^ __unbuffered_p0_r3)); // file mix050.c line 21 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 22 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 22 function P0 __unbuffered_p0_r5=1; // file mix050.c line 22 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 23 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 23 function P0 y=((__unbuffered_p0_r5+__unbuffered_p0_r4)); // file mix050.c line 23 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 24 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 24 function P0 __unbuffered_p0_r7=1; // file mix050.c line 24 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 25 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 25 function P0 czw_buff1=czw_buff0; // file mix050.c line 25 function P0 czw_buff0=__unbuffered_p0_r7; // file mix050.c line 25 function P0 czw_buff1_used=czw_buff0_used; // file mix050.c line 25 function P0 czw_buff0_used=true; // file mix050.c line 25 function P0 assert((!(czw_buff1_used && czw_buff0_used))); // file mix050.c line 25 function P0 czr_buff1_thd0=czr_buff0_thd0; // file mix050.c line 25 function P0 czr_buff1_thd1=czr_buff0_thd1; // file mix050.c line 25 function P0 czr_buff1_thd2=czr_buff0_thd2; // file mix050.c line 25 function P0 czr_buff0_thd1=true; // file mix050.c line 25 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 27 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 27 function P0 x=((cxw_buff0_used && cxr_buff0_thd1)? cxw_buff0:((cxw_buff1_used && cxr_buff1_thd1)? cxw_buff1:x)); // file mix050.c line 27 function P0 cxw_buff0_used=((cxw_buff0_used && cxr_buff0_thd1)? false:cxw_buff0_used); // file mix050.c line 27 function P0 cxw_buff1_used=(((cxw_buff0_used && cxr_buff0_thd1) || (cxw_buff1_used && cxr_buff1_thd1))? false:cxw_buff1_used); // file mix050.c line 27 function P0 cxr_buff0_thd1=((cxw_buff0_used && cxr_buff0_thd1)? false:cxr_buff0_thd1); // file mix050.c line 27 function P0 cxr_buff1_thd1=(((cxw_buff0_used && cxr_buff0_thd1) || (cxw_buff1_used && cxr_buff1_thd1))? false:cxr_buff1_thd1); // file mix050.c line 27 function P0 z=((czw_buff0_used && czr_buff0_thd1)? czw_buff0:((czw_buff1_used && czr_buff1_thd1)? czw_buff1:z)); // file mix050.c line 27 function P0 czw_buff0_used=((czw_buff0_used && czr_buff0_thd1)? false:czw_buff0_used); // file mix050.c line 27 function P0 czw_buff1_used=(((czw_buff0_used && czr_buff0_thd1) || (czw_buff1_used && czr_buff1_thd1))? false:czw_buff1_used); // file mix050.c line 27 function P0 czr_buff0_thd1=((czw_buff0_used && czr_buff0_thd1)? false:czr_buff0_thd1); // file mix050.c line 27 function P0 czr_buff1_thd1=(((czw_buff0_used && czr_buff0_thd1) || (czw_buff1_used && czr_buff1_thd1))? false:czr_buff1_thd1); // file mix050.c line 27 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 28 function P0 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 28 function P0 __unbuffered_cnt=((__unbuffered_cnt+1)); // file mix050.c line 28 function P0 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 29 function P0 return nondet_ptr(); // file mix050.c line 29 function P0 } // c::P1 // file mix050.c line 31 void * P1(void * arg1) { // file mix050.c line 32 function P1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 32 function P1 __unbuffered_p1_r1=2; // file mix050.c line 32 function P1 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 33 function P1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 33 function P1 czw_buff1=czw_buff0; // file mix050.c line 33 function P1 czw_buff0=__unbuffered_p1_r1; // file mix050.c line 33 function P1 czw_buff1_used=czw_buff0_used; // file mix050.c line 33 function P1 czw_buff0_used=true; // file mix050.c line 33 function P1 assert((!(czw_buff1_used && czw_buff0_used))); // file mix050.c line 33 function P1 czr_buff1_thd0=czr_buff0_thd0; // file mix050.c line 33 function P1 czr_buff1_thd1=czr_buff0_thd1; // file mix050.c line 33 function P1 czr_buff1_thd2=czr_buff0_thd2; // file mix050.c line 33 function P1 czr_buff0_thd2=true; // file mix050.c line 33 function P1 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 34 function P1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 34 function P1 weakchoice0=nondet_bool(); // file mix050.c line 34 function P1 weakchoice2=nondet_bool(); // file mix050.c line 34 function P1 czflush_delayed=weakchoice2; // file mix050.c line 34 function P1 czmem_tmp=z; // file mix050.c line 34 function P1 weakchoice1=nondet_bool(); // file mix050.c line 34 function P1 z=((!czw_buff0_used)? z:((czw_buff0_used && czr_buff0_thd2)? czw_buff0:(((czw_buff0_used && (!czr_buff1_thd2)) && (czw_buff1_used && (!czr_buff0_thd2)))? (weakchoice0? z:(weakchoice1? czw_buff0:czw_buff1)):(((czw_buff0_used && czr_buff1_thd2) && (czw_buff1_used && (!czr_buff0_thd2)))? (weakchoice0? czw_buff1:czw_buff0):(weakchoice0? czw_buff0:z))))); // file mix050.c line 34 function P1 czw_buff0=(weakchoice2? czw_buff0:((!czw_buff0_used)? czw_buff0:((czw_buff0_used && czr_buff0_thd2)? czw_buff0:(((czw_buff0_used && (!czr_buff1_thd2)) && (czw_buff1_used && (!czr_buff0_thd2)))? czw_buff0:(((czw_buff0_used && czr_buff1_thd2) && (czw_buff1_used && (!czr_buff0_thd2)))? czw_buff0:czw_buff0))))); // file mix050.c line 34 function P1 czw_buff1=(weakchoice2? czw_buff1:((!czw_buff0_used)? czw_buff1:((czw_buff0_used && czr_buff0_thd2)? czw_buff1:(((czw_buff0_used && (!czr_buff1_thd2)) && (czw_buff1_used && (!czr_buff0_thd2)))? czw_buff1:(((czw_buff0_used && czr_buff1_thd2) && (czw_buff1_used && (!czr_buff0_thd2)))? czw_buff1:czw_buff1))))); // file mix050.c line 34 function P1 czw_buff0_used=(weakchoice2? czw_buff0_used:((!czw_buff0_used)? czw_buff0_used:((czw_buff0_used && czr_buff0_thd2)? false:(((czw_buff0_used && (!czr_buff1_thd2)) && (czw_buff1_used && (!czr_buff0_thd2)))? (weakchoice0 || (!weakchoice1)):(((czw_buff0_used && czr_buff1_thd2) && (czw_buff1_used && (!czr_buff0_thd2)))? weakchoice0:weakchoice0))))); // file mix050.c line 34 function P1 czw_buff1_used=(weakchoice2? czw_buff1_used:((!czw_buff0_used)? czw_buff1_used:((czw_buff0_used && czr_buff0_thd2)? false:(((czw_buff0_used && (!czr_buff1_thd2)) && (czw_buff1_used && (!czr_buff0_thd2)))? weakchoice0:(((czw_buff0_used && czr_buff1_thd2) && (czw_buff1_used && (!czr_buff0_thd2)))? false:false))))); // file mix050.c line 34 function P1 czr_buff0_thd2=(weakchoice2? czr_buff0_thd2:((!czw_buff0_used)? czr_buff0_thd2:((czw_buff0_used && czr_buff0_thd2)? false:(((czw_buff0_used && (!czr_buff1_thd2)) && (czw_buff1_used && (!czr_buff0_thd2)))? czr_buff0_thd2:(((czw_buff0_used && czr_buff1_thd2) && (czw_buff1_used && (!czr_buff0_thd2)))? false:false))))); // file mix050.c line 34 function P1 czr_buff1_thd2=(weakchoice2? czr_buff1_thd2:((!czw_buff0_used)? czr_buff1_thd2:((czw_buff0_used && czr_buff0_thd2)? false:(((czw_buff0_used && (!czr_buff1_thd2)) && (czw_buff1_used && (!czr_buff0_thd2)))? (weakchoice0? czr_buff1_thd2:false):(((czw_buff0_used && czr_buff1_thd2) && (czw_buff1_used && (!czr_buff0_thd2)))? false:false))))); // file mix050.c line 34 function P1 c__unbuffered_p1_r3read_delayed=true; // file mix050.c line 34 function P1 c__unbuffered_p1_r3read_delayed_var=(&z); // file mix050.c line 34 function P1 __unbuffered_p1_r3=z; // file mix050.c line 34 function P1 z=(czflush_delayed? czmem_tmp:z); // file mix050.c line 34 function P1 czflush_delayed=false; // file mix050.c line 34 function P1 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 35 function P1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 35 function P1 weakchoice1=nondet_bool(); // file mix050.c line 35 function P1 __unbuffered_p1_r3=(c__unbuffered_p1_r3read_delayed? (weakchoice1? (*c__unbuffered_p1_r3read_delayed_var):__unbuffered_p1_r3):__unbuffered_p1_r3); // file mix050.c line 35 function P1 __unbuffered_p1_r4=((__unbuffered_p1_r3 ^ __unbuffered_p1_r3)); // file mix050.c line 35 function P1 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 36 function P1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 36 function P1 __unbuffered_p1_r5=1; // file mix050.c line 36 function P1 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 37 function P1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 37 function P1 a=((__unbuffered_p1_r5+__unbuffered_p1_r4)); // file mix050.c line 37 function P1 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 38 function P1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 38 function P1 __unbuffered_p1_r7=1; // file mix050.c line 38 function P1 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 39 function P1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 39 function P1 cxw_buff1=cxw_buff0; // file mix050.c line 39 function P1 cxw_buff0=__unbuffered_p1_r7; // file mix050.c line 39 function P1 cxw_buff1_used=cxw_buff0_used; // file mix050.c line 39 function P1 cxw_buff0_used=true; // file mix050.c line 39 function P1 assert((!(cxw_buff1_used && cxw_buff0_used))); // file mix050.c line 39 function P1 cxr_buff1_thd0=cxr_buff0_thd0; // file mix050.c line 39 function P1 cxr_buff1_thd1=cxr_buff0_thd1; // file mix050.c line 39 function P1 cxr_buff1_thd2=cxr_buff0_thd2; // file mix050.c line 39 function P1 cxr_buff0_thd2=true; // file mix050.c line 39 function P1 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 41 function P1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 41 function P1 x=((cxw_buff0_used && cxr_buff0_thd2)? cxw_buff0:((cxw_buff1_used && cxr_buff1_thd2)? cxw_buff1:x)); // file mix050.c line 41 function P1 cxw_buff0_used=((cxw_buff0_used && cxr_buff0_thd2)? false:cxw_buff0_used); // file mix050.c line 41 function P1 cxw_buff1_used=(((cxw_buff0_used && cxr_buff0_thd2) || (cxw_buff1_used && cxr_buff1_thd2))? false:cxw_buff1_used); // file mix050.c line 41 function P1 cxr_buff0_thd2=((cxw_buff0_used && cxr_buff0_thd2)? false:cxr_buff0_thd2); // file mix050.c line 41 function P1 cxr_buff1_thd2=(((cxw_buff0_used && cxr_buff0_thd2) || (cxw_buff1_used && cxr_buff1_thd2))? false:cxr_buff1_thd2); // file mix050.c line 41 function P1 z=((czw_buff0_used && czr_buff0_thd2)? czw_buff0:((czw_buff1_used && czr_buff1_thd2)? czw_buff1:z)); // file mix050.c line 41 function P1 czw_buff0_used=((czw_buff0_used && czr_buff0_thd2)? false:czw_buff0_used); // file mix050.c line 41 function P1 czw_buff1_used=(((czw_buff0_used && czr_buff0_thd2) || (czw_buff1_used && czr_buff1_thd2))? false:czw_buff1_used); // file mix050.c line 41 function P1 czr_buff0_thd2=((czw_buff0_used && czr_buff0_thd2)? false:czr_buff0_thd2); // file mix050.c line 41 function P1 czr_buff1_thd2=(((czw_buff0_used && czr_buff0_thd2) || (czw_buff1_used && czr_buff1_thd2))? false:czr_buff1_thd2); // file mix050.c line 41 function P1 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 42 function P1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 42 function P1 __unbuffered_cnt=((__unbuffered_cnt+1)); // file mix050.c line 42 function P1 // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 43 function P1 return nondet_ptr(); // file mix050.c line 43 function P1 } // c::main // file mix050.c line 45 int _main(void) { pthread_t __pt0; pthread_t __pt1; // file mix050.c line 46 function main // START_THREAD pthread_create(&__pt0, 0, P0, 0); // file mix050.c line 47 function main L1: // START_THREAD pthread_create(&__pt1, 0, P1, 0); // file mix050.c line 48 function main L2: // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 48 function main tmp_guard=(__unbuffered_cnt==2); // file mix050.c line 48 function main // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 48 function main __CPROVER_assume(tmp_guard); // file mix050.c line 49 function main // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file mix050.c line 49 function main weakchoice0=nondet_bool(); // file mix050.c line 49 function main weakchoice2=nondet_bool(); // file mix050.c line 49 function main czflush_delayed=weakchoice2; // file mix050.c line 49 function main czmem_tmp=z; // file mix050.c line 49 function main z=(((!czw_buff0_used) || (((!czr_buff0_thd0) && (!czw_buff1_used)) || ((!czr_buff0_thd0) && (!czr_buff1_thd0))))? z:((czw_buff0_used && czr_buff0_thd0)? czw_buff0:czw_buff1)); // file mix050.c line 49 function main czw_buff0=(weakchoice2? czw_buff0:(((!czw_buff0_used) || (((!czr_buff0_thd0) && (!czw_buff1_used)) || ((!czr_buff0_thd0) && (!czr_buff1_thd0))))? czw_buff0:((czw_buff0_used && czr_buff0_thd0)? czw_buff0:czw_buff0))); // file mix050.c line 49 function main czw_buff1=(weakchoice2? czw_buff1:(((!czw_buff0_used) || (((!czr_buff0_thd0) && (!czw_buff1_used)) || ((!czr_buff0_thd0) && (!czr_buff1_thd0))))? czw_buff1:((czw_buff0_used && czr_buff0_thd0)? czw_buff1:czw_buff1))); // file mix050.c line 49 function main czw_buff0_used=(weakchoice2? czw_buff0_used:(((!czw_buff0_used) || (((!czr_buff0_thd0) && (!czw_buff1_used)) || ((!czr_buff0_thd0) && (!czr_buff1_thd0))))? czw_buff0_used:((czw_buff0_used && czr_buff0_thd0)? false:czw_buff0_used))); // file mix050.c line 49 function main czw_buff1_used=(weakchoice2? czw_buff1_used:(((!czw_buff0_used) || (((!czr_buff0_thd0) && (!czw_buff1_used)) || ((!czr_buff0_thd0) && (!czr_buff1_thd0))))? czw_buff1_used:((czw_buff0_used && czr_buff0_thd0)? false:false))); // file mix050.c line 49 function main czr_buff0_thd0=(weakchoice2? czr_buff0_thd0:(((!czw_buff0_used) || (((!czr_buff0_thd0) && (!czw_buff1_used)) || ((!czr_buff0_thd0) && (!czr_buff1_thd0))))? czr_buff0_thd0:((czw_buff0_used && czr_buff0_thd0)? false:czr_buff0_thd0))); // file mix050.c line 49 function main czr_buff1_thd0=(weakchoice2? czr_buff1_thd0:(((!czw_buff0_used) || (((!czr_buff0_thd0) && (!czw_buff1_used)) || ((!czr_buff0_thd0) && (!czr_buff1_thd0))))? czr_buff1_thd0:((czw_buff0_used && czr_buff0_thd0)? false:false))); // file mix050.c line 49 function main weakchoice0=nondet_bool(); // file mix050.c line 49 function main weakchoice2=nondet_bool(); // file mix050.c line 49 function main cxflush_delayed=weakchoice2; // file mix050.c line 49 function main cxmem_tmp=x; // file mix050.c line 49 function main x=(((!cxw_buff0_used) || (((!cxr_buff0_thd0) && (!cxw_buff1_used)) || ((!cxr_buff0_thd0) && (!cxr_buff1_thd0))))? x:((cxw_buff0_used && cxr_buff0_thd0)? cxw_buff0:cxw_buff1)); // file mix050.c line 49 function main cxw_buff0=(weakchoice2? cxw_buff0:(((!cxw_buff0_used) || (((!cxr_buff0_thd0) && (!cxw_buff1_used)) || ((!cxr_buff0_thd0) && (!cxr_buff1_thd0))))? cxw_buff0:((cxw_buff0_used && cxr_buff0_thd0)? cxw_buff0:cxw_buff0))); // file mix050.c line 49 function main cxw_buff1=(weakchoice2? cxw_buff1:(((!cxw_buff0_used) || (((!cxr_buff0_thd0) && (!cxw_buff1_used)) || ((!cxr_buff0_thd0) && (!cxr_buff1_thd0))))? cxw_buff1:((cxw_buff0_used && cxr_buff0_thd0)? cxw_buff1:cxw_buff1))); // file mix050.c line 49 function main cxw_buff0_used=(weakchoice2? cxw_buff0_used:(((!cxw_buff0_used) || (((!cxr_buff0_thd0) && (!cxw_buff1_used)) || ((!cxr_buff0_thd0) && (!cxr_buff1_thd0))))? cxw_buff0_used:((cxw_buff0_used && cxr_buff0_thd0)? false:cxw_buff0_used))); // file mix050.c line 49 function main cxw_buff1_used=(weakchoice2? cxw_buff1_used:(((!cxw_buff0_used) || (((!cxr_buff0_thd0) && (!cxw_buff1_used)) || ((!cxr_buff0_thd0) && (!cxr_buff1_thd0))))? cxw_buff1_used:((cxw_buff0_used && cxr_buff0_thd0)? false:false))); // file mix050.c line 49 function main cxr_buff0_thd0=(weakchoice2? cxr_buff0_thd0:(((!cxw_buff0_used) || (((!cxr_buff0_thd0) && (!cxw_buff1_used)) || ((!cxr_buff0_thd0) && (!cxr_buff1_thd0))))? cxr_buff0_thd0:((cxw_buff0_used && cxr_buff0_thd0)? false:cxr_buff0_thd0))); // file mix050.c line 49 function main cxr_buff1_thd0=(weakchoice2? cxr_buff1_thd0:(((!cxw_buff0_used) || (((!cxr_buff0_thd0) && (!cxw_buff1_used)) || ((!cxr_buff0_thd0) && (!cxr_buff1_thd0))))? cxr_buff1_thd0:((cxw_buff0_used && cxr_buff0_thd0)? false:false))); // file mix050.c line 49 function main weakchoice1=nondet_bool(); // file mix050.c line 49 function main __unbuffered_p0_r3=(c__unbuffered_p0_r3read_delayed? (weakchoice1? (*c__unbuffered_p0_r3read_delayed_var):__unbuffered_p0_r3):__unbuffered_p0_r3); // file mix050.c line 49 function main weakchoice1=nondet_bool(); // file mix050.c line 49 function main __unbuffered_p1_r3=(c__unbuffered_p1_r3read_delayed? (weakchoice1? (*c__unbuffered_p1_r3read_delayed_var):__unbuffered_p1_r3):__unbuffered_p1_r3); // file mix050.c line 49 function main tmp_guard1=(!((((x==2) && (z==2)) && (__unbuffered_p0_r3==2)) && (__unbuffered_p1_r3==2))); // file mix050.c line 49 function main z=(czflush_delayed? czmem_tmp:z); // file mix050.c line 49 function main czflush_delayed=false; // file mix050.c line 49 function main x=(cxflush_delayed? cxmem_tmp:x); // file mix050.c line 49 function main cxflush_delayed=false; // file mix050.c line 49 function main // ATOMIC_END __CPROVER_atomic_end(); // file mix050.c line 49 function main assert(tmp_guard1); // file mix050.c line 50 function main return 0; // file mix050.c line 51 function main } // 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 mix050.c line 1 __unbuffered_cnt=0; // file mix050.c line 2 __unbuffered_p0_r1=0; // file mix050.c line 3 __unbuffered_p0_r3=0; // file mix050.c line 4 __unbuffered_p0_r4=0; // file mix050.c line 5 __unbuffered_p0_r5=0; // file mix050.c line 6 __unbuffered_p0_r7=0; // file mix050.c line 7 __unbuffered_p1_r1=0; // file mix050.c line 8 __unbuffered_p1_r3=0; // file mix050.c line 9 __unbuffered_p1_r4=0; // file mix050.c line 10 __unbuffered_p1_r5=0; // file mix050.c line 11 __unbuffered_p1_r7=0; // file mix050.c line 12 a=0; // file mix050.c line 13 x=0; // file mix050.c line 14 y=0; // file mix050.c line 15 z=0; }