630 void (*__parent) (void),
631 void (*__child) (void)) __attribute__ ((__nothrow__ , __leaf__));
632
633int flag1 = 0, flag2 = 0;
634int turn;
635int x;
636void *thr1() {
637 flag1 = 1;
638 while (flag2 >= 1) {
639 if (turn != 0) {
640 flag1 = 0;
641 while (turn != 0) {};
642 flag1 = 1;
643 }
644 }
645 x = 0;
646 if (!(x<=0)) ERROR: goto ERROR;;
647 turn = 1;
648 flag1 = 0;
649}
650void *thr2() {
651 flag2 = 1;
652 while (flag1 >= 1) {
653 if (turn != 1) {
654 flag2 = 0;
655 while (turn != 1) {};
656 flag2 = 1;
657 }
658 }
659 x = 1;
660 if (!(x>=1)) ERROR: goto ERROR;;
661 turn = 1;
662 flag2 = 0;
663}
664int main() {
665 pthread_t t1, t2;
666 __VERIFIER_assume(0<=turn && turn<=1);
667 pthread_create(&t1, 0, thr1, 0);
668 pthread_create(&t2, 0, thr2, 0);
669 pthread_join(t1, 0);
670 pthread_join(t2, 0);