630 List p = a;
631 while (__VERIFIER_nondet_int()) {
632 if (flag) {
633 p->h = 1;
634 flag = 0;
635 } else {
636 p->h = 2;
637 flag = 1;
638 }
639 t = (List) malloc(sizeof(struct node));
640 if (t == 0) exit(1);
641 p->n = t;
642 p = p->n;
643 }
644 p->h = 3;
645 p = a;
646 flag = 1;
647 while (p->h != 3) {
648 if (flag) {
649 flag = 0;
650 if (p->h != 1)
651 goto ERROR;
652 } else {
653 flag = 1;
654 if (p->h != 2)
655 goto ERROR;
656 }
657 p = p->n;
658 }
659 return 0;
660 ERROR:
661 printf("Alternation violation found.\n");
662 return 1;
663}