633int idx=0;
634int ctr1=1, ctr2=0;
635int readerprogress1=0, readerprogress2=0;
636pthread_mutex_t mutex;
637void __VERIFIER_atomic_use1(int myidx) {
638 __VERIFIER_assume(myidx <= 0 && ctr1>0);
639 ctr1++;
640}
641void __VERIFIER_atomic_use2(int myidx) {
642 __VERIFIER_assume(myidx >= 1 && ctr2>0);
643 ctr2++;
644}
645void __VERIFIER_atomic_use_done(int myidx) {
646 if (myidx <= 0) { ctr1--; }
647 else { ctr2--; }
648}
649void __VERIFIER_atomic_take_snapshot(int readerstart1, int readerstart2) {
650 readerstart1 = readerprogress1;
651 readerstart2 = readerprogress2;
652}
653void __VERIFIER_atomic_check_progress1(int readerstart1) {
654 if (__VERIFIER_nondet_int()) {
655 __VERIFIER_assume(readerstart1 == 1 && readerprogress1 == 1);
656 if (!(0)) ERROR: goto ERROR;;
657 }
658 return;
659}
660void __VERIFIER_atomic_check_progress2(int readerstart2) {
661 if (__VERIFIER_nondet_int()) {
662 __VERIFIER_assume(readerstart2 == 1 && readerprogress2 == 1);
663 if (!(0)) ERROR: goto ERROR;;
664 }
665 return;
666}
667void *qrcu_reader1() {
668 int myidx;
669 while (1) {
670 myidx = idx;
671 if (__VERIFIER_nondet_int()) {
672 __VERIFIER_atomic_use1(myidx);
673 break;