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

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

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

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

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

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

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

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

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

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

// main
// 
int main(void)
{
  __CPROVER_initialize();
  _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-developer-fix.sc.c line 6
  latch1=(_Bool)(1);
  // file pgsql_two-developer-fix.sc.c line 7
  flag1=(_Bool)(1);
  // file pgsql_two-developer-fix.sc.c line 8
  latch2=false;
  // file pgsql_two-developer-fix.sc.c line 8
  flag2=false;
  // file pgsql_two-developer-fix.sc.c line 14
  __unbuffered_tmp2=false;
}

// c::worker_1
// file pgsql_two-developer-fix.sc.c line 42
void * worker_1(void * arg)
{
  // file pgsql_two-developer-fix.sc.c line 47 function worker_1
L1:
  if( (!(!latch1)) ) goto L2;
  // file pgsql_two-developer-fix.sc.c line 47 function worker_1
  goto L1;
  // file pgsql_two-developer-fix.sc.c line 48 function worker_1
L2:
  assert(((!latch1) || flag1));
  // file pgsql_two-developer-fix.sc.c line 49 function worker_1
  latch1=(_Bool)(0);
  // file pgsql_two-developer-fix.sc.c line 50 function worker_1
  if( (!flag1) ) goto L3;
  // file pgsql_two-developer-fix.sc.c line 52 function worker_1
  flag1=(_Bool)(0);
  // file pgsql_two-developer-fix.sc.c line 53 function worker_1
  flag2=(_Bool)(1);
  // file pgsql_two-developer-fix.sc.c line 54 function worker_1
  latch2=(_Bool)(1);
  // file pgsql_two-developer-fix.sc.c line 45 function worker_1
L3:
  goto L1;
  // file pgsql_two-developer-fix.sc.c line 59 function worker_1
  return nondet_ptr();
  // file pgsql_two-developer-fix.sc.c line 59 function worker_1
}

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

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