_Bool nondet_bool();
_Bool LOCK = 0;

_Bool lock()
{
  if(nondet_bool())
  {
    assert(!LOCK);
    LOCK = 1;
    return 1;
  }

  return 0;
}

void unlock()
{
  assert(LOCK);
  LOCK = 0;
}

int main()
{
  unsigned got_lock = 0;
  int times;

  while(times > 0)
  {
    if(lock())
    {
      got_lock++;
      /* critical section */
    }

    if(got_lock != 0)
      unlock();

    got_lock--;
    times--;
  }
}