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

// c::BlockOnIdle
// file sober-fixed.sc.c line 31
void * BlockOnIdle(void *);

// c::NotifyPotentialWork
// file sober-fixed.sc.c line 44
void * NotifyPotentialWork(void *);

// c::main
// file sober-fixed.sc.c line 56
int _main(void);

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

// c::__unbuffered_condVariable
// file sober-fixed.sc.c line 3
int __unbuffered_condVariable;

// c::__unbuffered_prod_done
// file sober-fixed.sc.c line 41
_Bool __unbuffered_prod_done;

// c::isIdling
// file sober-fixed.sc.c line 1
_Bool isIdling;

// c::hasWork
// file sober-fixed.sc.c line 2
_Bool hasWork;

// 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 sober-fixed.sc.c line 1
  isIdling=(_Bool)(0);
  // file sober-fixed.sc.c line 2
  hasWork=(_Bool)(0);
  // file sober-fixed.sc.c line 3
  __unbuffered_condVariable=0;
  // file sober-fixed.sc.c line 41
  __unbuffered_prod_done=(_Bool)(0);
}

// c::BlockOnIdle
// file sober-fixed.sc.c line 31
void * BlockOnIdle(void * arg)
{
  // file sober-fixed.sc.c line 33 function BlockOnIdle
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file sober-fixed.sc.c line 33 function BlockOnIdle
  __CPROVER_assume(((__unbuffered_condVariable==0) || (__unbuffered_condVariable==2)));
  // file sober-fixed.sc.c line 33 function BlockOnIdle
  __unbuffered_condVariable=((__unbuffered_condVariable+1));
  // file sober-fixed.sc.c line 33 function BlockOnIdle
  // file sober-fixed.sc.c line 33 function BlockOnIdle
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file sober-fixed.sc.c line 34 function BlockOnIdle
  isIdling=(_Bool)(1);
  // file sober-fixed.sc.c line 35 function BlockOnIdle
  if( (!(!hasWork)) ) goto L1;
  // file sober-fixed.sc.c line 36 function BlockOnIdle
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file sober-fixed.sc.c line 36 function BlockOnIdle
  __CPROVER_assume((__unbuffered_condVariable==1));
  // file sober-fixed.sc.c line 36 function BlockOnIdle
  __unbuffered_condVariable=2;
  // file sober-fixed.sc.c line 36 function BlockOnIdle
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file sober-fixed.sc.c line 36 function BlockOnIdle
  __CPROVER_assume((__unbuffered_condVariable==4));
  // file sober-fixed.sc.c line 36 function BlockOnIdle
  __CPROVER_assume((__unbuffered_condVariable==0));
  // file sober-fixed.sc.c line 36 function BlockOnIdle
  __unbuffered_condVariable=1;
  // file sober-fixed.sc.c line 37 function BlockOnIdle
L1:
  isIdling=(_Bool)(0);
  // file sober-fixed.sc.c line 38 function BlockOnIdle
  __unbuffered_condVariable=0;
  // file sober-fixed.sc.c line 39 function BlockOnIdle
  return nondet_ptr();
  // file sober-fixed.sc.c line 39 function BlockOnIdle
}

// c::NotifyPotentialWork
// file sober-fixed.sc.c line 44
void * NotifyPotentialWork(void * arg1)
{
  // file sober-fixed.sc.c line 46 function NotifyPotentialWork
  hasWork=(_Bool)(1);
  // file sober-fixed.sc.c line 47 function NotifyPotentialWork
  if( (!isIdling) ) goto L1;
  // file sober-fixed.sc.c line 49 function NotifyPotentialWork
  // ATOMIC_BEGIN
  __CPROVER_atomic_begin();
  // file sober-fixed.sc.c line 49 function NotifyPotentialWork
  __CPROVER_assume(((__unbuffered_condVariable==0) || (__unbuffered_condVariable==2)));
  // file sober-fixed.sc.c line 49 function NotifyPotentialWork
  __unbuffered_condVariable=((__unbuffered_condVariable+1));
  // file sober-fixed.sc.c line 49 function NotifyPotentialWork
  // file sober-fixed.sc.c line 49 function NotifyPotentialWork
  // ATOMIC_END
  __CPROVER_atomic_end();
  // file sober-fixed.sc.c line 50 function NotifyPotentialWork
  __CPROVER_assume((__unbuffered_condVariable==2));
  // file sober-fixed.sc.c line 50 function NotifyPotentialWork
  __unbuffered_condVariable=4;
  // file sober-fixed.sc.c line 51 function NotifyPotentialWork
  __unbuffered_condVariable=0;
  // file sober-fixed.sc.c line 53 function NotifyPotentialWork
L1:
  __unbuffered_prod_done=(_Bool)(1);
  // file sober-fixed.sc.c line 54 function NotifyPotentialWork
  return nondet_ptr();
  // file sober-fixed.sc.c line 54 function NotifyPotentialWork
}

// c::main
// file sober-fixed.sc.c line 56
int _main(void)
{
  pthread_t __pt0;
  pthread_t __pt1;
  // file sober-fixed.sc.c line 58 function main
  // START_THREAD
  pthread_create(&__pt0, 0, BlockOnIdle, 0);
  // file sober-fixed.sc.c line 59 function main
L1:
  // START_THREAD
  pthread_create(&__pt1, 0, NotifyPotentialWork, 0);
  // file sober-fixed.sc.c line 60 function main
L2:
  assert(((!__unbuffered_prod_done) || (__unbuffered_condVariable!=2)));
  // file sober-fixed.sc.c line 61 function main
  return nondet_int();
  // file sober-fixed.sc.c line 61 function main
}