621typedef struct node {
622 int h;
623 struct node *n;
624} *List;
625int main() {
626 List a = (List) malloc(sizeof(struct node));
627 if (a == 0) exit(1);
628 List t;
629 List p = a;
630 while (__VERIFIER_nondet_int()) {
631 p->h = 1;
632 t = (List) malloc(sizeof(struct node));
633 if (t == 0) exit(1);
634 p->n = t;
635 p = p->n;
636 }
637 while (__VERIFIER_nondet_int()) {
638 p->h = 2;
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 while (p->h == 1)
647 p = p->n;
648 while (p->h == 2)
649 p = p->n;
650 if(p->h != 3)
651 ERROR: goto ERROR;
652 return 0;
653}