volatile _Bool isIdling = 0;
volatile _Bool hasWork = 0;
volatile int __unbuffered_condVariable = 0;

#define obtain_lock(c) \
{ \
  __CPROVER_atomic_begin(); \
  __CPROVER_assume(c==0 || c==2); \
  ++c; \
  __CPROVER_atomic_end(); \
}
#define release_lock(c) c=0

#define Wait(c) \
{ \
  __CPROVER_atomic_begin(); \
  __CPROVER_assume(c==1); \
  c=2; \
  __CPROVER_atomic_end(); \
  __CPROVER_assume(c==4); \
  __CPROVER_assume(c==0); \
  c=1; \
}
#define Pulse(c) \
{ \
  __CPROVER_assume(c==2); \
  c=4; \
}

// Consumer
void * BlockOnIdle(void * arg)
{
  obtain_lock(__unbuffered_condVariable);
  isIdling = 1;
  if(!hasWork)
    Wait(__unbuffered_condVariable);
  isIdling = 0;
  release_lock(__unbuffered_condVariable);
}

_Bool __unbuffered_prod_done=0;

// Producer
void * NotifyPotentialWork(void * arg)
{
  hasWork = 1;
  if(isIdling)
  {
    obtain_lock(__unbuffered_condVariable);
    Pulse(__unbuffered_condVariable);
    release_lock(__unbuffered_condVariable);
  }
  __unbuffered_prod_done=1;
}

int main()
{
__CPROVER_ASYNC_1: BlockOnIdle(0);
__CPROVER_ASYNC_2: NotifyPotentialWork(0);
assert(!__unbuffered_prod_done || __unbuffered_condVariable!=2);
}