// c::worker_1
// file pgsql_two-fix.c line 42
void * worker_1(void *);

// c::worker_2
// file pgsql_two-fix.c line 61
void * worker_2(void *);

// c::main
// file pgsql_two-fix.c line 94
int _main(void);

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

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

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

// c::worker_1$tmp_guard1
// 
_Bool tmp_guard1;

// c::worker_1$tmp_guard2
// 
_Bool tmp_guard2;

// c::worker_2$tmp_guard0
// 
_Bool tmp_guard3;

// c::worker_2$tmp_guard1
// 
_Bool tmp_guard4;

// c::worker_2$tmp_guard2
// 
_Bool tmp_guard5;

// c::latch1$w_buff0
// 
_Bool clatch1w_buff0;

// c::latch1$w_buff1
// 
_Bool clatch1w_buff1;

// c::latch1$w_buff0_used
// 
_Bool clatch1w_buff0_used;

// c::latch1$w_buff1_used
// 
_Bool clatch1w_buff1_used;

// c::latch1$mem_tmp
// 
_Bool clatch1mem_tmp;

// c::latch1$flush_delayed
// 
_Bool clatch1flush_delayed;

// c::latch1$read_delayed
// 
_Bool clatch1read_delayed;

// c::latch1$read_delayed_var
// 
_Bool * clatch1read_delayed_var;

// c::latch1$r_buff0_thd0
// 
_Bool clatch1r_buff0_thd0;

// c::latch1$r_buff1_thd0
// 
_Bool clatch1r_buff1_thd0;

// c::latch1$r_buff0_thd1
// 
_Bool clatch1r_buff0_thd1;

// c::latch1$r_buff1_thd1
// 
_Bool clatch1r_buff1_thd1;

// c::latch1$r_buff0_thd2
// 
_Bool clatch1r_buff0_thd2;

// c::latch1$r_buff1_thd2
// 
_Bool clatch1r_buff1_thd2;

// weak::choice0
// 
_Bool weakchoice0;

// weak::choice2
// 
_Bool weakchoice2;

// c::worker_1$tmp_guard0$w_buff0
// 
_Bool cworker_1tmp_guard0w_buff0;

// c::worker_1$tmp_guard0$w_buff1
// 
_Bool cworker_1tmp_guard0w_buff1;

// c::worker_1$tmp_guard0$w_buff0_used
// 
_Bool cworker_1tmp_guard0w_buff0_used;

// c::worker_1$tmp_guard0$w_buff1_used
// 
_Bool cworker_1tmp_guard0w_buff1_used;

// c::worker_1$tmp_guard0$mem_tmp
// 
_Bool cworker_1tmp_guard0mem_tmp;

// c::worker_1$tmp_guard0$flush_delayed
// 
_Bool cworker_1tmp_guard0flush_delayed;

// c::worker_1$tmp_guard0$read_delayed
// 
_Bool cworker_1tmp_guard0read_delayed;

// c::worker_1$tmp_guard0$read_delayed_var
// 
_Bool * cworker_1tmp_guard0read_delayed_var;

// c::worker_1$tmp_guard0$r_buff0_thd0
// 
_Bool cworker_1tmp_guard0r_buff0_thd0;

// c::worker_1$tmp_guard0$r_buff1_thd0
// 
_Bool cworker_1tmp_guard0r_buff1_thd0;

// c::worker_1$tmp_guard0$r_buff0_thd1
// 
_Bool cworker_1tmp_guard0r_buff0_thd1;

// c::worker_1$tmp_guard0$r_buff1_thd1
// 
_Bool cworker_1tmp_guard0r_buff1_thd1;

// c::worker_1$tmp_guard0$r_buff0_thd2
// 
_Bool cworker_1tmp_guard0r_buff0_thd2;

// c::worker_1$tmp_guard0$r_buff1_thd2
// 
_Bool cworker_1tmp_guard0r_buff1_thd2;

// c::flag1$w_buff0
// 
_Bool cflag1w_buff0;

// c::flag1$w_buff1
// 
_Bool cflag1w_buff1;

// c::flag1$w_buff0_used
// 
_Bool cflag1w_buff0_used;

// c::flag1$w_buff1_used
// 
_Bool cflag1w_buff1_used;

// c::flag1$mem_tmp
// 
_Bool cflag1mem_tmp;

// c::flag1$flush_delayed
// 
_Bool cflag1flush_delayed;

// c::flag1$read_delayed
// 
_Bool cflag1read_delayed;

// c::flag1$read_delayed_var
// 
_Bool * cflag1read_delayed_var;

// c::flag1$r_buff0_thd0
// 
_Bool cflag1r_buff0_thd0;

// c::flag1$r_buff1_thd0
// 
_Bool cflag1r_buff1_thd0;

// c::flag1$r_buff0_thd1
// 
_Bool cflag1r_buff0_thd1;

// c::flag1$r_buff1_thd1
// 
_Bool cflag1r_buff1_thd1;

// c::flag1$r_buff0_thd2
// 
_Bool cflag1r_buff0_thd2;

// c::flag1$r_buff1_thd2
// 
_Bool cflag1r_buff1_thd2;

// c::worker_1$tmp_guard2$w_buff0
// 
_Bool cworker_1tmp_guard2w_buff0;

// c::worker_1$tmp_guard2$w_buff1
// 
_Bool cworker_1tmp_guard2w_buff1;

// c::worker_1$tmp_guard2$w_buff0_used
// 
_Bool cworker_1tmp_guard2w_buff0_used;

// c::worker_1$tmp_guard2$w_buff1_used
// 
_Bool cworker_1tmp_guard2w_buff1_used;

// c::worker_1$tmp_guard2$mem_tmp
// 
_Bool cworker_1tmp_guard2mem_tmp;

// c::worker_1$tmp_guard2$flush_delayed
// 
_Bool cworker_1tmp_guard2flush_delayed;

// c::worker_1$tmp_guard2$read_delayed
// 
_Bool cworker_1tmp_guard2read_delayed;

// c::worker_1$tmp_guard2$read_delayed_var
// 
_Bool * cworker_1tmp_guard2read_delayed_var;

// c::worker_1$tmp_guard2$r_buff0_thd0
// 
_Bool cworker_1tmp_guard2r_buff0_thd0;

// c::worker_1$tmp_guard2$r_buff1_thd0
// 
_Bool cworker_1tmp_guard2r_buff1_thd0;

// c::worker_1$tmp_guard2$r_buff0_thd1
// 
_Bool cworker_1tmp_guard2r_buff0_thd1;

// c::worker_1$tmp_guard2$r_buff1_thd1
// 
_Bool cworker_1tmp_guard2r_buff1_thd1;

// c::worker_1$tmp_guard2$r_buff0_thd2
// 
_Bool cworker_1tmp_guard2r_buff0_thd2;

// c::worker_1$tmp_guard2$r_buff1_thd2
// 
_Bool cworker_1tmp_guard2r_buff1_thd2;

// c::latch2$w_buff0
// 
_Bool clatch2w_buff0;

// c::latch2$w_buff1
// 
_Bool clatch2w_buff1;

// c::latch2$w_buff0_used
// 
_Bool clatch2w_buff0_used;

// c::latch2$w_buff1_used
// 
_Bool clatch2w_buff1_used;

// c::latch2$mem_tmp
// 
_Bool clatch2mem_tmp;

// c::latch2$flush_delayed
// 
_Bool clatch2flush_delayed;

// c::latch2$read_delayed
// 
_Bool clatch2read_delayed;

// c::latch2$read_delayed_var
// 
_Bool * clatch2read_delayed_var;

// c::latch2$r_buff0_thd0
// 
_Bool clatch2r_buff0_thd0;

// c::latch2$r_buff1_thd0
// 
_Bool clatch2r_buff1_thd0;

// c::latch2$r_buff0_thd1
// 
_Bool clatch2r_buff0_thd1;

// c::latch2$r_buff1_thd1
// 
_Bool clatch2r_buff1_thd1;

// c::latch2$r_buff0_thd2
// 
_Bool clatch2r_buff0_thd2;

// c::latch2$r_buff1_thd2
// 
_Bool clatch2r_buff1_thd2;

// c::worker_2$tmp_guard0$w_buff0
// 
_Bool cworker_2tmp_guard0w_buff0;

// c::worker_2$tmp_guard0$w_buff1
// 
_Bool cworker_2tmp_guard0w_buff1;

// c::worker_2$tmp_guard0$w_buff0_used
// 
_Bool cworker_2tmp_guard0w_buff0_used;

// c::worker_2$tmp_guard0$w_buff1_used
// 
_Bool cworker_2tmp_guard0w_buff1_used;

// c::worker_2$tmp_guard0$mem_tmp
// 
_Bool cworker_2tmp_guard0mem_tmp;

// c::worker_2$tmp_guard0$flush_delayed
// 
_Bool cworker_2tmp_guard0flush_delayed;

// c::worker_2$tmp_guard0$read_delayed
// 
_Bool cworker_2tmp_guard0read_delayed;

// c::worker_2$tmp_guard0$read_delayed_var
// 
_Bool * cworker_2tmp_guard0read_delayed_var;

// c::worker_2$tmp_guard0$r_buff0_thd0
// 
_Bool cworker_2tmp_guard0r_buff0_thd0;

// c::worker_2$tmp_guard0$r_buff1_thd0
// 
_Bool cworker_2tmp_guard0r_buff1_thd0;

// c::worker_2$tmp_guard0$r_buff0_thd1
// 
_Bool cworker_2tmp_guard0r_buff0_thd1;

// c::worker_2$tmp_guard0$r_buff1_thd1
// 
_Bool cworker_2tmp_guard0r_buff1_thd1;

// c::worker_2$tmp_guard0$r_buff0_thd2
// 
_Bool cworker_2tmp_guard0r_buff0_thd2;

// c::worker_2$tmp_guard0$r_buff1_thd2
// 
_Bool cworker_2tmp_guard0r_buff1_thd2;

// c::latch1
// file pgsql_two-fix.c line 6
_Bool latch1;

// c::flag1
// file pgsql_two-fix.c line 7
_Bool flag1;

// c::latch2
// file pgsql_two-fix.c line 8
_Bool latch2;

// c::flag2
// file pgsql_two-fix.c line 8
_Bool flag2;

// c::__unbuffered_tmp2
// file pgsql_two-fix.c line 14
_Bool __unbuffered_tmp2;

// main
// 
int main(void)
{
  clatch1w_buff0_used=false;
  clatch1w_buff1_used=false;
  clatch1flush_delayed=false;
  clatch1read_delayed=false;
  clatch1read_delayed_var=0;
  clatch1r_buff0_thd0=false;
  clatch1r_buff0_thd1=false;
  clatch1r_buff0_thd2=false;
  clatch1r_buff1_thd0=false;
  clatch1r_buff1_thd1=false;
  clatch1r_buff1_thd2=false;
  cflag1w_buff0_used=false;
  cflag1w_buff1_used=false;
  cflag1flush_delayed=false;
  cflag1read_delayed=false;
  cflag1read_delayed_var=0;
  cflag1r_buff0_thd0=false;
  cflag1r_buff0_thd1=false;
  cflag1r_buff0_thd2=false;
  cflag1r_buff1_thd0=false;
  cflag1r_buff1_thd1=false;
  cflag1r_buff1_thd2=false;
  clatch2w_buff0_used=false;
  clatch2w_buff1_used=false;
  clatch2flush_delayed=false;
  clatch2read_delayed=false;
  clatch2read_delayed_var=0;
  clatch2r_buff0_thd0=false;
  clatch2r_buff0_thd1=false;
  clatch2r_buff0_thd2=false;
  clatch2r_buff1_thd0=false;
  clatch2r_buff1_thd1=false;
  clatch2r_buff1_thd2=false;
  cworker_1tmp_guard0w_buff0_used=false;
  cworker_1tmp_guard0w_buff1_used=false;
  cworker_1tmp_guard0flush_delayed=false;
  cworker_1tmp_guard0read_delayed=false;
  cworker_1tmp_guard0read_delayed_var=0;
  cworker_1tmp_guard0r_buff0_thd0=false;
  cworker_1tmp_guard0r_buff0_thd1=false;
  cworker_1tmp_guard0r_buff0_thd2=false;
  cworker_1tmp_guard0r_buff1_thd0=false;
  cworker_1tmp_guard0r_buff1_thd1=false;
  cworker_1tmp_guard0r_buff1_thd2=false;
  cworker_1tmp_guard2w_buff0_used=false;
  cworker_1tmp_guard2w_buff1_used=false;
  cworker_1tmp_guard2flush_delayed=false;
  cworker_1tmp_guard2read_delayed=false;
  cworker_1tmp_guard2read_delayed_var=0;
  cworker_1tmp_guard2r_buff0_thd0=false;
  cworker_1tmp_guard2r_buff0_thd1=false;
  cworker_1tmp_guard2r_buff0_thd2=false;
  cworker_1tmp_guard2r_buff1_thd0=false;
  cworker_1tmp_guard2r_buff1_thd1=false;
  cworker_1tmp_guard2r_buff1_thd2=false;
  cworker_2tmp_guard0w_buff0_used=false;
  cworker_2tmp_guard0w_buff1_used=false;
  cworker_2tmp_guard0flush_delayed=false;
  cworker_2tmp_guard0read_delayed=false;
  cworker_2tmp_guard0read_delayed_var=0;
  cworker_2tmp_guard0r_buff0_thd0=false;
  cworker_2tmp_guard0r_buff0_thd1=false;
  cworker_2tmp_guard0r_buff0_thd2=false;
  cworker_2tmp_guard0r_buff1_thd0=false;
  cworker_2tmp_guard0r_buff1_thd1=false;
  cworker_2tmp_guard0r_buff1_thd2=false;
  __CPROVER_initialize();
  _main();
}

// c::worker_1
// file pgsql_two-fix.c line 42
void * worker_1(void * arg)
{
  // file pgsql_two-fix.c line 47 function worker_1
L1:
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 47 function worker_1
  weakchoice0=nondet_bool();
  // file pgsql_two-fix.c line 47 function worker_1
  weakchoice2=nondet_bool();
  // file pgsql_two-fix.c line 47 function worker_1
  clatch1flush_delayed=weakchoice2;
  // file pgsql_two-fix.c line 47 function worker_1
  clatch1mem_tmp=latch1;
  // file pgsql_two-fix.c line 47 function worker_1
  latch1=(((!clatch1w_buff0_used) || (((!clatch1r_buff0_thd1) && (!clatch1w_buff1_used)) || ((!clatch1r_buff0_thd1) && (!clatch1r_buff1_thd1))))? latch1:((clatch1w_buff0_used && clatch1r_buff0_thd1)? clatch1w_buff0:clatch1w_buff1));
  // file pgsql_two-fix.c line 47 function worker_1
  clatch1w_buff0=(weakchoice2? clatch1w_buff0:(((!clatch1w_buff0_used) || (((!clatch1r_buff0_thd1) && (!clatch1w_buff1_used)) || ((!clatch1r_buff0_thd1) && (!clatch1r_buff1_thd1))))? clatch1w_buff0:((clatch1w_buff0_used && clatch1r_buff0_thd1)? clatch1w_buff0:clatch1w_buff0)));
  // file pgsql_two-fix.c line 47 function worker_1
  clatch1w_buff1=(weakchoice2? clatch1w_buff1:(((!clatch1w_buff0_used) || (((!clatch1r_buff0_thd1) && (!clatch1w_buff1_used)) || ((!clatch1r_buff0_thd1) && (!clatch1r_buff1_thd1))))? clatch1w_buff1:((clatch1w_buff0_used && clatch1r_buff0_thd1)? clatch1w_buff1:clatch1w_buff1)));
  // file pgsql_two-fix.c line 47 function worker_1
  clatch1w_buff0_used=(weakchoice2? clatch1w_buff0_used:(((!clatch1w_buff0_used) || (((!clatch1r_buff0_thd1) && (!clatch1w_buff1_used)) || ((!clatch1r_buff0_thd1) && (!clatch1r_buff1_thd1))))? clatch1w_buff0_used:((clatch1w_buff0_used && clatch1r_buff0_thd1)? false:clatch1w_buff0_used)));
  // file pgsql_two-fix.c line 47 function worker_1
  clatch1w_buff1_used=(weakchoice2? clatch1w_buff1_used:(((!clatch1w_buff0_used) || (((!clatch1r_buff0_thd1) && (!clatch1w_buff1_used)) || ((!clatch1r_buff0_thd1) && (!clatch1r_buff1_thd1))))? clatch1w_buff1_used:((clatch1w_buff0_used && clatch1r_buff0_thd1)? false:false)));
  // file pgsql_two-fix.c line 47 function worker_1
  clatch1r_buff0_thd1=(weakchoice2? clatch1r_buff0_thd1:(((!clatch1w_buff0_used) || (((!clatch1r_buff0_thd1) && (!clatch1w_buff1_used)) || ((!clatch1r_buff0_thd1) && (!clatch1r_buff1_thd1))))? clatch1r_buff0_thd1:((clatch1w_buff0_used && clatch1r_buff0_thd1)? false:clatch1r_buff0_thd1)));
  // file pgsql_two-fix.c line 47 function worker_1
  clatch1r_buff1_thd1=(weakchoice2? clatch1r_buff1_thd1:(((!clatch1w_buff0_used) || (((!clatch1r_buff0_thd1) && (!clatch1w_buff1_used)) || ((!clatch1r_buff0_thd1) && (!clatch1r_buff1_thd1))))? clatch1r_buff1_thd1:((clatch1w_buff0_used && clatch1r_buff0_thd1)? false:false)));
  // file pgsql_two-fix.c line 47 function worker_1
  cworker_1tmp_guard0read_delayed=true;
  // file pgsql_two-fix.c line 47 function worker_1
  cworker_1tmp_guard0read_delayed_var=(&latch1);
  // file pgsql_two-fix.c line 47 function worker_1
  tmp_guard=(!(!latch1));
  // file pgsql_two-fix.c line 47 function worker_1
  latch1=(clatch1flush_delayed? clatch1mem_tmp:latch1);
  // file pgsql_two-fix.c line 47 function worker_1
  clatch1flush_delayed=false;
  // file pgsql_two-fix.c line 47 function worker_1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 47 function worker_1
  if( tmp_guard ) goto L2;
  // file pgsql_two-fix.c line 47 function worker_1
  goto L1;
  // file pgsql_two-fix.c line 48 function worker_1
L2:
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 48 function worker_1
  weakchoice0=nondet_bool();
  // file pgsql_two-fix.c line 48 function worker_1
  weakchoice2=nondet_bool();
  // file pgsql_two-fix.c line 48 function worker_1
  cflag1flush_delayed=weakchoice2;
  // file pgsql_two-fix.c line 48 function worker_1
  cflag1mem_tmp=flag1;
  // file pgsql_two-fix.c line 48 function worker_1
  flag1=(((!cflag1w_buff0_used) || (((!cflag1r_buff0_thd1) && (!cflag1w_buff1_used)) || ((!cflag1r_buff0_thd1) && (!cflag1r_buff1_thd1))))? flag1:((cflag1w_buff0_used && cflag1r_buff0_thd1)? cflag1w_buff0:cflag1w_buff1));
  // file pgsql_two-fix.c line 48 function worker_1
  cflag1w_buff0=(weakchoice2? cflag1w_buff0:(((!cflag1w_buff0_used) || (((!cflag1r_buff0_thd1) && (!cflag1w_buff1_used)) || ((!cflag1r_buff0_thd1) && (!cflag1r_buff1_thd1))))? cflag1w_buff0:((cflag1w_buff0_used && cflag1r_buff0_thd1)? cflag1w_buff0:cflag1w_buff0)));
  // file pgsql_two-fix.c line 48 function worker_1
  cflag1w_buff1=(weakchoice2? cflag1w_buff1:(((!cflag1w_buff0_used) || (((!cflag1r_buff0_thd1) && (!cflag1w_buff1_used)) || ((!cflag1r_buff0_thd1) && (!cflag1r_buff1_thd1))))? cflag1w_buff1:((cflag1w_buff0_used && cflag1r_buff0_thd1)? cflag1w_buff1:cflag1w_buff1)));
  // file pgsql_two-fix.c line 48 function worker_1
  cflag1w_buff0_used=(weakchoice2? cflag1w_buff0_used:(((!cflag1w_buff0_used) || (((!cflag1r_buff0_thd1) && (!cflag1w_buff1_used)) || ((!cflag1r_buff0_thd1) && (!cflag1r_buff1_thd1))))? cflag1w_buff0_used:((cflag1w_buff0_used && cflag1r_buff0_thd1)? false:cflag1w_buff0_used)));
  // file pgsql_two-fix.c line 48 function worker_1
  cflag1w_buff1_used=(weakchoice2? cflag1w_buff1_used:(((!cflag1w_buff0_used) || (((!cflag1r_buff0_thd1) && (!cflag1w_buff1_used)) || ((!cflag1r_buff0_thd1) && (!cflag1r_buff1_thd1))))? cflag1w_buff1_used:((cflag1w_buff0_used && cflag1r_buff0_thd1)? false:false)));
  // file pgsql_two-fix.c line 48 function worker_1
  cflag1r_buff0_thd1=(weakchoice2? cflag1r_buff0_thd1:(((!cflag1w_buff0_used) || (((!cflag1r_buff0_thd1) && (!cflag1w_buff1_used)) || ((!cflag1r_buff0_thd1) && (!cflag1r_buff1_thd1))))? cflag1r_buff0_thd1:((cflag1w_buff0_used && cflag1r_buff0_thd1)? false:cflag1r_buff0_thd1)));
  // file pgsql_two-fix.c line 48 function worker_1
  cflag1r_buff1_thd1=(weakchoice2? cflag1r_buff1_thd1:(((!cflag1w_buff0_used) || (((!cflag1r_buff0_thd1) && (!cflag1w_buff1_used)) || ((!cflag1r_buff0_thd1) && (!cflag1r_buff1_thd1))))? cflag1r_buff1_thd1:((cflag1w_buff0_used && cflag1r_buff0_thd1)? false:false)));
  // file pgsql_two-fix.c line 48 function worker_1
  weakchoice0=nondet_bool();
  // file pgsql_two-fix.c line 48 function worker_1
  weakchoice2=nondet_bool();
  // file pgsql_two-fix.c line 48 function worker_1
  clatch1flush_delayed=weakchoice2;
  // file pgsql_two-fix.c line 48 function worker_1
  clatch1mem_tmp=latch1;
  // file pgsql_two-fix.c line 48 function worker_1
  latch1=(((!clatch1w_buff0_used) || (((!clatch1r_buff0_thd1) && (!clatch1w_buff1_used)) || ((!clatch1r_buff0_thd1) && (!clatch1r_buff1_thd1))))? latch1:((clatch1w_buff0_used && clatch1r_buff0_thd1)? clatch1w_buff0:clatch1w_buff1));
  // file pgsql_two-fix.c line 48 function worker_1
  clatch1w_buff0=(weakchoice2? clatch1w_buff0:(((!clatch1w_buff0_used) || (((!clatch1r_buff0_thd1) && (!clatch1w_buff1_used)) || ((!clatch1r_buff0_thd1) && (!clatch1r_buff1_thd1))))? clatch1w_buff0:((clatch1w_buff0_used && clatch1r_buff0_thd1)? clatch1w_buff0:clatch1w_buff0)));
  // file pgsql_two-fix.c line 48 function worker_1
  clatch1w_buff1=(weakchoice2? clatch1w_buff1:(((!clatch1w_buff0_used) || (((!clatch1r_buff0_thd1) && (!clatch1w_buff1_used)) || ((!clatch1r_buff0_thd1) && (!clatch1r_buff1_thd1))))? clatch1w_buff1:((clatch1w_buff0_used && clatch1r_buff0_thd1)? clatch1w_buff1:clatch1w_buff1)));
  // file pgsql_two-fix.c line 48 function worker_1
  clatch1w_buff0_used=(weakchoice2? clatch1w_buff0_used:(((!clatch1w_buff0_used) || (((!clatch1r_buff0_thd1) && (!clatch1w_buff1_used)) || ((!clatch1r_buff0_thd1) && (!clatch1r_buff1_thd1))))? clatch1w_buff0_used:((clatch1w_buff0_used && clatch1r_buff0_thd1)? false:clatch1w_buff0_used)));
  // file pgsql_two-fix.c line 48 function worker_1
  clatch1w_buff1_used=(weakchoice2? clatch1w_buff1_used:(((!clatch1w_buff0_used) || (((!clatch1r_buff0_thd1) && (!clatch1w_buff1_used)) || ((!clatch1r_buff0_thd1) && (!clatch1r_buff1_thd1))))? clatch1w_buff1_used:((clatch1w_buff0_used && clatch1r_buff0_thd1)? false:false)));
  // file pgsql_two-fix.c line 48 function worker_1
  clatch1r_buff0_thd1=(weakchoice2? clatch1r_buff0_thd1:(((!clatch1w_buff0_used) || (((!clatch1r_buff0_thd1) && (!clatch1w_buff1_used)) || ((!clatch1r_buff0_thd1) && (!clatch1r_buff1_thd1))))? clatch1r_buff0_thd1:((clatch1w_buff0_used && clatch1r_buff0_thd1)? false:clatch1r_buff0_thd1)));
  // file pgsql_two-fix.c line 48 function worker_1
  clatch1r_buff1_thd1=(weakchoice2? clatch1r_buff1_thd1:(((!clatch1w_buff0_used) || (((!clatch1r_buff0_thd1) && (!clatch1w_buff1_used)) || ((!clatch1r_buff0_thd1) && (!clatch1r_buff1_thd1))))? clatch1r_buff1_thd1:((clatch1w_buff0_used && clatch1r_buff0_thd1)? false:false)));
  // file pgsql_two-fix.c line 48 function worker_1
  tmp_guard1=((!latch1) || flag1);
  // file pgsql_two-fix.c line 48 function worker_1
  flag1=(cflag1flush_delayed? cflag1mem_tmp:flag1);
  // file pgsql_two-fix.c line 48 function worker_1
  cflag1flush_delayed=false;
  // file pgsql_two-fix.c line 48 function worker_1
  latch1=(clatch1flush_delayed? clatch1mem_tmp:latch1);
  // file pgsql_two-fix.c line 48 function worker_1
  clatch1flush_delayed=false;
  // file pgsql_two-fix.c line 48 function worker_1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 48 function worker_1
  assert(tmp_guard1);
  // file pgsql_two-fix.c line 49 function worker_1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 49 function worker_1
  clatch1w_buff1=clatch1w_buff0;
  // file pgsql_two-fix.c line 49 function worker_1
  clatch1w_buff0=(_Bool)(0);
  // file pgsql_two-fix.c line 49 function worker_1
  clatch1w_buff1_used=clatch1w_buff0_used;
  // file pgsql_two-fix.c line 49 function worker_1
  clatch1w_buff0_used=true;
  // file pgsql_two-fix.c line 49 function worker_1
  assert((!(clatch1w_buff1_used && clatch1w_buff0_used)));
  // file pgsql_two-fix.c line 49 function worker_1
  clatch1r_buff1_thd0=clatch1r_buff0_thd0;
  // file pgsql_two-fix.c line 49 function worker_1
  clatch1r_buff1_thd1=clatch1r_buff0_thd1;
  // file pgsql_two-fix.c line 49 function worker_1
  clatch1r_buff1_thd2=clatch1r_buff0_thd2;
  // file pgsql_two-fix.c line 49 function worker_1
  clatch1r_buff0_thd1=true;
  // file pgsql_two-fix.c line 49 function worker_1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 50 function worker_1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 50 function worker_1
  weakchoice0=nondet_bool();
  // file pgsql_two-fix.c line 50 function worker_1
  weakchoice2=nondet_bool();
  // file pgsql_two-fix.c line 50 function worker_1
  cflag1flush_delayed=weakchoice2;
  // file pgsql_two-fix.c line 50 function worker_1
  cflag1mem_tmp=flag1;
  // file pgsql_two-fix.c line 50 function worker_1
  flag1=(((!cflag1w_buff0_used) || (((!cflag1r_buff0_thd1) && (!cflag1w_buff1_used)) || ((!cflag1r_buff0_thd1) && (!cflag1r_buff1_thd1))))? flag1:((cflag1w_buff0_used && cflag1r_buff0_thd1)? cflag1w_buff0:cflag1w_buff1));
  // file pgsql_two-fix.c line 50 function worker_1
  cflag1w_buff0=(weakchoice2? cflag1w_buff0:(((!cflag1w_buff0_used) || (((!cflag1r_buff0_thd1) && (!cflag1w_buff1_used)) || ((!cflag1r_buff0_thd1) && (!cflag1r_buff1_thd1))))? cflag1w_buff0:((cflag1w_buff0_used && cflag1r_buff0_thd1)? cflag1w_buff0:cflag1w_buff0)));
  // file pgsql_two-fix.c line 50 function worker_1
  cflag1w_buff1=(weakchoice2? cflag1w_buff1:(((!cflag1w_buff0_used) || (((!cflag1r_buff0_thd1) && (!cflag1w_buff1_used)) || ((!cflag1r_buff0_thd1) && (!cflag1r_buff1_thd1))))? cflag1w_buff1:((cflag1w_buff0_used && cflag1r_buff0_thd1)? cflag1w_buff1:cflag1w_buff1)));
  // file pgsql_two-fix.c line 50 function worker_1
  cflag1w_buff0_used=(weakchoice2? cflag1w_buff0_used:(((!cflag1w_buff0_used) || (((!cflag1r_buff0_thd1) && (!cflag1w_buff1_used)) || ((!cflag1r_buff0_thd1) && (!cflag1r_buff1_thd1))))? cflag1w_buff0_used:((cflag1w_buff0_used && cflag1r_buff0_thd1)? false:cflag1w_buff0_used)));
  // file pgsql_two-fix.c line 50 function worker_1
  cflag1w_buff1_used=(weakchoice2? cflag1w_buff1_used:(((!cflag1w_buff0_used) || (((!cflag1r_buff0_thd1) && (!cflag1w_buff1_used)) || ((!cflag1r_buff0_thd1) && (!cflag1r_buff1_thd1))))? cflag1w_buff1_used:((cflag1w_buff0_used && cflag1r_buff0_thd1)? false:false)));
  // file pgsql_two-fix.c line 50 function worker_1
  cflag1r_buff0_thd1=(weakchoice2? cflag1r_buff0_thd1:(((!cflag1w_buff0_used) || (((!cflag1r_buff0_thd1) && (!cflag1w_buff1_used)) || ((!cflag1r_buff0_thd1) && (!cflag1r_buff1_thd1))))? cflag1r_buff0_thd1:((cflag1w_buff0_used && cflag1r_buff0_thd1)? false:cflag1r_buff0_thd1)));
  // file pgsql_two-fix.c line 50 function worker_1
  cflag1r_buff1_thd1=(weakchoice2? cflag1r_buff1_thd1:(((!cflag1w_buff0_used) || (((!cflag1r_buff0_thd1) && (!cflag1w_buff1_used)) || ((!cflag1r_buff0_thd1) && (!cflag1r_buff1_thd1))))? cflag1r_buff1_thd1:((cflag1w_buff0_used && cflag1r_buff0_thd1)? false:false)));
  // file pgsql_two-fix.c line 50 function worker_1
  cworker_1tmp_guard2read_delayed=true;
  // file pgsql_two-fix.c line 50 function worker_1
  cworker_1tmp_guard2read_delayed_var=(&flag1);
  // file pgsql_two-fix.c line 50 function worker_1
  tmp_guard2=(!flag1);
  // file pgsql_two-fix.c line 50 function worker_1
  flag1=(cflag1flush_delayed? cflag1mem_tmp:flag1);
  // file pgsql_two-fix.c line 50 function worker_1
  cflag1flush_delayed=false;
  // file pgsql_two-fix.c line 50 function worker_1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 50 function worker_1
  if( tmp_guard2 ) goto L3;
  // file pgsql_two-fix.c line 52 function worker_1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 52 function worker_1
  flag1=(_Bool)(0);
  // file pgsql_two-fix.c line 52 function worker_1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 53 function worker_1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 53 function worker_1
  flag2=(_Bool)(1);
  // file pgsql_two-fix.c line 53 function worker_1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 54 function worker_1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 54 function worker_1
  latch2=(_Bool)(1);
  // file pgsql_two-fix.c line 54 function worker_1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 45 function worker_1
L3:
  goto L1;
  // file pgsql_two-fix.c line 59 function worker_1
  return nondet_ptr();
  // file pgsql_two-fix.c line 59 function worker_1
}

// c::worker_2
// file pgsql_two-fix.c line 61
void * worker_2(void * arg1)
{
  // file pgsql_two-fix.c line 66 function worker_2
L1:
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 66 function worker_2
  weakchoice0=nondet_bool();
  // file pgsql_two-fix.c line 66 function worker_2
  weakchoice2=nondet_bool();
  // file pgsql_two-fix.c line 66 function worker_2
  clatch2flush_delayed=weakchoice2;
  // file pgsql_two-fix.c line 66 function worker_2
  clatch2mem_tmp=latch2;
  // file pgsql_two-fix.c line 66 function worker_2
  latch2=(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? latch2:((clatch2w_buff0_used && clatch2r_buff0_thd2)? clatch2w_buff0:clatch2w_buff1));
  // file pgsql_two-fix.c line 66 function worker_2
  clatch2w_buff0=(weakchoice2? clatch2w_buff0:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2w_buff0:((clatch2w_buff0_used && clatch2r_buff0_thd2)? clatch2w_buff0:clatch2w_buff0)));
  // file pgsql_two-fix.c line 66 function worker_2
  clatch2w_buff1=(weakchoice2? clatch2w_buff1:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2w_buff1:((clatch2w_buff0_used && clatch2r_buff0_thd2)? clatch2w_buff1:clatch2w_buff1)));
  // file pgsql_two-fix.c line 66 function worker_2
  clatch2w_buff0_used=(weakchoice2? clatch2w_buff0_used:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2w_buff0_used:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:clatch2w_buff0_used)));
  // file pgsql_two-fix.c line 66 function worker_2
  clatch2w_buff1_used=(weakchoice2? clatch2w_buff1_used:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2w_buff1_used:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:false)));
  // file pgsql_two-fix.c line 66 function worker_2
  clatch2r_buff0_thd2=(weakchoice2? clatch2r_buff0_thd2:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2r_buff0_thd2:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:clatch2r_buff0_thd2)));
  // file pgsql_two-fix.c line 66 function worker_2
  clatch2r_buff1_thd2=(weakchoice2? clatch2r_buff1_thd2:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2r_buff1_thd2:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:false)));
  // file pgsql_two-fix.c line 66 function worker_2
  cworker_2tmp_guard0read_delayed=true;
  // file pgsql_two-fix.c line 66 function worker_2
  cworker_2tmp_guard0read_delayed_var=(&latch2);
  // file pgsql_two-fix.c line 66 function worker_2
  tmp_guard3=(!(!latch2));
  // file pgsql_two-fix.c line 66 function worker_2
  latch2=(clatch2flush_delayed? clatch2mem_tmp:latch2);
  // file pgsql_two-fix.c line 66 function worker_2
  clatch2flush_delayed=false;
  // file pgsql_two-fix.c line 66 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 66 function worker_2
  if( tmp_guard3 ) goto L2;
  // file pgsql_two-fix.c line 66 function worker_2
  goto L1;
  // file pgsql_two-fix.c line 67 function worker_2
L2:
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 67 function worker_2
  weakchoice0=nondet_bool();
  // file pgsql_two-fix.c line 67 function worker_2
  weakchoice2=nondet_bool();
  // file pgsql_two-fix.c line 67 function worker_2
  clatch2flush_delayed=weakchoice2;
  // file pgsql_two-fix.c line 67 function worker_2
  clatch2mem_tmp=latch2;
  // file pgsql_two-fix.c line 67 function worker_2
  latch2=(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? latch2:((clatch2w_buff0_used && clatch2r_buff0_thd2)? clatch2w_buff0:clatch2w_buff1));
  // file pgsql_two-fix.c line 67 function worker_2
  clatch2w_buff0=(weakchoice2? clatch2w_buff0:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2w_buff0:((clatch2w_buff0_used && clatch2r_buff0_thd2)? clatch2w_buff0:clatch2w_buff0)));
  // file pgsql_two-fix.c line 67 function worker_2
  clatch2w_buff1=(weakchoice2? clatch2w_buff1:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2w_buff1:((clatch2w_buff0_used && clatch2r_buff0_thd2)? clatch2w_buff1:clatch2w_buff1)));
  // file pgsql_two-fix.c line 67 function worker_2
  clatch2w_buff0_used=(weakchoice2? clatch2w_buff0_used:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2w_buff0_used:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:clatch2w_buff0_used)));
  // file pgsql_two-fix.c line 67 function worker_2
  clatch2w_buff1_used=(weakchoice2? clatch2w_buff1_used:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2w_buff1_used:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:false)));
  // file pgsql_two-fix.c line 67 function worker_2
  clatch2r_buff0_thd2=(weakchoice2? clatch2r_buff0_thd2:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2r_buff0_thd2:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:clatch2r_buff0_thd2)));
  // file pgsql_two-fix.c line 67 function worker_2
  clatch2r_buff1_thd2=(weakchoice2? clatch2r_buff1_thd2:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2r_buff1_thd2:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:false)));
  // file pgsql_two-fix.c line 67 function worker_2
  tmp_guard4=((!latch2) || flag2);
  // file pgsql_two-fix.c line 67 function worker_2
  latch2=(clatch2flush_delayed? clatch2mem_tmp:latch2);
  // file pgsql_two-fix.c line 67 function worker_2
  clatch2flush_delayed=false;
  // file pgsql_two-fix.c line 67 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 67 function worker_2
  assert(tmp_guard4);
  // file pgsql_two-fix.c line 68 function worker_2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 68 function worker_2
  clatch2w_buff1=clatch2w_buff0;
  // file pgsql_two-fix.c line 68 function worker_2
  clatch2w_buff0=(_Bool)(0);
  // file pgsql_two-fix.c line 68 function worker_2
  clatch2w_buff1_used=clatch2w_buff0_used;
  // file pgsql_two-fix.c line 68 function worker_2
  clatch2w_buff0_used=true;
  // file pgsql_two-fix.c line 68 function worker_2
  assert((!(clatch2w_buff1_used && clatch2w_buff0_used)));
  // file pgsql_two-fix.c line 68 function worker_2
  clatch2r_buff1_thd0=clatch2r_buff0_thd0;
  // file pgsql_two-fix.c line 68 function worker_2
  clatch2r_buff1_thd1=clatch2r_buff0_thd1;
  // file pgsql_two-fix.c line 68 function worker_2
  clatch2r_buff1_thd2=clatch2r_buff0_thd2;
  // file pgsql_two-fix.c line 68 function worker_2
  clatch2r_buff0_thd2=true;
  // file pgsql_two-fix.c line 68 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 70 function worker_2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 70 function worker_2
  weakchoice0=nondet_bool();
  // file pgsql_two-fix.c line 70 function worker_2
  weakchoice2=nondet_bool();
  // file pgsql_two-fix.c line 70 function worker_2
  clatch2flush_delayed=weakchoice2;
  // file pgsql_two-fix.c line 70 function worker_2
  clatch2mem_tmp=latch2;
  // file pgsql_two-fix.c line 70 function worker_2
  latch2=(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? latch2:((clatch2w_buff0_used && clatch2r_buff0_thd2)? clatch2w_buff0:clatch2w_buff1));
  // file pgsql_two-fix.c line 70 function worker_2
  clatch2w_buff0=(weakchoice2? clatch2w_buff0:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2w_buff0:((clatch2w_buff0_used && clatch2r_buff0_thd2)? clatch2w_buff0:clatch2w_buff0)));
  // file pgsql_two-fix.c line 70 function worker_2
  clatch2w_buff1=(weakchoice2? clatch2w_buff1:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2w_buff1:((clatch2w_buff0_used && clatch2r_buff0_thd2)? clatch2w_buff1:clatch2w_buff1)));
  // file pgsql_two-fix.c line 70 function worker_2
  clatch2w_buff0_used=(weakchoice2? clatch2w_buff0_used:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2w_buff0_used:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:clatch2w_buff0_used)));
  // file pgsql_two-fix.c line 70 function worker_2
  clatch2w_buff1_used=(weakchoice2? clatch2w_buff1_used:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2w_buff1_used:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:false)));
  // file pgsql_two-fix.c line 70 function worker_2
  clatch2r_buff0_thd2=(weakchoice2? clatch2r_buff0_thd2:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2r_buff0_thd2:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:clatch2r_buff0_thd2)));
  // file pgsql_two-fix.c line 70 function worker_2
  clatch2r_buff1_thd2=(weakchoice2? clatch2r_buff1_thd2:(((!clatch2w_buff0_used) || (((!clatch2r_buff0_thd2) && (!clatch2w_buff1_used)) || ((!clatch2r_buff0_thd2) && (!clatch2r_buff1_thd2))))? clatch2r_buff1_thd2:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:false)));
  // file pgsql_two-fix.c line 70 function worker_2
  __unbuffered_tmp2=(_Bool)((((int) latch2) ^= ((int) latch2)));
  // file pgsql_two-fix.c line 70 function worker_2
  latch2=(clatch2flush_delayed? clatch2mem_tmp:latch2);
  // file pgsql_two-fix.c line 70 function worker_2
  clatch2flush_delayed=false;
  // file pgsql_two-fix.c line 70 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 71 function worker_2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 71 function worker_2
  tmp_guard5=(!(_Bool)((((int) flag2) |= ((int) __unbuffered_tmp2))));
  // file pgsql_two-fix.c line 71 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 71 function worker_2
  if( tmp_guard5 ) goto L3;
  // file pgsql_two-fix.c line 73 function worker_2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 73 function worker_2
  flag2=(_Bool)(0);
  // file pgsql_two-fix.c line 73 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 74 function worker_2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 74 function worker_2
  flag1=(_Bool)(1);
  // file pgsql_two-fix.c line 74 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 75 function worker_2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 75 function worker_2
  flag1=((cflag1w_buff0_used && cflag1r_buff0_thd2)? cflag1w_buff0:((cflag1w_buff1_used && cflag1r_buff1_thd2)? cflag1w_buff1:flag1));
  // file pgsql_two-fix.c line 75 function worker_2
  cflag1w_buff0_used=((cflag1w_buff0_used && cflag1r_buff0_thd2)? false:cflag1w_buff0_used);
  // file pgsql_two-fix.c line 75 function worker_2
  cflag1w_buff1_used=(((cflag1w_buff0_used && cflag1r_buff0_thd2) || (cflag1w_buff1_used && cflag1r_buff1_thd2))? false:cflag1w_buff1_used);
  // file pgsql_two-fix.c line 75 function worker_2
  cflag1r_buff0_thd2=((cflag1w_buff0_used && cflag1r_buff0_thd2)? false:cflag1r_buff0_thd2);
  // file pgsql_two-fix.c line 75 function worker_2
  cflag1r_buff1_thd2=(((cflag1w_buff0_used && cflag1r_buff0_thd2) || (cflag1w_buff1_used && cflag1r_buff1_thd2))? false:cflag1r_buff1_thd2);
  // file pgsql_two-fix.c line 75 function worker_2
  latch2=((clatch2w_buff0_used && clatch2r_buff0_thd2)? clatch2w_buff0:((clatch2w_buff1_used && clatch2r_buff1_thd2)? clatch2w_buff1:latch2));
  // file pgsql_two-fix.c line 75 function worker_2
  clatch2w_buff0_used=((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:clatch2w_buff0_used);
  // file pgsql_two-fix.c line 75 function worker_2
  clatch2w_buff1_used=(((clatch2w_buff0_used && clatch2r_buff0_thd2) || (clatch2w_buff1_used && clatch2r_buff1_thd2))? false:clatch2w_buff1_used);
  // file pgsql_two-fix.c line 75 function worker_2
  clatch2r_buff0_thd2=((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:clatch2r_buff0_thd2);
  // file pgsql_two-fix.c line 75 function worker_2
  clatch2r_buff1_thd2=(((clatch2w_buff0_used && clatch2r_buff0_thd2) || (clatch2w_buff1_used && clatch2r_buff1_thd2))? false:clatch2r_buff1_thd2);
  // file pgsql_two-fix.c line 75 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 76 function worker_2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two-fix.c line 76 function worker_2
  latch1=(_Bool)(1);
  // file pgsql_two-fix.c line 76 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two-fix.c line 64 function worker_2
L3:
  goto L1;
  // file pgsql_two-fix.c line 81 function worker_2
  return nondet_ptr();
  // file pgsql_two-fix.c line 81 function worker_2
}

// c::main
// file pgsql_two-fix.c line 94
int _main(void)
{
  pthread_t __pt0;
  pthread_t __pt1;
  // file pgsql_two-fix.c line 98 function main
  // START_THREAD
  pthread_create(&__pt0, 0, worker_1, 0);
  // file pgsql_two-fix.c line 99 function main
L1:
  // START_THREAD
  pthread_create(&__pt1, 0, worker_2, 0);
  // file pgsql_two-fix.c line 106 function main
L2:
  return 0;
  // file pgsql_two-fix.c line 107 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 pgsql_two-fix.c line 6
  latch1=(_Bool)(1);
  // file pgsql_two-fix.c line 7
  flag1=(_Bool)(1);
  // file pgsql_two-fix.c line 8
  latch2=false;
  // file pgsql_two-fix.c line 8
  flag2=false;
  // file pgsql_two-fix.c line 14
  __unbuffered_tmp2=false;
}