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

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

// c::main
// file pgsql_two.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;

// weak::choice1
// 
_Bool weakchoice1;

// 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::flag2$w_buff0
// 
_Bool cflag2w_buff0;

// c::flag2$w_buff1
// 
_Bool cflag2w_buff1;

// c::flag2$w_buff0_used
// 
_Bool cflag2w_buff0_used;

// c::flag2$w_buff1_used
// 
_Bool cflag2w_buff1_used;

// c::flag2$mem_tmp
// 
_Bool cflag2mem_tmp;

// c::flag2$flush_delayed
// 
_Bool cflag2flush_delayed;

// c::flag2$read_delayed
// 
_Bool cflag2read_delayed;

// c::flag2$read_delayed_var
// 
_Bool * cflag2read_delayed_var;

// c::flag2$r_buff0_thd0
// 
_Bool cflag2r_buff0_thd0;

// c::flag2$r_buff1_thd0
// 
_Bool cflag2r_buff1_thd0;

// c::flag2$r_buff0_thd1
// 
_Bool cflag2r_buff0_thd1;

// c::flag2$r_buff1_thd1
// 
_Bool cflag2r_buff1_thd1;

// c::flag2$r_buff0_thd2
// 
_Bool cflag2r_buff0_thd2;

// c::flag2$r_buff1_thd2
// 
_Bool cflag2r_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::worker_2$tmp_guard2$w_buff0
// 
_Bool cworker_2tmp_guard2w_buff0;

// c::worker_2$tmp_guard2$w_buff1
// 
_Bool cworker_2tmp_guard2w_buff1;

// c::worker_2$tmp_guard2$w_buff0_used
// 
_Bool cworker_2tmp_guard2w_buff0_used;

// c::worker_2$tmp_guard2$w_buff1_used
// 
_Bool cworker_2tmp_guard2w_buff1_used;

// c::worker_2$tmp_guard2$mem_tmp
// 
_Bool cworker_2tmp_guard2mem_tmp;

// c::worker_2$tmp_guard2$flush_delayed
// 
_Bool cworker_2tmp_guard2flush_delayed;

// c::worker_2$tmp_guard2$read_delayed
// 
_Bool cworker_2tmp_guard2read_delayed;

// c::worker_2$tmp_guard2$read_delayed_var
// 
_Bool * cworker_2tmp_guard2read_delayed_var;

// c::worker_2$tmp_guard2$r_buff0_thd0
// 
_Bool cworker_2tmp_guard2r_buff0_thd0;

// c::worker_2$tmp_guard2$r_buff1_thd0
// 
_Bool cworker_2tmp_guard2r_buff1_thd0;

// c::worker_2$tmp_guard2$r_buff0_thd1
// 
_Bool cworker_2tmp_guard2r_buff0_thd1;

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

// c::worker_2$tmp_guard2$r_buff1_thd1
// 
_Bool cworker_2tmp_guard2r_buff1_thd1;

// c::worker_2$tmp_guard2$r_buff0_thd2
// 
_Bool cworker_2tmp_guard2r_buff0_thd2;

// c::worker_2$tmp_guard2$r_buff1_thd2
// 
_Bool cworker_2tmp_guard2r_buff1_thd2;

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

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

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

// c::__unbuffered_tmp2
// file pgsql_two.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;
  cflag2w_buff0_used=false;
  cflag2w_buff1_used=false;
  cflag2flush_delayed=false;
  cflag2read_delayed=false;
  cflag2read_delayed_var=0;
  cflag2r_buff0_thd0=false;
  cflag2r_buff0_thd1=false;
  cflag2r_buff0_thd2=false;
  cflag2r_buff1_thd0=false;
  cflag2r_buff1_thd1=false;
  cflag2r_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;
  cworker_2tmp_guard2w_buff0_used=false;
  cworker_2tmp_guard2w_buff1_used=false;
  cworker_2tmp_guard2flush_delayed=false;
  cworker_2tmp_guard2read_delayed=false;
  cworker_2tmp_guard2read_delayed_var=0;
  cworker_2tmp_guard2r_buff0_thd0=false;
  cworker_2tmp_guard2r_buff0_thd1=false;
  cworker_2tmp_guard2r_buff0_thd2=false;
  cworker_2tmp_guard2r_buff1_thd0=false;
  cworker_2tmp_guard2r_buff1_thd1=false;
  cworker_2tmp_guard2r_buff1_thd2=false;
  __CPROVER_initialize();
  _main();
}

// c::worker_1
// file pgsql_two.c line 42
void * worker_1(void * arg)
{
  // file pgsql_two.c line 47 function worker_1
L1:
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two.c line 47 function worker_1
  weakchoice0=nondet_bool();
  // file pgsql_two.c line 47 function worker_1
  weakchoice2=nondet_bool();
  // file pgsql_two.c line 47 function worker_1
  clatch1flush_delayed=weakchoice2;
  // file pgsql_two.c line 47 function worker_1
  clatch1mem_tmp=latch1;
  // file pgsql_two.c line 47 function worker_1
  weakchoice1=nondet_bool();
  // file pgsql_two.c line 47 function worker_1
  latch1=((!clatch1w_buff0_used)? latch1:((clatch1w_buff0_used && clatch1r_buff0_thd1)? clatch1w_buff0:(((clatch1w_buff0_used && (!clatch1r_buff1_thd1)) && (clatch1w_buff1_used && (!clatch1r_buff0_thd1)))? (weakchoice0? latch1:(weakchoice1? clatch1w_buff0:clatch1w_buff1)):(((clatch1w_buff0_used && clatch1r_buff1_thd1) && (clatch1w_buff1_used && (!clatch1r_buff0_thd1)))? (weakchoice0? clatch1w_buff1:clatch1w_buff0):(weakchoice0? clatch1w_buff0:latch1)))));
  // file pgsql_two.c line 47 function worker_1
  clatch1w_buff0=(weakchoice2? clatch1w_buff0:((!clatch1w_buff0_used)? clatch1w_buff0:((clatch1w_buff0_used && clatch1r_buff0_thd1)? clatch1w_buff0:(((clatch1w_buff0_used && (!clatch1r_buff1_thd1)) && (clatch1w_buff1_used && (!clatch1r_buff0_thd1)))? clatch1w_buff0:(((clatch1w_buff0_used && clatch1r_buff1_thd1) && (clatch1w_buff1_used && (!clatch1r_buff0_thd1)))? clatch1w_buff0:clatch1w_buff0)))));
  // file pgsql_two.c line 47 function worker_1
  clatch1w_buff1=(weakchoice2? clatch1w_buff1:((!clatch1w_buff0_used)? clatch1w_buff1:((clatch1w_buff0_used && clatch1r_buff0_thd1)? clatch1w_buff1:(((clatch1w_buff0_used && (!clatch1r_buff1_thd1)) && (clatch1w_buff1_used && (!clatch1r_buff0_thd1)))? clatch1w_buff1:(((clatch1w_buff0_used && clatch1r_buff1_thd1) && (clatch1w_buff1_used && (!clatch1r_buff0_thd1)))? clatch1w_buff1:clatch1w_buff1)))));
  // file pgsql_two.c line 47 function worker_1
  clatch1w_buff0_used=(weakchoice2? clatch1w_buff0_used:((!clatch1w_buff0_used)? clatch1w_buff0_used:((clatch1w_buff0_used && clatch1r_buff0_thd1)? false:(((clatch1w_buff0_used && (!clatch1r_buff1_thd1)) && (clatch1w_buff1_used && (!clatch1r_buff0_thd1)))? (weakchoice0 || (!weakchoice1)):(((clatch1w_buff0_used && clatch1r_buff1_thd1) && (clatch1w_buff1_used && (!clatch1r_buff0_thd1)))? weakchoice0:weakchoice0)))));
  // file pgsql_two.c line 47 function worker_1
  clatch1w_buff1_used=(weakchoice2? clatch1w_buff1_used:((!clatch1w_buff0_used)? clatch1w_buff1_used:((clatch1w_buff0_used && clatch1r_buff0_thd1)? false:(((clatch1w_buff0_used && (!clatch1r_buff1_thd1)) && (clatch1w_buff1_used && (!clatch1r_buff0_thd1)))? weakchoice0:(((clatch1w_buff0_used && clatch1r_buff1_thd1) && (clatch1w_buff1_used && (!clatch1r_buff0_thd1)))? false:false)))));
  // file pgsql_two.c line 47 function worker_1
  clatch1r_buff0_thd1=(weakchoice2? clatch1r_buff0_thd1:((!clatch1w_buff0_used)? clatch1r_buff0_thd1:((clatch1w_buff0_used && clatch1r_buff0_thd1)? false:(((clatch1w_buff0_used && (!clatch1r_buff1_thd1)) && (clatch1w_buff1_used && (!clatch1r_buff0_thd1)))? clatch1r_buff0_thd1:(((clatch1w_buff0_used && clatch1r_buff1_thd1) && (clatch1w_buff1_used && (!clatch1r_buff0_thd1)))? false:false)))));
  // file pgsql_two.c line 47 function worker_1
  clatch1r_buff1_thd1=(weakchoice2? clatch1r_buff1_thd1:((!clatch1w_buff0_used)? clatch1r_buff1_thd1:((clatch1w_buff0_used && clatch1r_buff0_thd1)? false:(((clatch1w_buff0_used && (!clatch1r_buff1_thd1)) && (clatch1w_buff1_used && (!clatch1r_buff0_thd1)))? (weakchoice0? clatch1r_buff1_thd1:false):(((clatch1w_buff0_used && clatch1r_buff1_thd1) && (clatch1w_buff1_used && (!clatch1r_buff0_thd1)))? false:false)))));
  // file pgsql_two.c line 47 function worker_1
  cworker_1tmp_guard0read_delayed=true;
  // file pgsql_two.c line 47 function worker_1
  cworker_1tmp_guard0read_delayed_var=(&latch1);
  // file pgsql_two.c line 47 function worker_1
  tmp_guard=(!(!latch1));
  // file pgsql_two.c line 47 function worker_1
  latch1=(clatch1flush_delayed? clatch1mem_tmp:latch1);
  // file pgsql_two.c line 47 function worker_1
  clatch1flush_delayed=false;
  // file pgsql_two.c line 47 function worker_1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two.c line 47 function worker_1
  if( tmp_guard ) goto L2;
  // file pgsql_two.c line 47 function worker_1
  goto L1;
  // file pgsql_two.c line 48 function worker_1
L2:
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two.c line 48 function worker_1
  weakchoice0=nondet_bool();
  // file pgsql_two.c line 48 function worker_1
  weakchoice2=nondet_bool();
  // file pgsql_two.c line 48 function worker_1
  clatch1flush_delayed=weakchoice2;
  // file pgsql_two.c line 48 function worker_1
  clatch1mem_tmp=latch1;
  // file pgsql_two.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.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.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.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.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.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.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.c line 48 function worker_1
  weakchoice0=nondet_bool();
  // file pgsql_two.c line 48 function worker_1
  weakchoice2=nondet_bool();
  // file pgsql_two.c line 48 function worker_1
  cflag1flush_delayed=weakchoice2;
  // file pgsql_two.c line 48 function worker_1
  cflag1mem_tmp=flag1;
  // file pgsql_two.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.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.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.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.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.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.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.c line 48 function worker_1
  tmp_guard1=((!latch1) || flag1);
  // file pgsql_two.c line 48 function worker_1
  latch1=(clatch1flush_delayed? clatch1mem_tmp:latch1);
  // file pgsql_two.c line 48 function worker_1
  clatch1flush_delayed=false;
  // file pgsql_two.c line 48 function worker_1
  flag1=(cflag1flush_delayed? cflag1mem_tmp:flag1);
  // file pgsql_two.c line 48 function worker_1
  cflag1flush_delayed=false;
  // file pgsql_two.c line 48 function worker_1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two.c line 48 function worker_1
  assert(tmp_guard1);
  // file pgsql_two.c line 49 function worker_1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two.c line 49 function worker_1
  clatch1w_buff1=clatch1w_buff0;
  // file pgsql_two.c line 49 function worker_1
  clatch1w_buff0=(_Bool)(0);
  // file pgsql_two.c line 49 function worker_1
  clatch1w_buff1_used=clatch1w_buff0_used;
  // file pgsql_two.c line 49 function worker_1
  clatch1w_buff0_used=true;
  // file pgsql_two.c line 49 function worker_1
  assert((!(clatch1w_buff1_used && clatch1w_buff0_used)));
  // file pgsql_two.c line 49 function worker_1
  clatch1r_buff1_thd0=clatch1r_buff0_thd0;
  // file pgsql_two.c line 49 function worker_1
  clatch1r_buff1_thd1=clatch1r_buff0_thd1;
  // file pgsql_two.c line 49 function worker_1
  clatch1r_buff1_thd2=clatch1r_buff0_thd2;
  // file pgsql_two.c line 49 function worker_1
  clatch1r_buff0_thd1=true;
  // file pgsql_two.c line 49 function worker_1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two.c line 50 function worker_1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two.c line 50 function worker_1
  weakchoice0=nondet_bool();
  // file pgsql_two.c line 50 function worker_1
  weakchoice2=nondet_bool();
  // file pgsql_two.c line 50 function worker_1
  cflag1flush_delayed=weakchoice2;
  // file pgsql_two.c line 50 function worker_1
  cflag1mem_tmp=flag1;
  // file pgsql_two.c line 50 function worker_1
  weakchoice1=nondet_bool();
  // file pgsql_two.c line 50 function worker_1
  flag1=((!cflag1w_buff0_used)? flag1:((cflag1w_buff0_used && cflag1r_buff0_thd1)? cflag1w_buff0:(((cflag1w_buff0_used && (!cflag1r_buff1_thd1)) && (cflag1w_buff1_used && (!cflag1r_buff0_thd1)))? (weakchoice0? flag1:(weakchoice1? cflag1w_buff0:cflag1w_buff1)):(((cflag1w_buff0_used && cflag1r_buff1_thd1) && (cflag1w_buff1_used && (!cflag1r_buff0_thd1)))? (weakchoice0? cflag1w_buff1:cflag1w_buff0):(weakchoice0? cflag1w_buff0:flag1)))));
  // file pgsql_two.c line 50 function worker_1
  cflag1w_buff0=(weakchoice2? cflag1w_buff0:((!cflag1w_buff0_used)? cflag1w_buff0:((cflag1w_buff0_used && cflag1r_buff0_thd1)? cflag1w_buff0:(((cflag1w_buff0_used && (!cflag1r_buff1_thd1)) && (cflag1w_buff1_used && (!cflag1r_buff0_thd1)))? cflag1w_buff0:(((cflag1w_buff0_used && cflag1r_buff1_thd1) && (cflag1w_buff1_used && (!cflag1r_buff0_thd1)))? cflag1w_buff0:cflag1w_buff0)))));
  // file pgsql_two.c line 50 function worker_1
  cflag1w_buff1=(weakchoice2? cflag1w_buff1:((!cflag1w_buff0_used)? cflag1w_buff1:((cflag1w_buff0_used && cflag1r_buff0_thd1)? cflag1w_buff1:(((cflag1w_buff0_used && (!cflag1r_buff1_thd1)) && (cflag1w_buff1_used && (!cflag1r_buff0_thd1)))? cflag1w_buff1:(((cflag1w_buff0_used && cflag1r_buff1_thd1) && (cflag1w_buff1_used && (!cflag1r_buff0_thd1)))? cflag1w_buff1:cflag1w_buff1)))));
  // file pgsql_two.c line 50 function worker_1
  cflag1w_buff0_used=(weakchoice2? cflag1w_buff0_used:((!cflag1w_buff0_used)? cflag1w_buff0_used:((cflag1w_buff0_used && cflag1r_buff0_thd1)? false:(((cflag1w_buff0_used && (!cflag1r_buff1_thd1)) && (cflag1w_buff1_used && (!cflag1r_buff0_thd1)))? (weakchoice0 || (!weakchoice1)):(((cflag1w_buff0_used && cflag1r_buff1_thd1) && (cflag1w_buff1_used && (!cflag1r_buff0_thd1)))? weakchoice0:weakchoice0)))));
  // file pgsql_two.c line 50 function worker_1
  cflag1w_buff1_used=(weakchoice2? cflag1w_buff1_used:((!cflag1w_buff0_used)? cflag1w_buff1_used:((cflag1w_buff0_used && cflag1r_buff0_thd1)? false:(((cflag1w_buff0_used && (!cflag1r_buff1_thd1)) && (cflag1w_buff1_used && (!cflag1r_buff0_thd1)))? weakchoice0:(((cflag1w_buff0_used && cflag1r_buff1_thd1) && (cflag1w_buff1_used && (!cflag1r_buff0_thd1)))? false:false)))));
  // file pgsql_two.c line 50 function worker_1
  cflag1r_buff0_thd1=(weakchoice2? cflag1r_buff0_thd1:((!cflag1w_buff0_used)? cflag1r_buff0_thd1:((cflag1w_buff0_used && cflag1r_buff0_thd1)? false:(((cflag1w_buff0_used && (!cflag1r_buff1_thd1)) && (cflag1w_buff1_used && (!cflag1r_buff0_thd1)))? cflag1r_buff0_thd1:(((cflag1w_buff0_used && cflag1r_buff1_thd1) && (cflag1w_buff1_used && (!cflag1r_buff0_thd1)))? false:false)))));
  // file pgsql_two.c line 50 function worker_1
  cflag1r_buff1_thd1=(weakchoice2? cflag1r_buff1_thd1:((!cflag1w_buff0_used)? cflag1r_buff1_thd1:((cflag1w_buff0_used && cflag1r_buff0_thd1)? false:(((cflag1w_buff0_used && (!cflag1r_buff1_thd1)) && (cflag1w_buff1_used && (!cflag1r_buff0_thd1)))? (weakchoice0? cflag1r_buff1_thd1:false):(((cflag1w_buff0_used && cflag1r_buff1_thd1) && (cflag1w_buff1_used && (!cflag1r_buff0_thd1)))? false:false)))));
  // file pgsql_two.c line 50 function worker_1
  cworker_1tmp_guard2read_delayed=true;
  // file pgsql_two.c line 50 function worker_1
  cworker_1tmp_guard2read_delayed_var=(&flag1);
  // file pgsql_two.c line 50 function worker_1
  tmp_guard2=(!flag1);
  // file pgsql_two.c line 50 function worker_1
  flag1=(cflag1flush_delayed? cflag1mem_tmp:flag1);
  // file pgsql_two.c line 50 function worker_1
  cflag1flush_delayed=false;
  // file pgsql_two.c line 50 function worker_1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two.c line 50 function worker_1
  if( tmp_guard2 ) goto L3;
  // file pgsql_two.c line 52 function worker_1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two.c line 52 function worker_1
  cflag1w_buff1=cflag1w_buff0;
  // file pgsql_two.c line 52 function worker_1
  cflag1w_buff0=(_Bool)(0);
  // file pgsql_two.c line 52 function worker_1
  cflag1w_buff1_used=cflag1w_buff0_used;
  // file pgsql_two.c line 52 function worker_1
  cflag1w_buff0_used=true;
  // file pgsql_two.c line 52 function worker_1
  assert((!(cflag1w_buff1_used && cflag1w_buff0_used)));
  // file pgsql_two.c line 52 function worker_1
  cflag1r_buff1_thd0=cflag1r_buff0_thd0;
  // file pgsql_two.c line 52 function worker_1
  cflag1r_buff1_thd1=cflag1r_buff0_thd1;
  // file pgsql_two.c line 52 function worker_1
  cflag1r_buff1_thd2=cflag1r_buff0_thd2;
  // file pgsql_two.c line 52 function worker_1
  cflag1r_buff0_thd1=true;
  // file pgsql_two.c line 52 function worker_1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two.c line 53 function worker_1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two.c line 53 function worker_1
  cflag2w_buff1=cflag2w_buff0;
  // file pgsql_two.c line 53 function worker_1
  cflag2w_buff0=(_Bool)(1);
  // file pgsql_two.c line 53 function worker_1
  cflag2w_buff1_used=cflag2w_buff0_used;
  // file pgsql_two.c line 53 function worker_1
  cflag2w_buff0_used=true;
  // file pgsql_two.c line 53 function worker_1
  assert((!(cflag2w_buff1_used && cflag2w_buff0_used)));
  // file pgsql_two.c line 53 function worker_1
  cflag2r_buff1_thd0=cflag2r_buff0_thd0;
  // file pgsql_two.c line 53 function worker_1
  cflag2r_buff1_thd1=cflag2r_buff0_thd1;
  // file pgsql_two.c line 53 function worker_1
  cflag2r_buff1_thd2=cflag2r_buff0_thd2;
  // file pgsql_two.c line 53 function worker_1
  cflag2r_buff0_thd1=true;
  // file pgsql_two.c line 53 function worker_1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two.c line 54 function worker_1
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two.c line 54 function worker_1
  clatch2w_buff1=clatch2w_buff0;
  // file pgsql_two.c line 54 function worker_1
  clatch2w_buff0=(_Bool)(1);
  // file pgsql_two.c line 54 function worker_1
  clatch2w_buff1_used=clatch2w_buff0_used;
  // file pgsql_two.c line 54 function worker_1
  clatch2w_buff0_used=true;
  // file pgsql_two.c line 54 function worker_1
  assert((!(clatch2w_buff1_used && clatch2w_buff0_used)));
  // file pgsql_two.c line 54 function worker_1
  clatch2r_buff1_thd0=clatch2r_buff0_thd0;
  // file pgsql_two.c line 54 function worker_1
  clatch2r_buff1_thd1=clatch2r_buff0_thd1;
  // file pgsql_two.c line 54 function worker_1
  clatch2r_buff1_thd2=clatch2r_buff0_thd2;
  // file pgsql_two.c line 54 function worker_1
  clatch2r_buff0_thd1=true;
  // file pgsql_two.c line 54 function worker_1
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two.c line 45 function worker_1
L3:
  goto L1;
  // file pgsql_two.c line 59 function worker_1
  return nondet_ptr();
  // file pgsql_two.c line 59 function worker_1
}

// c::worker_2
// file pgsql_two.c line 61
void * worker_2(void * arg1)
{
  // file pgsql_two.c line 66 function worker_2
L1:
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two.c line 66 function worker_2
  weakchoice0=nondet_bool();
  // file pgsql_two.c line 66 function worker_2
  weakchoice2=nondet_bool();
  // file pgsql_two.c line 66 function worker_2
  clatch2flush_delayed=weakchoice2;
  // file pgsql_two.c line 66 function worker_2
  clatch2mem_tmp=latch2;
  // file pgsql_two.c line 66 function worker_2
  weakchoice1=nondet_bool();
  // file pgsql_two.c line 66 function worker_2
  latch2=((!clatch2w_buff0_used)? latch2:((clatch2w_buff0_used && clatch2r_buff0_thd2)? clatch2w_buff0:(((clatch2w_buff0_used && (!clatch2r_buff1_thd2)) && (clatch2w_buff1_used && (!clatch2r_buff0_thd2)))? (weakchoice0? latch2:(weakchoice1? clatch2w_buff0:clatch2w_buff1)):(((clatch2w_buff0_used && clatch2r_buff1_thd2) && (clatch2w_buff1_used && (!clatch2r_buff0_thd2)))? (weakchoice0? clatch2w_buff1:clatch2w_buff0):(weakchoice0? clatch2w_buff0:latch2)))));
  // file pgsql_two.c line 66 function worker_2
  clatch2w_buff0=(weakchoice2? clatch2w_buff0:((!clatch2w_buff0_used)? clatch2w_buff0:((clatch2w_buff0_used && clatch2r_buff0_thd2)? clatch2w_buff0:(((clatch2w_buff0_used && (!clatch2r_buff1_thd2)) && (clatch2w_buff1_used && (!clatch2r_buff0_thd2)))? clatch2w_buff0:(((clatch2w_buff0_used && clatch2r_buff1_thd2) && (clatch2w_buff1_used && (!clatch2r_buff0_thd2)))? clatch2w_buff0:clatch2w_buff0)))));
  // file pgsql_two.c line 66 function worker_2
  clatch2w_buff1=(weakchoice2? clatch2w_buff1:((!clatch2w_buff0_used)? clatch2w_buff1:((clatch2w_buff0_used && clatch2r_buff0_thd2)? clatch2w_buff1:(((clatch2w_buff0_used && (!clatch2r_buff1_thd2)) && (clatch2w_buff1_used && (!clatch2r_buff0_thd2)))? clatch2w_buff1:(((clatch2w_buff0_used && clatch2r_buff1_thd2) && (clatch2w_buff1_used && (!clatch2r_buff0_thd2)))? clatch2w_buff1:clatch2w_buff1)))));
  // file pgsql_two.c line 66 function worker_2
  clatch2w_buff0_used=(weakchoice2? clatch2w_buff0_used:((!clatch2w_buff0_used)? clatch2w_buff0_used:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:(((clatch2w_buff0_used && (!clatch2r_buff1_thd2)) && (clatch2w_buff1_used && (!clatch2r_buff0_thd2)))? (weakchoice0 || (!weakchoice1)):(((clatch2w_buff0_used && clatch2r_buff1_thd2) && (clatch2w_buff1_used && (!clatch2r_buff0_thd2)))? weakchoice0:weakchoice0)))));
  // file pgsql_two.c line 66 function worker_2
  clatch2w_buff1_used=(weakchoice2? clatch2w_buff1_used:((!clatch2w_buff0_used)? clatch2w_buff1_used:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:(((clatch2w_buff0_used && (!clatch2r_buff1_thd2)) && (clatch2w_buff1_used && (!clatch2r_buff0_thd2)))? weakchoice0:(((clatch2w_buff0_used && clatch2r_buff1_thd2) && (clatch2w_buff1_used && (!clatch2r_buff0_thd2)))? false:false)))));
  // file pgsql_two.c line 66 function worker_2
  clatch2r_buff0_thd2=(weakchoice2? clatch2r_buff0_thd2:((!clatch2w_buff0_used)? clatch2r_buff0_thd2:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:(((clatch2w_buff0_used && (!clatch2r_buff1_thd2)) && (clatch2w_buff1_used && (!clatch2r_buff0_thd2)))? clatch2r_buff0_thd2:(((clatch2w_buff0_used && clatch2r_buff1_thd2) && (clatch2w_buff1_used && (!clatch2r_buff0_thd2)))? false:false)))));
  // file pgsql_two.c line 66 function worker_2
  clatch2r_buff1_thd2=(weakchoice2? clatch2r_buff1_thd2:((!clatch2w_buff0_used)? clatch2r_buff1_thd2:((clatch2w_buff0_used && clatch2r_buff0_thd2)? false:(((clatch2w_buff0_used && (!clatch2r_buff1_thd2)) && (clatch2w_buff1_used && (!clatch2r_buff0_thd2)))? (weakchoice0? clatch2r_buff1_thd2:false):(((clatch2w_buff0_used && clatch2r_buff1_thd2) && (clatch2w_buff1_used && (!clatch2r_buff0_thd2)))? false:false)))));
  // file pgsql_two.c line 66 function worker_2
  cworker_2tmp_guard0read_delayed=true;
  // file pgsql_two.c line 66 function worker_2
  cworker_2tmp_guard0read_delayed_var=(&latch2);
  // file pgsql_two.c line 66 function worker_2
  tmp_guard3=(!(!latch2));
  // file pgsql_two.c line 66 function worker_2
  latch2=(clatch2flush_delayed? clatch2mem_tmp:latch2);
  // file pgsql_two.c line 66 function worker_2
  clatch2flush_delayed=false;
  // file pgsql_two.c line 66 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two.c line 66 function worker_2
  if( tmp_guard3 ) goto L2;
  // file pgsql_two.c line 66 function worker_2
  goto L1;
  // file pgsql_two.c line 67 function worker_2
L2:
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two.c line 67 function worker_2
  weakchoice0=nondet_bool();
  // file pgsql_two.c line 67 function worker_2
  weakchoice2=nondet_bool();
  // file pgsql_two.c line 67 function worker_2
  clatch2flush_delayed=weakchoice2;
  // file pgsql_two.c line 67 function worker_2
  clatch2mem_tmp=latch2;
  // file pgsql_two.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.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.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.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.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.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.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.c line 67 function worker_2
  weakchoice0=nondet_bool();
  // file pgsql_two.c line 67 function worker_2
  weakchoice2=nondet_bool();
  // file pgsql_two.c line 67 function worker_2
  cflag2flush_delayed=weakchoice2;
  // file pgsql_two.c line 67 function worker_2
  cflag2mem_tmp=flag2;
  // file pgsql_two.c line 67 function worker_2
  flag2=(((!cflag2w_buff0_used) || (((!cflag2r_buff0_thd2) && (!cflag2w_buff1_used)) || ((!cflag2r_buff0_thd2) && (!cflag2r_buff1_thd2))))? flag2:((cflag2w_buff0_used && cflag2r_buff0_thd2)? cflag2w_buff0:cflag2w_buff1));
  // file pgsql_two.c line 67 function worker_2
  cflag2w_buff0=(weakchoice2? cflag2w_buff0:(((!cflag2w_buff0_used) || (((!cflag2r_buff0_thd2) && (!cflag2w_buff1_used)) || ((!cflag2r_buff0_thd2) && (!cflag2r_buff1_thd2))))? cflag2w_buff0:((cflag2w_buff0_used && cflag2r_buff0_thd2)? cflag2w_buff0:cflag2w_buff0)));
  // file pgsql_two.c line 67 function worker_2
  cflag2w_buff1=(weakchoice2? cflag2w_buff1:(((!cflag2w_buff0_used) || (((!cflag2r_buff0_thd2) && (!cflag2w_buff1_used)) || ((!cflag2r_buff0_thd2) && (!cflag2r_buff1_thd2))))? cflag2w_buff1:((cflag2w_buff0_used && cflag2r_buff0_thd2)? cflag2w_buff1:cflag2w_buff1)));
  // file pgsql_two.c line 67 function worker_2
  cflag2w_buff0_used=(weakchoice2? cflag2w_buff0_used:(((!cflag2w_buff0_used) || (((!cflag2r_buff0_thd2) && (!cflag2w_buff1_used)) || ((!cflag2r_buff0_thd2) && (!cflag2r_buff1_thd2))))? cflag2w_buff0_used:((cflag2w_buff0_used && cflag2r_buff0_thd2)? false:cflag2w_buff0_used)));
  // file pgsql_two.c line 67 function worker_2
  cflag2w_buff1_used=(weakchoice2? cflag2w_buff1_used:(((!cflag2w_buff0_used) || (((!cflag2r_buff0_thd2) && (!cflag2w_buff1_used)) || ((!cflag2r_buff0_thd2) && (!cflag2r_buff1_thd2))))? cflag2w_buff1_used:((cflag2w_buff0_used && cflag2r_buff0_thd2)? false:false)));
  // file pgsql_two.c line 67 function worker_2
  cflag2r_buff0_thd2=(weakchoice2? cflag2r_buff0_thd2:(((!cflag2w_buff0_used) || (((!cflag2r_buff0_thd2) && (!cflag2w_buff1_used)) || ((!cflag2r_buff0_thd2) && (!cflag2r_buff1_thd2))))? cflag2r_buff0_thd2:((cflag2w_buff0_used && cflag2r_buff0_thd2)? false:cflag2r_buff0_thd2)));
  // file pgsql_two.c line 67 function worker_2
  cflag2r_buff1_thd2=(weakchoice2? cflag2r_buff1_thd2:(((!cflag2w_buff0_used) || (((!cflag2r_buff0_thd2) && (!cflag2w_buff1_used)) || ((!cflag2r_buff0_thd2) && (!cflag2r_buff1_thd2))))? cflag2r_buff1_thd2:((cflag2w_buff0_used && cflag2r_buff0_thd2)? false:false)));
  // file pgsql_two.c line 67 function worker_2
  tmp_guard4=((!latch2) || flag2);
  // file pgsql_two.c line 67 function worker_2
  latch2=(clatch2flush_delayed? clatch2mem_tmp:latch2);
  // file pgsql_two.c line 67 function worker_2
  clatch2flush_delayed=false;
  // file pgsql_two.c line 67 function worker_2
  flag2=(cflag2flush_delayed? cflag2mem_tmp:flag2);
  // file pgsql_two.c line 67 function worker_2
  cflag2flush_delayed=false;
  // file pgsql_two.c line 67 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two.c line 67 function worker_2
  assert(tmp_guard4);
  // file pgsql_two.c line 68 function worker_2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two.c line 68 function worker_2
  clatch2w_buff1=clatch2w_buff0;
  // file pgsql_two.c line 68 function worker_2
  clatch2w_buff0=(_Bool)(0);
  // file pgsql_two.c line 68 function worker_2
  clatch2w_buff1_used=clatch2w_buff0_used;
  // file pgsql_two.c line 68 function worker_2
  clatch2w_buff0_used=true;
  // file pgsql_two.c line 68 function worker_2
  assert((!(clatch2w_buff1_used && clatch2w_buff0_used)));
  // file pgsql_two.c line 68 function worker_2
  clatch2r_buff1_thd0=clatch2r_buff0_thd0;
  // file pgsql_two.c line 68 function worker_2
  clatch2r_buff1_thd1=clatch2r_buff0_thd1;
  // file pgsql_two.c line 68 function worker_2
  clatch2r_buff1_thd2=clatch2r_buff0_thd2;
  // file pgsql_two.c line 68 function worker_2
  clatch2r_buff0_thd2=true;
  // file pgsql_two.c line 68 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two.c line 71 function worker_2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two.c line 71 function worker_2
  weakchoice0=nondet_bool();
  // file pgsql_two.c line 71 function worker_2
  weakchoice2=nondet_bool();
  // file pgsql_two.c line 71 function worker_2
  cflag2flush_delayed=weakchoice2;
  // file pgsql_two.c line 71 function worker_2
  cflag2mem_tmp=flag2;
  // file pgsql_two.c line 71 function worker_2
  weakchoice1=nondet_bool();
  // file pgsql_two.c line 71 function worker_2
  flag2=((!cflag2w_buff0_used)? flag2:((cflag2w_buff0_used && cflag2r_buff0_thd2)? cflag2w_buff0:(((cflag2w_buff0_used && (!cflag2r_buff1_thd2)) && (cflag2w_buff1_used && (!cflag2r_buff0_thd2)))? (weakchoice0? flag2:(weakchoice1? cflag2w_buff0:cflag2w_buff1)):(((cflag2w_buff0_used && cflag2r_buff1_thd2) && (cflag2w_buff1_used && (!cflag2r_buff0_thd2)))? (weakchoice0? cflag2w_buff1:cflag2w_buff0):(weakchoice0? cflag2w_buff0:flag2)))));
  // file pgsql_two.c line 71 function worker_2
  cflag2w_buff0=(weakchoice2? cflag2w_buff0:((!cflag2w_buff0_used)? cflag2w_buff0:((cflag2w_buff0_used && cflag2r_buff0_thd2)? cflag2w_buff0:(((cflag2w_buff0_used && (!cflag2r_buff1_thd2)) && (cflag2w_buff1_used && (!cflag2r_buff0_thd2)))? cflag2w_buff0:(((cflag2w_buff0_used && cflag2r_buff1_thd2) && (cflag2w_buff1_used && (!cflag2r_buff0_thd2)))? cflag2w_buff0:cflag2w_buff0)))));
  // file pgsql_two.c line 71 function worker_2
  cflag2w_buff1=(weakchoice2? cflag2w_buff1:((!cflag2w_buff0_used)? cflag2w_buff1:((cflag2w_buff0_used && cflag2r_buff0_thd2)? cflag2w_buff1:(((cflag2w_buff0_used && (!cflag2r_buff1_thd2)) && (cflag2w_buff1_used && (!cflag2r_buff0_thd2)))? cflag2w_buff1:(((cflag2w_buff0_used && cflag2r_buff1_thd2) && (cflag2w_buff1_used && (!cflag2r_buff0_thd2)))? cflag2w_buff1:cflag2w_buff1)))));
  // file pgsql_two.c line 71 function worker_2
  cflag2w_buff0_used=(weakchoice2? cflag2w_buff0_used:((!cflag2w_buff0_used)? cflag2w_buff0_used:((cflag2w_buff0_used && cflag2r_buff0_thd2)? false:(((cflag2w_buff0_used && (!cflag2r_buff1_thd2)) && (cflag2w_buff1_used && (!cflag2r_buff0_thd2)))? (weakchoice0 || (!weakchoice1)):(((cflag2w_buff0_used && cflag2r_buff1_thd2) && (cflag2w_buff1_used && (!cflag2r_buff0_thd2)))? weakchoice0:weakchoice0)))));
  // file pgsql_two.c line 71 function worker_2
  cflag2w_buff1_used=(weakchoice2? cflag2w_buff1_used:((!cflag2w_buff0_used)? cflag2w_buff1_used:((cflag2w_buff0_used && cflag2r_buff0_thd2)? false:(((cflag2w_buff0_used && (!cflag2r_buff1_thd2)) && (cflag2w_buff1_used && (!cflag2r_buff0_thd2)))? weakchoice0:(((cflag2w_buff0_used && cflag2r_buff1_thd2) && (cflag2w_buff1_used && (!cflag2r_buff0_thd2)))? false:false)))));
  // file pgsql_two.c line 71 function worker_2
  cflag2r_buff0_thd2=(weakchoice2? cflag2r_buff0_thd2:((!cflag2w_buff0_used)? cflag2r_buff0_thd2:((cflag2w_buff0_used && cflag2r_buff0_thd2)? false:(((cflag2w_buff0_used && (!cflag2r_buff1_thd2)) && (cflag2w_buff1_used && (!cflag2r_buff0_thd2)))? cflag2r_buff0_thd2:(((cflag2w_buff0_used && cflag2r_buff1_thd2) && (cflag2w_buff1_used && (!cflag2r_buff0_thd2)))? false:false)))));
  // file pgsql_two.c line 71 function worker_2
  cflag2r_buff1_thd2=(weakchoice2? cflag2r_buff1_thd2:((!cflag2w_buff0_used)? cflag2r_buff1_thd2:((cflag2w_buff0_used && cflag2r_buff0_thd2)? false:(((cflag2w_buff0_used && (!cflag2r_buff1_thd2)) && (cflag2w_buff1_used && (!cflag2r_buff0_thd2)))? (weakchoice0? cflag2r_buff1_thd2:false):(((cflag2w_buff0_used && cflag2r_buff1_thd2) && (cflag2w_buff1_used && (!cflag2r_buff0_thd2)))? false:false)))));
  // file pgsql_two.c line 71 function worker_2
  cworker_2tmp_guard2read_delayed=true;
  // file pgsql_two.c line 71 function worker_2
  cworker_2tmp_guard2read_delayed_var=(&flag2);
  // file pgsql_two.c line 71 function worker_2
  tmp_guard5=(!flag2);
  // file pgsql_two.c line 71 function worker_2
  flag2=(cflag2flush_delayed? cflag2mem_tmp:flag2);
  // file pgsql_two.c line 71 function worker_2
  cflag2flush_delayed=false;
  // file pgsql_two.c line 71 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two.c line 71 function worker_2
  if( tmp_guard5 ) goto L3;
  // file pgsql_two.c line 73 function worker_2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two.c line 73 function worker_2
  cflag2w_buff1=cflag2w_buff0;
  // file pgsql_two.c line 73 function worker_2
  cflag2w_buff0=(_Bool)(0);
  // file pgsql_two.c line 73 function worker_2
  cflag2w_buff1_used=cflag2w_buff0_used;
  // file pgsql_two.c line 73 function worker_2
  cflag2w_buff0_used=true;
  // file pgsql_two.c line 73 function worker_2
  assert((!(cflag2w_buff1_used && cflag2w_buff0_used)));
  // file pgsql_two.c line 73 function worker_2
  cflag2r_buff1_thd0=cflag2r_buff0_thd0;
  // file pgsql_two.c line 73 function worker_2
  cflag2r_buff1_thd1=cflag2r_buff0_thd1;
  // file pgsql_two.c line 73 function worker_2
  cflag2r_buff1_thd2=cflag2r_buff0_thd2;
  // file pgsql_two.c line 73 function worker_2
  cflag2r_buff0_thd2=true;
  // file pgsql_two.c line 73 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two.c line 74 function worker_2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two.c line 74 function worker_2
  cflag1w_buff1=cflag1w_buff0;
  // file pgsql_two.c line 74 function worker_2
  cflag1w_buff0=(_Bool)(1);
  // file pgsql_two.c line 74 function worker_2
  cflag1w_buff1_used=cflag1w_buff0_used;
  // file pgsql_two.c line 74 function worker_2
  cflag1w_buff0_used=true;
  // file pgsql_two.c line 74 function worker_2
  assert((!(cflag1w_buff1_used && cflag1w_buff0_used)));
  // file pgsql_two.c line 74 function worker_2
  cflag1r_buff1_thd0=cflag1r_buff0_thd0;
  // file pgsql_two.c line 74 function worker_2
  cflag1r_buff1_thd1=cflag1r_buff0_thd1;
  // file pgsql_two.c line 74 function worker_2
  cflag1r_buff1_thd2=cflag1r_buff0_thd2;
  // file pgsql_two.c line 74 function worker_2
  cflag1r_buff0_thd2=true;
  // file pgsql_two.c line 74 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two.c line 76 function worker_2
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file pgsql_two.c line 76 function worker_2
  clatch1w_buff1=clatch1w_buff0;
  // file pgsql_two.c line 76 function worker_2
  clatch1w_buff0=(_Bool)(1);
  // file pgsql_two.c line 76 function worker_2
  clatch1w_buff1_used=clatch1w_buff0_used;
  // file pgsql_two.c line 76 function worker_2
  clatch1w_buff0_used=true;
  // file pgsql_two.c line 76 function worker_2
  assert((!(clatch1w_buff1_used && clatch1w_buff0_used)));
  // file pgsql_two.c line 76 function worker_2
  clatch1r_buff1_thd0=clatch1r_buff0_thd0;
  // file pgsql_two.c line 76 function worker_2
  clatch1r_buff1_thd1=clatch1r_buff0_thd1;
  // file pgsql_two.c line 76 function worker_2
  clatch1r_buff1_thd2=clatch1r_buff0_thd2;
  // file pgsql_two.c line 76 function worker_2
  clatch1r_buff0_thd2=true;
  // file pgsql_two.c line 76 function worker_2
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file pgsql_two.c line 64 function worker_2
L3:
  goto L1;
  // file pgsql_two.c line 81 function worker_2
  return nondet_ptr();
  // file pgsql_two.c line 81 function worker_2
}

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