621typedef struct node {
622 int h;
623 struct node *n;
624} *List;
625void main() {
626 int flag = __VERIFIER_nondet_int();
627 List p, a, t;
628 a = (List) malloc(sizeof(struct node));
629 if (a == 0) exit(1);
630 p = a;
631 while (__VERIFIER_nondet_int()) {
632 if (flag) {
633 p->h = 1;
634 } else {
635 p->h = 2;
636 }
637 t = (List) malloc(sizeof(struct node));
638 if (t == 0) exit(1);
639 p->n = t;
640 p = p->n;
641 }
642 p->h = 3;
643 p = a;
644 if (flag)
645 while (p->h == 1)
646 p = p->n;
647 else
648 while (p->h == 2)
649 p = p->n;
650 if (p->h != 3)
651 ERROR: goto ERROR;
652}