1extern int __VERIFIER_nondet_int();
2typedef long unsigned int size_t;
3typedef int wchar_t;
4
5union wait
6 {
7 int w_status;
8 struct
9 {
10 unsigned int __w_termsig:7;
11 unsigned int __w_coredump:1;
12 unsigned int __w_retcode:8;
13 unsigned int:16;
14 } __wait_terminated;
15 struct
16 {
17 unsigned int __w_stopval:8;
18 unsigned int __w_stopsig:8;
19 unsigned int:16;
20 } __wait_stopped;
21 };
22typedef union
23 {
24 union wait *__uptr;
25 int *__iptr;
26 } __WAIT_STATUS __attribute__ ((__transparent_union__));
27
28typedef struct
29 {
30 int quot;
31 int rem;
32 } div_t;
33typedef struct
34 {
35 long int quot;
36 long int rem;
37 } ldiv_t;
38
39
40__extension__ typedef struct
41 {
42 long long int quot;
43 long long int rem;
44 } lldiv_t;
45
46extern size_t __ctype_get_mb_cur_max (void) __attribute__ ((__nothrow__ , __leaf__)) ;
47
48extern double atof (__const char *__nptr)
49 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
50extern int atoi (__const char *__nptr)
51 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
52extern long int atol (__const char *__nptr)
53 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
54
55
56__extension__ extern long long int atoll (__const char *__nptr)
57 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
58
59
60extern double strtod (__const char *__restrict __nptr,
61 char **__restrict __endptr)
62 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
63
64
65extern float strtof (__const char *__restrict __nptr,
66 char **__restrict __endptr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
67extern long double strtold (__const char *__restrict __nptr,
68 char **__restrict __endptr)
69 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
70
71
72extern long int strtol (__const char *__restrict __nptr,
73 char **__restrict __endptr, int __base)
74 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
75extern unsigned long int strtoul (__const char *__restrict __nptr,
76 char **__restrict __endptr, int __base)
77 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
78
79__extension__
80extern long long int strtoq (__const char *__restrict __nptr,
81 char **__restrict __endptr, int __base)
82 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
83__extension__
84extern unsigned long long int strtouq (__const char *__restrict __nptr,
85 char **__restrict __endptr, int __base)
86 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
87
88__extension__
89extern long long int strtoll (__const char *__restrict __nptr,
90 char **__restrict __endptr, int __base)
91 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
92__extension__
93extern unsigned long long int strtoull (__const char *__restrict __nptr,
94 char **__restrict __endptr, int __base)
95 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
96
97extern char *l64a (long int __n) __attribute__ ((__nothrow__ , __leaf__)) ;
98extern long int a64l (__const char *__s)
99 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
100
101typedef unsigned char __u_char;
102typedef unsigned short int __u_short;
103typedef unsigned int __u_int;
104typedef unsigned long int __u_long;
105typedef signed char __int8_t;
106typedef unsigned char __uint8_t;
107typedef signed short int __int16_t;
108typedef unsigned short int __uint16_t;
109typedef signed int __int32_t;
110typedef unsigned int __uint32_t;
111typedef signed long int __int64_t;
112typedef unsigned long int __uint64_t;
113typedef long int __quad_t;
114typedef unsigned long int __u_quad_t;
115typedef unsigned long int __dev_t;
116typedef unsigned int __uid_t;
117typedef unsigned int __gid_t;
118typedef unsigned long int __ino_t;
119typedef unsigned long int __ino64_t;
120typedef unsigned int __mode_t;
121typedef unsigned long int __nlink_t;
122typedef long int __off_t;
123typedef long int __off64_t;
124typedef int __pid_t;
125typedef struct { int __val[2]; } __fsid_t;
126typedef long int __clock_t;
127typedef unsigned long int __rlim_t;
128typedef unsigned long int __rlim64_t;
129typedef unsigned int __id_t;
130typedef long int __time_t;
131typedef unsigned int __useconds_t;
132typedef long int __suseconds_t;
133typedef int __daddr_t;
134typedef long int __swblk_t;
135typedef int __key_t;
136typedef int __clockid_t;
137typedef void * __timer_t;
138typedef long int __blksize_t;
139typedef long int __blkcnt_t;
140typedef long int __blkcnt64_t;
141typedef unsigned long int __fsblkcnt_t;
142typedef unsigned long int __fsblkcnt64_t;
143typedef unsigned long int __fsfilcnt_t;
144typedef unsigned long int __fsfilcnt64_t;
145typedef long int __ssize_t;
146typedef __off64_t __loff_t;
147typedef __quad_t *__qaddr_t;
148typedef char *__caddr_t;
149typedef long int __intptr_t;
150typedef unsigned int __socklen_t;
151typedef __u_char u_char;
152typedef __u_short u_short;
153typedef __u_int u_int;
154typedef __u_long u_long;
155typedef __quad_t quad_t;
156typedef __u_quad_t u_quad_t;
157typedef __fsid_t fsid_t;
158typedef __loff_t loff_t;
159typedef __ino_t ino_t;
160typedef __dev_t dev_t;
161typedef __gid_t gid_t;
162typedef __mode_t mode_t;
163typedef __nlink_t nlink_t;
164typedef __uid_t uid_t;
165typedef __off_t off_t;
166typedef __pid_t pid_t;
167typedef __id_t id_t;
168typedef __ssize_t ssize_t;
169typedef __daddr_t daddr_t;
170typedef __caddr_t caddr_t;
171typedef __key_t key_t;
172
173typedef __clock_t clock_t;
174
175
176
177typedef __time_t time_t;
178
179
180typedef __clockid_t clockid_t;
181typedef __timer_t timer_t;
182typedef unsigned long int ulong;
183typedef unsigned short int ushort;
184typedef unsigned int uint;
185typedef int int8_t __attribute__ ((__mode__ (__QI__)));
186typedef int int16_t __attribute__ ((__mode__ (__HI__)));
187typedef int int32_t __attribute__ ((__mode__ (__SI__)));
188typedef int int64_t __attribute__ ((__mode__ (__DI__)));
189typedef unsigned int u_int8_t __attribute__ ((__mode__ (__QI__)));
190typedef unsigned int u_int16_t __attribute__ ((__mode__ (__HI__)));
191typedef unsigned int u_int32_t __attribute__ ((__mode__ (__SI__)));
192typedef unsigned int u_int64_t __attribute__ ((__mode__ (__DI__)));
193typedef int register_t __attribute__ ((__mode__ (__word__)));
194typedef int __sig_atomic_t;
195typedef struct
196 {
197 unsigned long int __val[(1024 / (8 * sizeof (unsigned long int)))];
198 } __sigset_t;
199typedef __sigset_t sigset_t;
200struct timespec
201 {
202 __time_t tv_sec;
203 long int tv_nsec;
204 };
205struct timeval
206 {
207 __time_t tv_sec;
208 __suseconds_t tv_usec;
209 };
210typedef __suseconds_t suseconds_t;
211typedef long int __fd_mask;
212typedef struct
213 {
214 __fd_mask __fds_bits[1024 / (8 * (int) sizeof (__fd_mask))];
215 } fd_set;
216typedef __fd_mask fd_mask;
217
218extern int select (int __nfds, fd_set *__restrict __readfds,
219 fd_set *__restrict __writefds,
220 fd_set *__restrict __exceptfds,
221 struct timeval *__restrict __timeout);
222extern int pselect (int __nfds, fd_set *__restrict __readfds,
223 fd_set *__restrict __writefds,
224 fd_set *__restrict __exceptfds,
225 const struct timespec *__restrict __timeout,
226 const __sigset_t *__restrict __sigmask);
227
228
229__extension__
230extern unsigned int gnu_dev_major (unsigned long long int __dev)
231 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
232__extension__
233extern unsigned int gnu_dev_minor (unsigned long long int __dev)
234 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
235__extension__
236extern unsigned long long int gnu_dev_makedev (unsigned int __major,
237 unsigned int __minor)
238 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
239
240typedef __blksize_t blksize_t;
241typedef __blkcnt_t blkcnt_t;
242typedef __fsblkcnt_t fsblkcnt_t;
243
244
245typedef __fsfilcnt_t fsfilcnt_t;
246typedef unsigned long int pthread_t;
247typedef union
248{
249 char __size[56];
250 long int __align;
251} pthread_attr_t;
252typedef struct __pthread_internal_list
253{
254 struct __pthread_internal_list *__prev;
255 struct __pthread_internal_list *__next;
256} __pthread_list_t;
257typedef union
258{
259 struct __pthread_mutex_s
260 {
261 int __lock;
262 unsigned int __count;
263 int __owner;
264 unsigned int __nusers;
265 int __kind;
266 int __spins;
267 __pthread_list_t __list;
268 } __data;
269 char __size[40];
270 long int __align;
271} pthread_mutex_t;
272typedef union
273{
274 char __size[4];
275 int __align;
276} pthread_mutexattr_t;
277typedef union
278{
279 struct
280 {
281 int __lock;
282 unsigned int __futex;
283 __extension__ unsigned long long int __total_seq;
284 __extension__ unsigned long long int __wakeup_seq;
285 __extension__ unsigned long long int __woken_seq;
286 void *__mutex;
287 unsigned int __nwaiters;
288 unsigned int __broadcast_seq;
289 } __data;
290 char __size[48];
291 __extension__ long long int __align;
292} pthread_cond_t;
293typedef union
294{
295 char __size[4];
296 int __align;
297} pthread_condattr_t;
298typedef unsigned int pthread_key_t;
299typedef int pthread_once_t;
300typedef union
301{
302 struct
303 {
304 int __lock;
305 unsigned int __nr_readers;
306 unsigned int __readers_wakeup;
307 unsigned int __writer_wakeup;
308 unsigned int __nr_readers_queued;
309 unsigned int __nr_writers_queued;
310 int __writer;
311 int __shared;
312 unsigned long int __pad1;
313 unsigned long int __pad2;
314 unsigned int __flags;
315 } __data;
316 char __size[56];
317 long int __align;
318} pthread_rwlock_t;
319typedef union
320{
321 char __size[8];
322 long int __align;
323} pthread_rwlockattr_t;
324typedef volatile int pthread_spinlock_t;
325typedef union
326{
327 char __size[32];
328 long int __align;
329} pthread_barrier_t;
330typedef union
331{
332 char __size[4];
333 int __align;
334} pthread_barrierattr_t;
335
336extern long int random (void) __attribute__ ((__nothrow__ , __leaf__));
337extern void srandom (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));
338extern char *initstate (unsigned int __seed, char *__statebuf,
339 size_t __statelen) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
340
341
342extern char *setstate (char *__statebuf) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
343
344
345
346
347
348
349
350struct random_data
351 {
352 int32_t *fptr;
353 int32_t *rptr;
354 int32_t *state;
355 int rand_type;
356 int rand_deg;
357 int rand_sep;
358 int32_t *end_ptr;
359 };
360
361extern int random_r (struct random_data *__restrict __buf,
362 int32_t *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
363
364extern int srandom_r (unsigned int __seed, struct random_data *__buf)
365 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
366
367extern int initstate_r (unsigned int __seed, char *__restrict __statebuf,
368 size_t __statelen,
369 struct random_data *__restrict __buf)
370 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 4)));
371
372extern int setstate_r (char *__restrict __statebuf,
373 struct random_data *__restrict __buf)
374 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
375
376
377
378
379
380
381extern int rand (void) __attribute__ ((__nothrow__ , __leaf__));
382
383extern void srand (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));
384
385
386
387
388extern int rand_r (unsigned int *__seed) __attribute__ ((__nothrow__ , __leaf__));
389
390
391
392
393
394
395
396extern double drand48 (void) __attribute__ ((__nothrow__ , __leaf__));
397extern double erand48 (unsigned short int __xsubi[3]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
398
399
400extern long int lrand48 (void) __attribute__ ((__nothrow__ , __leaf__));
401extern long int nrand48 (unsigned short int __xsubi[3])
402 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
403
404
405extern long int mrand48 (void) __attribute__ ((__nothrow__ , __leaf__));
406extern long int jrand48 (unsigned short int __xsubi[3])
407 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
408
409
410extern void srand48 (long int __seedval) __attribute__ ((__nothrow__ , __leaf__));
411extern unsigned short int *seed48 (unsigned short int __seed16v[3])
412 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
413extern void lcong48 (unsigned short int __param[7]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
414
415
416
417
418
419struct drand48_data
420 {
421 unsigned short int __x[3];
422 unsigned short int __old_x[3];
423 unsigned short int __c;
424 unsigned short int __init;
425 unsigned long long int __a;
426 };
427
428
429extern int drand48_r (struct drand48_data *__restrict __buffer,
430 double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
431extern int erand48_r (unsigned short int __xsubi[3],
432 struct drand48_data *__restrict __buffer,
433 double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
434
435
436extern int lrand48_r (struct drand48_data *__restrict __buffer,
437 long int *__restrict __result)
438 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
439extern int nrand48_r (unsigned short int __xsubi[3],
440 struct drand48_data *__restrict __buffer,
441 long int *__restrict __result)
442 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
443
444
445extern int mrand48_r (struct drand48_data *__restrict __buffer,
446 long int *__restrict __result)
447 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
448extern int jrand48_r (unsigned short int __xsubi[3],
449 struct drand48_data *__restrict __buffer,
450 long int *__restrict __result)
451 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
452
453
454extern int srand48_r (long int __seedval, struct drand48_data *__buffer)
455 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
456
457extern int seed48_r (unsigned short int __seed16v[3],
458 struct drand48_data *__buffer) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
459
460extern int lcong48_r (unsigned short int __param[7],
461 struct drand48_data *__buffer)
462 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
463
464
465
466
467
468
469
470
471
472extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
473
474extern void *calloc (size_t __nmemb, size_t __size)
475 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
476
477
478
479
480
481
482
483
484
485
486extern void *realloc (void *__ptr, size_t __size)
487 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__warn_unused_result__));
488
489extern void free (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));
490
491
492
493
494extern void cfree (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));
495
496extern void *alloca (size_t __size) __attribute__ ((__nothrow__ , __leaf__));
497
498
499
500
501
502
503
504extern void *valloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
505
506
507
508
509extern int posix_memalign (void **__memptr, size_t __alignment, size_t __size)
510 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
511
512
513
514
515extern void abort (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
516
517
518
519extern int atexit (void (*__func) (void)) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
520
521extern int on_exit (void (*__func) (int __status, void *__arg), void *__arg)
522 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
523
524extern void exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
525
526
527extern void _Exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
528
529
530extern char *getenv (__const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
531
532extern char *__secure_getenv (__const char *__name)
533 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
534extern int putenv (char *__string) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
535extern int setenv (__const char *__name, __const char *__value, int __replace)
536 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
537extern int unsetenv (__const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
538extern int clearenv (void) __attribute__ ((__nothrow__ , __leaf__));
539extern char *mktemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
540extern int mkstemp (char *__template) __attribute__ ((__nonnull__ (1))) ;
541extern int mkstemps (char *__template, int __suffixlen) __attribute__ ((__nonnull__ (1))) ;
542extern char *mkdtemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
543
544extern int system (__const char *__command) ;
545
546extern char *realpath (__const char *__restrict __name,
547 char *__restrict __resolved) __attribute__ ((__nothrow__ , __leaf__)) ;
548typedef int (*__compar_fn_t) (__const void *, __const void *);
549
550extern void *bsearch (__const void *__key, __const void *__base,
551 size_t __nmemb, size_t __size, __compar_fn_t __compar)
552 __attribute__ ((__nonnull__ (1, 2, 5))) ;
553extern void qsort (void *__base, size_t __nmemb, size_t __size,
554 __compar_fn_t __compar) __attribute__ ((__nonnull__ (1, 4)));
555extern int abs (int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
556extern long int labs (long int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
557
558__extension__ extern long long int llabs (long long int __x)
559 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
560
561extern div_t div (int __numer, int __denom)
562 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
563extern ldiv_t ldiv (long int __numer, long int __denom)
564 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
565
566
567__extension__ extern lldiv_t lldiv (long long int __numer,
568 long long int __denom)
569 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
570
571extern char *ecvt (double __value, int __ndigit, int *__restrict __decpt,
572 int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
573extern char *fcvt (double __value, int __ndigit, int *__restrict __decpt,
574 int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
575extern char *gcvt (double __value, int __ndigit, char *__buf)
576 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ;
577extern char *qecvt (long double __value, int __ndigit,
578 int *__restrict __decpt, int *__restrict __sign)
579 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
580extern char *qfcvt (long double __value, int __ndigit,
581 int *__restrict __decpt, int *__restrict __sign)
582 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
583extern char *qgcvt (long double __value, int __ndigit, char *__buf)
584 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ;
585extern int ecvt_r (double __value, int __ndigit, int *__restrict __decpt,
586 int *__restrict __sign, char *__restrict __buf,
587 size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
588extern int fcvt_r (double __value, int __ndigit, int *__restrict __decpt,
589 int *__restrict __sign, char *__restrict __buf,
590 size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
591extern int qecvt_r (long double __value, int __ndigit,
592 int *__restrict __decpt, int *__restrict __sign,
593 char *__restrict __buf, size_t __len)
594 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
595extern int qfcvt_r (long double __value, int __ndigit,
596 int *__restrict __decpt, int *__restrict __sign,
597 char *__restrict __buf, size_t __len)
598 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
599
600extern int mblen (__const char *__s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) ;
601extern int mbtowc (wchar_t *__restrict __pwc,
602 __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) ;
603extern int wctomb (char *__s, wchar_t __wchar) __attribute__ ((__nothrow__ , __leaf__)) ;
604extern size_t mbstowcs (wchar_t *__restrict __pwcs,
605 __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__));
606extern size_t wcstombs (char *__restrict __s,
607 __const wchar_t *__restrict __pwcs, size_t __n)
608 __attribute__ ((__nothrow__ , __leaf__));
609
610extern int rpmatch (__const char *__response) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
611extern int getsubopt (char **__restrict __optionp,
612 char *__const *__restrict __tokens,
613 char **__restrict __valuep)
614 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3))) ;
615extern int getloadavg (double __loadavg[], int __nelem)
616 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
617
618void exit(int s) {
619 _EXIT: goto _EXIT;
620}
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 p->h = 1;
638 p->n = 0;
639 p = a;
640 while (p!=0) {
641 if (p->h != 1) {
642 ERROR: goto ERROR;
643 }
644 p = p->n;
645 }
646 return 0;
647}