626extern int pthread_getcpuclockid (pthread_t __thread_id,
627 __clockid_t *__clock_id)
628 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
629extern int pthread_atfork (void (*__prepare) (void),
630 void (*__parent) (void),
631 void (*__child) (void)) __attribute__ ((__nothrow__ , __leaf__));
632
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}