// c::worker_1
// file pgsql_two-fix-lwsync.sc.c line 43
void * worker_1(void *);

// c::worker_2
// file pgsql_two-fix-lwsync.sc.c line 62
void * worker_2(void *);

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

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

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

// c::latch1
// file pgsql_two-fix-lwsync.sc.c line 7
_Bool latch1;

// c::flag1
// file pgsql_two-fix-lwsync.sc.c line 8
_Bool flag1;

// c::latch2
// file pgsql_two-fix-lwsync.sc.c line 9
_Bool latch2;

// c::flag2
// file pgsql_two-fix-lwsync.sc.c line 9
_Bool flag2;

// c::__unbuffered_tmp2
// file pgsql_two-fix-lwsync.sc.c line 15
_Bool __unbuffered_tmp2;

// main
// 
int main(void)
{
  __CPROVER_initialize();
  _main();
}

// c::worker_1
// file pgsql_two-fix-lwsync.sc.c line 43
void * worker_1(void * arg)
{
  // file pgsql_two-fix-lwsync.sc.c line 48 function worker_1
L1:
  if( (!(!latch1)) ) goto L2;
  // file pgsql_two-fix-lwsync.sc.c line 48 function worker_1
  goto L1;
  // file pgsql_two-fix-lwsync.sc.c line 49 function worker_1
L2:
  latch1=(_Bool)(0);
  // file pgsql_two-fix-lwsync.sc.c line 50 function worker_1
  assert(flag1);
  // file pgsql_two-fix-lwsync.sc.c line 51 function worker_1
  if( (!flag1) ) goto L3;
  // file pgsql_two-fix-lwsync.sc.c line 53 function worker_1
  flag1=(_Bool)(0);
  // file pgsql_two-fix-lwsync.sc.c line 54 function worker_1
  flag2=(_Bool)(1);
  // file pgsql_two-fix-lwsync.sc.c line 55 function worker_1
  latch2=(_Bool)(1);
  // file pgsql_two-fix-lwsync.sc.c line 46 function worker_1
L3:
  goto L1;
  // file pgsql_two-fix-lwsync.sc.c line 60 function worker_1
  return nondet_ptr();
  // file pgsql_two-fix-lwsync.sc.c line 60 function worker_1
}

// c::worker_2
// file pgsql_two-fix-lwsync.sc.c line 62
void * worker_2(void * arg1)
{
  // file pgsql_two-fix-lwsync.sc.c line 67 function worker_2
L1:
  if( (!(!latch2)) ) goto L2;
  // file pgsql_two-fix-lwsync.sc.c line 67 function worker_2
  goto L1;
  // file pgsql_two-fix-lwsync.sc.c line 68 function worker_2
L2:
  latch2=(_Bool)(0);
  // file pgsql_two-fix-lwsync.sc.c line 69 function worker_2
  assert(flag2);
  // file pgsql_two-fix-lwsync.sc.c line 70 function worker_2
  if( (!flag2) ) goto L3;
  // file pgsql_two-fix-lwsync.sc.c line 72 function worker_2
  flag2=(_Bool)(0);
  // file pgsql_two-fix-lwsync.sc.c line 73 function worker_2
  flag1=(_Bool)(1);
  // file pgsql_two-fix-lwsync.sc.c line 74 function worker_2
  latch1=(_Bool)(1);
  // file pgsql_two-fix-lwsync.sc.c line 65 function worker_2
L3:
  goto L1;
  // file pgsql_two-fix-lwsync.sc.c line 79 function worker_2
  return nondet_ptr();
  // file pgsql_two-fix-lwsync.sc.c line 79 function worker_2
}

// c::main
// file pgsql_two-fix-lwsync.sc.c line 92
int _main(void)
{
  pthread_t __pt0;
  pthread_t __pt1;
  // file pgsql_two-fix-lwsync.sc.c line 96 function main
  // START_THREAD
  pthread_create(&__pt0, 0, worker_1, 0);
  // file pgsql_two-fix-lwsync.sc.c line 97 function main
L1:
  // START_THREAD
  pthread_create(&__pt1, 0, worker_2, 0);
  // file pgsql_two-fix-lwsync.sc.c line 104 function main
L2:
  return 0;
  // file pgsql_two-fix-lwsync.sc.c line 105 function main
}

// c::__CPROVER_initialize
// file <built-in> line 14
void __CPROVER_initialize(void)
{
  // file pgsql_two-fix-lwsync.sc.c line 7
  latch1=(_Bool)(1);
  // file pgsql_two-fix-lwsync.sc.c line 8
  flag1=(_Bool)(1);
  // file pgsql_two-fix-lwsync.sc.c line 9
  latch2=false;
  // file pgsql_two-fix-lwsync.sc.c line 9
  flag2=false;
  // file pgsql_two-fix-lwsync.sc.c line 15
  __unbuffered_tmp2=false;
  // 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
}