// c::P0
// file mix052.c line 13
void * P0(void *);

// c::P1
// file mix052.c line 23
void * P1(void *);

// c::main
// file mix052.c line 36
int _main(void);

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

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

// c::y
// file mix052.c line 10
int y;

// c::z
// file mix052.c line 11
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;

// 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;

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

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

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

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

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

// c::__unbuffered_p1_r4
// file mix052.c line 6
int __unbuffered_p1_r4;

// c::__unbuffered_p1_r5
// file mix052.c line 7
int __unbuffered_p1_r5;

// c::__unbuffered_p1_r7
// file mix052.c line 8
int __unbuffered_p1_r7;

// c::x
// file mix052.c line 9
int x;

// main
// 
int main(void)
{
  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;
  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 mix052.c line 13
void * P0(void * arg)
{
  // file mix052.c line 14 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 14 function P0
  __unbuffered_p0_r1=1;
  // file mix052.c line 14 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 15 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 15 function P0
  cxw_buff1=cxw_buff0;
  // file mix052.c line 15 function P0
  cxw_buff0=__unbuffered_p0_r1;
  // file mix052.c line 15 function P0
  cxw_buff1_used=cxw_buff0_used;
  // file mix052.c line 15 function P0
  cxw_buff0_used=true;
  // file mix052.c line 15 function P0
  assert((!(cxw_buff1_used && cxw_buff0_used)));
  // file mix052.c line 15 function P0
  cxr_buff1_thd0=cxr_buff0_thd0;
  // file mix052.c line 15 function P0
  cxr_buff1_thd1=cxr_buff0_thd1;
  // file mix052.c line 15 function P0
  cxr_buff1_thd2=cxr_buff0_thd2;
  // file mix052.c line 15 function P0
  cxr_buff0_thd1=true;
  // file mix052.c line 15 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 16 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 16 function P0
  __unbuffered_p0_r3=1;
  // file mix052.c line 16 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 17 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 17 function P0
  y=__unbuffered_p0_r3;
  // file mix052.c line 17 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 19 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 19 function P0
  x=((cxw_buff0_used && cxr_buff0_thd1)? cxw_buff0:((cxw_buff1_used && cxr_buff1_thd1)? cxw_buff1:x));
  // file mix052.c line 19 function P0
  cxw_buff0_used=((cxw_buff0_used && cxr_buff0_thd1)? false:cxw_buff0_used);
  // file mix052.c line 19 function P0
  cxw_buff1_used=(((cxw_buff0_used && cxr_buff0_thd1) || (cxw_buff1_used && cxr_buff1_thd1))? false:cxw_buff1_used);
  // file mix052.c line 19 function P0
  cxr_buff0_thd1=((cxw_buff0_used && cxr_buff0_thd1)? false:cxr_buff0_thd1);
  // file mix052.c line 19 function P0
  cxr_buff1_thd1=(((cxw_buff0_used && cxr_buff0_thd1) || (cxw_buff1_used && cxr_buff1_thd1))? false:cxr_buff1_thd1);
  // file mix052.c line 19 function P0
  y=((cyw_buff0_used && cyr_buff0_thd1)? cyw_buff0:((cyw_buff1_used && cyr_buff1_thd1)? cyw_buff1:y));
  // file mix052.c line 19 function P0
  cyw_buff0_used=((cyw_buff0_used && cyr_buff0_thd1)? false:cyw_buff0_used);
  // file mix052.c line 19 function P0
  cyw_buff1_used=(((cyw_buff0_used && cyr_buff0_thd1) || (cyw_buff1_used && cyr_buff1_thd1))? false:cyw_buff1_used);
  // file mix052.c line 19 function P0
  cyr_buff0_thd1=((cyw_buff0_used && cyr_buff0_thd1)? false:cyr_buff0_thd1);
  // file mix052.c line 19 function P0
  cyr_buff1_thd1=(((cyw_buff0_used && cyr_buff0_thd1) || (cyw_buff1_used && cyr_buff1_thd1))? false:cyr_buff1_thd1);
  // file mix052.c line 19 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 20 function P0
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 20 function P0
  __unbuffered_cnt=((__unbuffered_cnt+1));
  // file mix052.c line 20 function P0
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 21 function P0
  return nondet_ptr();
  // file mix052.c line 21 function P0
}

// c::P1
// file mix052.c line 23
void * P1(void * arg1)
{
  // file mix052.c line 24 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 24 function P1
  __unbuffered_p1_r1=2;
  // file mix052.c line 24 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 25 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 25 function P1
  cyw_buff1=cyw_buff0;
  // file mix052.c line 25 function P1
  cyw_buff0=__unbuffered_p1_r1;
  // file mix052.c line 25 function P1
  cyw_buff1_used=cyw_buff0_used;
  // file mix052.c line 25 function P1
  cyw_buff0_used=true;
  // file mix052.c line 25 function P1
  assert((!(cyw_buff1_used && cyw_buff0_used)));
  // file mix052.c line 25 function P1
  cyr_buff1_thd0=cyr_buff0_thd0;
  // file mix052.c line 25 function P1
  cyr_buff1_thd1=cyr_buff0_thd1;
  // file mix052.c line 25 function P1
  cyr_buff1_thd2=cyr_buff0_thd2;
  // file mix052.c line 25 function P1
  cyr_buff0_thd2=true;
  // file mix052.c line 25 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 26 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 26 function P1
  weakchoice0=nondet_bool();
  // file mix052.c line 26 function P1
  weakchoice2=nondet_bool();
  // file mix052.c line 26 function P1
  cyflush_delayed=weakchoice2;
  // file mix052.c line 26 function P1
  cymem_tmp=y;
  // file mix052.c line 26 function P1
  y=(((!cyw_buff0_used) || (((!cyr_buff0_thd2) && (!cyw_buff1_used)) || ((!cyr_buff0_thd2) && (!cyr_buff1_thd2))))? y:((cyw_buff0_used && cyr_buff0_thd2)? cyw_buff0:cyw_buff1));
  // file mix052.c line 26 function P1
  cyw_buff0=(weakchoice2? cyw_buff0:(((!cyw_buff0_used) || (((!cyr_buff0_thd2) && (!cyw_buff1_used)) || ((!cyr_buff0_thd2) && (!cyr_buff1_thd2))))? cyw_buff0:((cyw_buff0_used && cyr_buff0_thd2)? cyw_buff0:cyw_buff0)));
  // file mix052.c line 26 function P1
  cyw_buff1=(weakchoice2? cyw_buff1:(((!cyw_buff0_used) || (((!cyr_buff0_thd2) && (!cyw_buff1_used)) || ((!cyr_buff0_thd2) && (!cyr_buff1_thd2))))? cyw_buff1:((cyw_buff0_used && cyr_buff0_thd2)? cyw_buff1:cyw_buff1)));
  // file mix052.c line 26 function P1
  cyw_buff0_used=(weakchoice2? cyw_buff0_used:(((!cyw_buff0_used) || (((!cyr_buff0_thd2) && (!cyw_buff1_used)) || ((!cyr_buff0_thd2) && (!cyr_buff1_thd2))))? cyw_buff0_used:((cyw_buff0_used && cyr_buff0_thd2)? false:cyw_buff0_used)));
  // file mix052.c line 26 function P1
  cyw_buff1_used=(weakchoice2? cyw_buff1_used:(((!cyw_buff0_used) || (((!cyr_buff0_thd2) && (!cyw_buff1_used)) || ((!cyr_buff0_thd2) && (!cyr_buff1_thd2))))? cyw_buff1_used:((cyw_buff0_used && cyr_buff0_thd2)? false:false)));
  // file mix052.c line 26 function P1
  cyr_buff0_thd2=(weakchoice2? cyr_buff0_thd2:(((!cyw_buff0_used) || (((!cyr_buff0_thd2) && (!cyw_buff1_used)) || ((!cyr_buff0_thd2) && (!cyr_buff1_thd2))))? cyr_buff0_thd2:((cyw_buff0_used && cyr_buff0_thd2)? false:cyr_buff0_thd2)));
  // file mix052.c line 26 function P1
  cyr_buff1_thd2=(weakchoice2? cyr_buff1_thd2:(((!cyw_buff0_used) || (((!cyr_buff0_thd2) && (!cyw_buff1_used)) || ((!cyr_buff0_thd2) && (!cyr_buff1_thd2))))? cyr_buff1_thd2:((cyw_buff0_used && cyr_buff0_thd2)? false:false)));
  // file mix052.c line 26 function P1
  __unbuffered_p1_r3=y;
  // file mix052.c line 26 function P1
  y=(cyflush_delayed? cymem_tmp:y);
  // file mix052.c line 26 function P1
  cyflush_delayed=false;
  // file mix052.c line 26 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 27 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 27 function P1
  __unbuffered_p1_r4=((__unbuffered_p1_r3 ^ __unbuffered_p1_r3));
  // file mix052.c line 27 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 28 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 28 function P1
  __unbuffered_p1_r5=1;
  // file mix052.c line 28 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 29 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 29 function P1
  z=((__unbuffered_p1_r5+__unbuffered_p1_r4));
  // file mix052.c line 29 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 30 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 30 function P1
  weakchoice0=nondet_bool();
  // file mix052.c line 30 function P1
  weakchoice2=nondet_bool();
  // file mix052.c line 30 function P1
  cxflush_delayed=weakchoice2;
  // file mix052.c line 30 function P1
  cxmem_tmp=x;
  // file mix052.c line 30 function P1
  x=(((!cxw_buff0_used) || (((!cxr_buff0_thd2) && (!cxw_buff1_used)) || ((!cxr_buff0_thd2) && (!cxr_buff1_thd2))))? x:((cxw_buff0_used && cxr_buff0_thd2)? cxw_buff0:cxw_buff1));
  // file mix052.c line 30 function P1
  cxw_buff0=(weakchoice2? cxw_buff0:(((!cxw_buff0_used) || (((!cxr_buff0_thd2) && (!cxw_buff1_used)) || ((!cxr_buff0_thd2) && (!cxr_buff1_thd2))))? cxw_buff0:((cxw_buff0_used && cxr_buff0_thd2)? cxw_buff0:cxw_buff0)));
  // file mix052.c line 30 function P1
  cxw_buff1=(weakchoice2? cxw_buff1:(((!cxw_buff0_used) || (((!cxr_buff0_thd2) && (!cxw_buff1_used)) || ((!cxr_buff0_thd2) && (!cxr_buff1_thd2))))? cxw_buff1:((cxw_buff0_used && cxr_buff0_thd2)? cxw_buff1:cxw_buff1)));
  // file mix052.c line 30 function P1
  cxw_buff0_used=(weakchoice2? cxw_buff0_used:(((!cxw_buff0_used) || (((!cxr_buff0_thd2) && (!cxw_buff1_used)) || ((!cxr_buff0_thd2) && (!cxr_buff1_thd2))))? cxw_buff0_used:((cxw_buff0_used && cxr_buff0_thd2)? false:cxw_buff0_used)));
  // file mix052.c line 30 function P1
  cxw_buff1_used=(weakchoice2? cxw_buff1_used:(((!cxw_buff0_used) || (((!cxr_buff0_thd2) && (!cxw_buff1_used)) || ((!cxr_buff0_thd2) && (!cxr_buff1_thd2))))? cxw_buff1_used:((cxw_buff0_used && cxr_buff0_thd2)? false:false)));
  // file mix052.c line 30 function P1
  cxr_buff0_thd2=(weakchoice2? cxr_buff0_thd2:(((!cxw_buff0_used) || (((!cxr_buff0_thd2) && (!cxw_buff1_used)) || ((!cxr_buff0_thd2) && (!cxr_buff1_thd2))))? cxr_buff0_thd2:((cxw_buff0_used && cxr_buff0_thd2)? false:cxr_buff0_thd2)));
  // file mix052.c line 30 function P1
  cxr_buff1_thd2=(weakchoice2? cxr_buff1_thd2:(((!cxw_buff0_used) || (((!cxr_buff0_thd2) && (!cxw_buff1_used)) || ((!cxr_buff0_thd2) && (!cxr_buff1_thd2))))? cxr_buff1_thd2:((cxw_buff0_used && cxr_buff0_thd2)? false:false)));
  // file mix052.c line 30 function P1
  __unbuffered_p1_r7=x;
  // file mix052.c line 30 function P1
  x=(cxflush_delayed? cxmem_tmp:x);
  // file mix052.c line 30 function P1
  cxflush_delayed=false;
  // file mix052.c line 30 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 32 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 32 function P1
  y=((cyw_buff0_used && cyr_buff0_thd2)? cyw_buff0:((cyw_buff1_used && cyr_buff1_thd2)? cyw_buff1:y));
  // file mix052.c line 32 function P1
  cyw_buff0_used=((cyw_buff0_used && cyr_buff0_thd2)? false:cyw_buff0_used);
  // file mix052.c line 32 function P1
  cyw_buff1_used=(((cyw_buff0_used && cyr_buff0_thd2) || (cyw_buff1_used && cyr_buff1_thd2))? false:cyw_buff1_used);
  // file mix052.c line 32 function P1
  cyr_buff0_thd2=((cyw_buff0_used && cyr_buff0_thd2)? false:cyr_buff0_thd2);
  // file mix052.c line 32 function P1
  cyr_buff1_thd2=(((cyw_buff0_used && cyr_buff0_thd2) || (cyw_buff1_used && cyr_buff1_thd2))? false:cyr_buff1_thd2);
  // file mix052.c line 32 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 33 function P1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 33 function P1
  __unbuffered_cnt=((__unbuffered_cnt+1));
  // file mix052.c line 33 function P1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 34 function P1
  return nondet_ptr();
  // file mix052.c line 34 function P1
}

// c::main
// file mix052.c line 36
int _main(void)
{
  pthread_t __pt0;
  pthread_t __pt1;
  // file mix052.c line 37 function main
  // START_THREAD
  pthread_create(&__pt0, 0, P0, 0);
  // file mix052.c line 38 function main
L1:
  // START_THREAD
  pthread_create(&__pt1, 0, P1, 0);
  // file mix052.c line 39 function main
L2:
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 39 function main
  tmp_guard=(__unbuffered_cnt==2);
  // file mix052.c line 39 function main
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 39 function main
  __CPROVER_assume(tmp_guard);
  // file mix052.c line 40 function main
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file mix052.c line 40 function main
  weakchoice0=nondet_bool();
  // file mix052.c line 40 function main
  weakchoice2=nondet_bool();
  // file mix052.c line 40 function main
  cyflush_delayed=weakchoice2;
  // file mix052.c line 40 function main
  cymem_tmp=y;
  // file mix052.c line 40 function main
  y=(((!cyw_buff0_used) || (((!cyr_buff0_thd0) && (!cyw_buff1_used)) || ((!cyr_buff0_thd0) && (!cyr_buff1_thd0))))? y:((cyw_buff0_used && cyr_buff0_thd0)? cyw_buff0:cyw_buff1));
  // file mix052.c line 40 function main
  cyw_buff0=(weakchoice2? cyw_buff0:(((!cyw_buff0_used) || (((!cyr_buff0_thd0) && (!cyw_buff1_used)) || ((!cyr_buff0_thd0) && (!cyr_buff1_thd0))))? cyw_buff0:((cyw_buff0_used && cyr_buff0_thd0)? cyw_buff0:cyw_buff0)));
  // file mix052.c line 40 function main
  cyw_buff1=(weakchoice2? cyw_buff1:(((!cyw_buff0_used) || (((!cyr_buff0_thd0) && (!cyw_buff1_used)) || ((!cyr_buff0_thd0) && (!cyr_buff1_thd0))))? cyw_buff1:((cyw_buff0_used && cyr_buff0_thd0)? cyw_buff1:cyw_buff1)));
  // file mix052.c line 40 function main
  cyw_buff0_used=(weakchoice2? cyw_buff0_used:(((!cyw_buff0_used) || (((!cyr_buff0_thd0) && (!cyw_buff1_used)) || ((!cyr_buff0_thd0) && (!cyr_buff1_thd0))))? cyw_buff0_used:((cyw_buff0_used && cyr_buff0_thd0)? false:cyw_buff0_used)));
  // file mix052.c line 40 function main
  cyw_buff1_used=(weakchoice2? cyw_buff1_used:(((!cyw_buff0_used) || (((!cyr_buff0_thd0) && (!cyw_buff1_used)) || ((!cyr_buff0_thd0) && (!cyr_buff1_thd0))))? cyw_buff1_used:((cyw_buff0_used && cyr_buff0_thd0)? false:false)));
  // file mix052.c line 40 function main
  cyr_buff0_thd0=(weakchoice2? cyr_buff0_thd0:(((!cyw_buff0_used) || (((!cyr_buff0_thd0) && (!cyw_buff1_used)) || ((!cyr_buff0_thd0) && (!cyr_buff1_thd0))))? cyr_buff0_thd0:((cyw_buff0_used && cyr_buff0_thd0)? false:cyr_buff0_thd0)));
  // file mix052.c line 40 function main
  cyr_buff1_thd0=(weakchoice2? cyr_buff1_thd0:(((!cyw_buff0_used) || (((!cyr_buff0_thd0) && (!cyw_buff1_used)) || ((!cyr_buff0_thd0) && (!cyr_buff1_thd0))))? cyr_buff1_thd0:((cyw_buff0_used && cyr_buff0_thd0)? false:false)));
  // file mix052.c line 40 function main
  tmp_guard1=(!(((y==2) && (__unbuffered_p1_r3==2)) && (__unbuffered_p1_r7==0)));
  // file mix052.c line 40 function main
  y=(cyflush_delayed? cymem_tmp:y);
  // file mix052.c line 40 function main
  cyflush_delayed=false;
  // file mix052.c line 40 function main
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file mix052.c line 40 function main
  assert(tmp_guard1);
  // file mix052.c line 41 function main
  return 0;
  // file mix052.c line 42 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 mix052.c line 1
  __unbuffered_cnt=0;
  // file mix052.c line 2
  __unbuffered_p0_r1=0;
  // file mix052.c line 3
  __unbuffered_p0_r3=0;
  // file mix052.c line 4
  __unbuffered_p1_r1=0;
  // file mix052.c line 5
  __unbuffered_p1_r3=0;
  // file mix052.c line 6
  __unbuffered_p1_r4=0;
  // file mix052.c line 7
  __unbuffered_p1_r5=0;
  // file mix052.c line 8
  __unbuffered_p1_r7=0;
  // file mix052.c line 9
  x=0;
  // file mix052.c line 10
  y=0;
  // file mix052.c line 11
  z=0;
}