text: extern int __VERIFIER_nondet_int();
  /* Testcase from Threader's distribution. For details see:
     http://www.model.in.tum.de/~popeea/research/threader
  
     This file is adapted from the Promela code introduced in the paper:
     Using Promela and Spin to verify parallel algorithms
     by Paul McKenney
  */
  
  int idx=0; // boolean to control which of the two elements will be used by readers
    // (idx <= 0) then ctr1 is used
    // (idx >= 1) then ctr2 is used
  int ctr1=1, ctr2=0;
  int readerprogress1=0, readerprogress2=0; // the progress is indicated by an integer:
    // 0: reader not yet started
    // 1: reader withing QRCU read-side critical section
    // 2: reader finished with QRCU read-side critical section
  
  void __VERIFIER_atomic_use1(int myidx) {
    __VERIFIER_assume(myidx <= 0 && ctr1>0);
    ctr1++;
  }
  
  void __VERIFIER_atomic_use2(int myidx) {
    __VERIFIER_assume(myidx >= 1 && ctr2>0);
    ctr2++;
  }
  
  void __VERIFIER_atomic_use_done(int myidx) {
    if (myidx <= 0) { ctr1--; }
    else { ctr2--; }
  }
  
  void __VERIFIER_atomic_take_snapshot(int *readerstart1, int *readerstart2) {
    /* Snapshot reader state. */
    *readerstart1 = readerprogress1;
    *readerstart2 = readerprogress2;
  }
  
  void __VERIFIER_atomic_check_progress1(int readerstart1) {
    /* Verify reader progress. */
    if (__VERIFIER_nondet_int()) {
      __VERIFIER_assume(readerstart1 == 1 && readerprogress1 == 1);
      assert(0);
    }
    return;
  }
  
  void __VERIFIER_atomic_check_progress2(int readerstart2) {
    if (__VERIFIER_nondet_int()) {
      __VERIFIER_assume(readerstart2 == 1 && readerprogress2 == 1);
      assert(0);
    }
    return;
  }
  
  void *qrcu_reader1() {
    int myidx;
    /* rcu_read_lock */
    while (1) {
      myidx = idx;
      if (__VERIFIER_nondet_int()) {
        __VERIFIER_atomic_use1(myidx);
        break;
      } else {
        if (__VERIFIER_nondet_int()) {
  	__VERIFIER_atomic_use2(myidx);
  	break;
        } else {}
      }
    }
    readerprogress1 = 1;
    readerprogress1 = 2;
    /* rcu_read_unlock */
    __VERIFIER_atomic_use_done(myidx);
    return 0;
  }
  
  void *qrcu_reader2() {
    int myidx;
    /* rcu_read_lock */
    while (1) {
      myidx = idx;
      if (__VERIFIER_nondet_int()) {
        __VERIFIER_atomic_use1(myidx);
        break;
      } else {
        if (__VERIFIER_nondet_int()) {
  	__VERIFIER_atomic_use2(myidx);
  	break;
        } else {}
      }
    }
    readerprogress2 = 1;
    readerprogress2 = 2;
    /* rcu_read_unlock */
    __VERIFIER_atomic_use_done(myidx);
    return 0;
  }
  
  void* qrcu_updater() {
    int i;
    int readerstart1, readerstart2;
    int sum;
    __VERIFIER_atomic_take_snapshot(&readerstart1, &readerstart2);
    sum = ctr2;
    sum = sum + ctr1;
    if (sum > 1) {
      if (idx <= 0) { ctr2++; idx = 1; ctr1--; }
      else { ctr1++; idx = 0; ctr2--; }
      if (idx <= 0) { __CPROVER_assume (ctr1 <= 0); }
      else { __CPROVER_assume (ctr2 <= 0); }
    } else {}
    __VERIFIER_atomic_check_progress1(readerstart1);
    __VERIFIER_atomic_check_progress2(readerstart2);
    return 0;
  }
  
  int main() {
  __CPROVER_ASYNC_1: qrcu_reader1();
  __CPROVER_ASYNC_1: qrcu_reader2();
  __CPROVER_ASYNC_1: qrcu_updater();
    return 0;
  }
  