1extern int __VERIFIER_nondet_int();
2
3void error(void)
4{
5
6 {
7 goto ERROR;
8 ERROR: ;
9 return;
10}
11}
12int main_in1_val ;
13int main_in1_val_t ;
14int main_in1_ev ;
15int main_in1_req_up ;
16int main_in2_val ;
17int main_in2_val_t ;
18int main_in2_ev ;
19int main_in2_req_up ;
20int main_diff_val ;
21int main_diff_val_t ;
22int main_diff_ev ;
23int main_diff_req_up ;
24int main_sum_val ;
25int main_sum_val_t ;
26int main_sum_ev ;
27int main_sum_req_up ;
28int main_pres_val ;
29int main_pres_val_t ;
30int main_pres_ev ;
31int main_pres_req_up ;
32int main_dbl_val ;
33int main_dbl_val_t ;
34int main_dbl_ev ;
35int main_dbl_req_up ;
36int main_zero_val ;
37int main_zero_val_t ;
38int main_zero_ev ;
39int main_zero_req_up ;
40int main_clk_val ;
41int main_clk_val_t ;
42int main_clk_ev ;
43int main_clk_req_up ;
44int main_clk_pos_edge ;
45int main_clk_neg_edge ;
46int N_generate_st ;
47int N_generate_i ;
48int S1_addsub_st ;
49int S1_addsub_i ;
50int S2_presdbl_st ;
51int S2_presdbl_i ;
52int S3_zero_st ;
53int S3_zero_i ;
54int D_z ;
55int D_print_st ;
56int D_print_i ;
57void N_generate(void)
58{ int a ;
59 int b ;
60
61 {
62 main_in1_val_t = a;
63 main_in1_req_up = 1;
64 main_in2_val_t = b;
65 main_in2_req_up = 1;
66
67 return;
68}
69}
70void S1_addsub(void)
71{ int a ;
72 int b ;
73
74 {
75 a = main_in1_val;
76 b = main_in2_val;
77 main_sum_val_t = a + b;
78 main_sum_req_up = 1;
79 main_diff_val_t = a - b;
80 main_diff_req_up = 1;
81
82 return;
83}
84}
85void S2_presdbl(void)
86{ int a ;
87 int b ;
88 int c ;
89 int d ;
90
91 {
92 a = main_sum_val;
93 b = main_diff_val;
94 main_pres_val_t = a;
95 main_pres_req_up = 1;
96 c = a + b;
97 d = a - b;
98 main_dbl_val_t = c + d;
99 main_dbl_req_up = 1;
100
101 return;
102}
103}
104void S3_zero(void)
105{ int a ;
106 int b ;
107
108 {
109 a = main_pres_val;
110 b = main_dbl_val;
111 main_zero_val_t = b - (a + a);
112 main_zero_req_up = 1;
113
114 return;
115}
116}
117void D_print(void)
118{
119
120 {
121 D_z = main_zero_val;
122
123 return;
124}
125}
126void eval(void)
127{ int tmp ;
128 int tmp___0 ;
129 int tmp___1 ;
130 int tmp___2 ;
131 int tmp___3 ;
132
133 {
134 {
135 while (1) {
136 while_0_continue: ;
137 if ((int )N_generate_st == 0) {
138
139 } else {
140 if ((int )S1_addsub_st == 0) {
141
142 } else {
143 if ((int )S2_presdbl_st == 0) {
144
145 } else {
146 if ((int )S3_zero_st == 0) {
147
148 } else {
149 if ((int )D_print_st == 0) {
150
151 } else {
152 goto while_0_break;
153 }
154 }
155 }
156 }
157 }
158 if ((int )N_generate_st == 0) {
159 {
160 tmp = __VERIFIER_nondet_int();
161 }
162 if (tmp) {
163 {
164 N_generate_st = 1;
165 N_generate();
166 }
167 } else {
168
169 }
170 } else {
171
172 }
173 if ((int )S1_addsub_st == 0) {
174 {
175 tmp___0 = __VERIFIER_nondet_int();
176 }
177 if (tmp___0) {
178 {
179 S1_addsub_st = 1;
180 S1_addsub();
181 }
182 } else {
183
184 }
185 } else {
186
187 }
188 if ((int )S2_presdbl_st == 0) {
189 {
190 tmp___1 = __VERIFIER_nondet_int();
191 }
192 if (tmp___1) {
193 {
194 S2_presdbl_st = 1;
195 S2_presdbl();
196 }
197 } else {
198
199 }
200 } else {
201
202 }
203 if ((int )S3_zero_st == 0) {
204 {
205 tmp___2 = __VERIFIER_nondet_int();
206 }
207 if (tmp___2) {
208 {
209 S3_zero_st = 1;
210 S3_zero();
211 }
212 } else {
213
214 }
215 } else {
216
217 }
218 if ((int )D_print_st == 0) {
219 {
220 tmp___3 = __VERIFIER_nondet_int();
221 }
222 if (tmp___3) {
223 {
224 D_print_st = 1;
225 D_print();
226 }
227 } else {
228
229 }
230 } else {
231
232 }
233 }
234 while_0_break: ;
235 }
236
237 return;
238}
239}
240void start_simulation(void)
241{ int kernel_st ;
242
243 {
244 kernel_st = 0;
245 if ((int )main_in1_req_up == 1) {
246 if (main_in1_val != main_in1_val_t) {
247 main_in1_val = main_in1_val_t;
248 main_in1_ev = 0;
249 } else {
250
251 }
252 main_in1_req_up = 0;
253 } else {
254
255 }
256 if ((int )main_in2_req_up == 1) {
257 if (main_in2_val != main_in2_val_t) {
258 main_in2_val = main_in2_val_t;
259 main_in2_ev = 0;
260 } else {
261
262 }
263 main_in2_req_up = 0;
264 } else {
265
266 }
267 if ((int )main_sum_req_up == 1) {
268 if (main_sum_val != main_sum_val_t) {
269 main_sum_val = main_sum_val_t;
270 main_sum_ev = 0;
271 } else {
272
273 }
274 main_sum_req_up = 0;
275 } else {
276
277 }
278 if ((int )main_diff_req_up == 1) {
279 if (main_diff_val != main_diff_val_t) {
280 main_diff_val = main_diff_val_t;
281 main_diff_ev = 0;
282 } else {
283
284 }
285 main_diff_req_up = 0;
286 } else {
287
288 }
289 if ((int )main_pres_req_up == 1) {
290 if (main_pres_val != main_pres_val_t) {
291 main_pres_val = main_pres_val_t;
292 main_pres_ev = 0;
293 } else {
294
295 }
296 main_pres_req_up = 0;
297 } else {
298
299 }
300 if ((int )main_dbl_req_up == 1) {
301 if (main_dbl_val != main_dbl_val_t) {
302 main_dbl_val = main_dbl_val_t;
303 main_dbl_ev = 0;
304 } else {
305
306 }
307 main_dbl_req_up = 0;
308 } else {
309
310 }
311 if ((int )main_zero_req_up == 1) {
312 if (main_zero_val != main_zero_val_t) {
313 main_zero_val = main_zero_val_t;
314 main_zero_ev = 0;
315 } else {
316
317 }
318 main_zero_req_up = 0;
319 } else {
320
321 }
322 if ((int )main_clk_req_up == 1) {
323 if ((int )main_clk_val != (int )main_clk_val_t) {
324 main_clk_val = main_clk_val_t;
325 main_clk_ev = 0;
326 if ((int )main_clk_val == 1) {
327 main_clk_pos_edge = 0;
328 main_clk_neg_edge = 2;
329 } else {
330 main_clk_neg_edge = 0;
331 main_clk_pos_edge = 2;
332 }
333 } else {
334
335 }
336 main_clk_req_up = 0;
337 } else {
338
339 }
340 if ((int )N_generate_i == 1) {
341 N_generate_st = 0;
342 } else {
343 N_generate_st = 2;
344 }
345 if ((int )S1_addsub_i == 1) {
346 S1_addsub_st = 0;
347 } else {
348 S1_addsub_st = 2;
349 }
350 if ((int )S2_presdbl_i == 1) {
351 S2_presdbl_st = 0;
352 } else {
353 S2_presdbl_st = 2;
354 }
355 if ((int )S3_zero_i == 1) {
356 S3_zero_st = 0;
357 } else {
358 S3_zero_st = 2;
359 }
360 if ((int )D_print_i == 1) {
361 D_print_st = 0;
362 } else {
363 D_print_st = 2;
364 }
365 if ((int )main_in1_ev == 0) {
366 main_in1_ev = 1;
367 } else {
368
369 }
370 if ((int )main_in2_ev == 0) {
371 main_in2_ev = 1;
372 } else {
373
374 }
375 if ((int )main_sum_ev == 0) {
376 main_sum_ev = 1;
377 } else {
378
379 }
380 if ((int )main_diff_ev == 0) {
381 main_diff_ev = 1;
382 } else {
383
384 }
385 if ((int )main_pres_ev == 0) {
386 main_pres_ev = 1;
387 } else {
388
389 }
390 if ((int )main_dbl_ev == 0) {
391 main_dbl_ev = 1;
392 } else {
393
394 }
395 if ((int )main_zero_ev == 0) {
396 main_zero_ev = 1;
397 } else {
398
399 }
400 if ((int )main_clk_ev == 0) {
401 main_clk_ev = 1;
402 } else {
403
404 }
405 if ((int )main_clk_pos_edge == 0) {
406 main_clk_pos_edge = 1;
407 } else {
408
409 }
410 if ((int )main_clk_neg_edge == 0) {
411 main_clk_neg_edge = 1;
412 } else {
413
414 }
415 if ((int )main_clk_pos_edge == 1) {
416 N_generate_st = 0;
417 } else {
418
419 }
420 if ((int )main_clk_pos_edge == 1) {
421 S1_addsub_st = 0;
422 } else {
423
424 }
425 if ((int )main_clk_pos_edge == 1) {
426 S2_presdbl_st = 0;
427 } else {
428
429 }
430 if ((int )main_clk_pos_edge == 1) {
431 S3_zero_st = 0;
432 } else {
433
434 }
435 if ((int )main_clk_pos_edge == 1) {
436 D_print_st = 0;
437 } else {
438
439 }
440 if ((int )main_in1_ev == 1) {
441 main_in1_ev = 2;
442 } else {
443
444 }
445 if ((int )main_in2_ev == 1) {
446 main_in2_ev = 2;
447 } else {
448
449 }
450 if ((int )main_sum_ev == 1) {
451 main_sum_ev = 2;
452 } else {
453
454 }
455 if ((int )main_diff_ev == 1) {
456 main_diff_ev = 2;
457 } else {
458
459 }
460 if ((int )main_pres_ev == 1) {
461 main_pres_ev = 2;
462 } else {
463
464 }
465 if ((int )main_dbl_ev == 1) {
466 main_dbl_ev = 2;
467 } else {
468
469 }
470 if ((int )main_zero_ev == 1) {
471 main_zero_ev = 2;
472 } else {
473
474 }
475 if ((int )main_clk_ev == 1) {
476 main_clk_ev = 2;
477 } else {
478
479 }
480 if ((int )main_clk_pos_edge == 1) {
481 main_clk_pos_edge = 2;
482 } else {
483
484 }
485 if ((int )main_clk_neg_edge == 1) {
486 main_clk_neg_edge = 2;
487 } else {
488
489 }
490 {
491 while (1) {
492 while_1_continue: ;
493 {
494 kernel_st = 1;
495 eval();
496 }
497 kernel_st = 2;
498 if ((int )main_in1_req_up == 1) {
499 if (main_in1_val != main_in1_val_t) {
500 main_in1_val = main_in1_val_t;
501 main_in1_ev = 0;
502 } else {
503
504 }
505 main_in1_req_up = 0;
506 } else {
507
508 }
509 if ((int )main_in2_req_up == 1) {
510 if (main_in2_val != main_in2_val_t) {
511 main_in2_val = main_in2_val_t;
512 main_in2_ev = 0;
513 } else {
514
515 }
516 main_in2_req_up = 0;
517 } else {
518
519 }
520 if ((int )main_sum_req_up == 1) {
521 if (main_sum_val != main_sum_val_t) {
522 main_sum_val = main_sum_val_t;
523 main_sum_ev = 0;
524 } else {
525
526 }
527 main_sum_req_up = 0;
528 } else {
529
530 }
531 if ((int )main_diff_req_up == 1) {
532 if (main_diff_val != main_diff_val_t) {
533 main_diff_val = main_diff_val_t;
534 main_diff_ev = 0;
535 } else {
536
537 }
538 main_diff_req_up = 0;
539 } else {
540
541 }
542 if ((int )main_pres_req_up == 1) {
543 if (main_pres_val != main_pres_val_t) {
544 main_pres_val = main_pres_val_t;
545 main_pres_ev = 0;
546 } else {
547
548 }
549 main_pres_req_up = 0;
550 } else {
551
552 }
553 if ((int )main_dbl_req_up == 1) {
554 if (main_dbl_val != main_dbl_val_t) {
555 main_dbl_val = main_dbl_val_t;
556 main_dbl_ev = 0;
557 } else {
558
559 }
560 main_dbl_req_up = 0;
561 } else {
562
563 }
564 if ((int )main_zero_req_up == 1) {
565 if (main_zero_val != main_zero_val_t) {
566 main_zero_val = main_zero_val_t;
567 main_zero_ev = 0;
568 } else {
569
570 }
571 main_zero_req_up = 0;
572 } else {
573
574 }
575 if ((int )main_clk_req_up == 1) {
576 if ((int )main_clk_val != (int )main_clk_val_t) {
577 main_clk_val = main_clk_val_t;
578 main_clk_ev = 0;
579 if ((int )main_clk_val == 1) {
580 main_clk_pos_edge = 0;
581 main_clk_neg_edge = 2;
582 } else {
583 main_clk_neg_edge = 0;
584 main_clk_pos_edge = 2;
585 }
586 } else {
587
588 }
589 main_clk_req_up = 0;
590 } else {
591
592 }
593 kernel_st = 3;
594 if ((int )main_in1_ev == 0) {
595 main_in1_ev = 1;
596 } else {
597
598 }
599 if ((int )main_in2_ev == 0) {
600 main_in2_ev = 1;
601 } else {
602
603 }
604 if ((int )main_sum_ev == 0) {
605 main_sum_ev = 1;
606 } else {
607
608 }
609 if ((int )main_diff_ev == 0) {
610 main_diff_ev = 1;
611 } else {
612
613 }
614 if ((int )main_pres_ev == 0) {
615 main_pres_ev = 1;
616 } else {
617
618 }
619 if ((int )main_dbl_ev == 0) {
620 main_dbl_ev = 1;
621 } else {
622
623 }
624 if ((int )main_zero_ev == 0) {
625 main_zero_ev = 1;
626 } else {
627
628 }
629 if ((int )main_clk_ev == 0) {
630 main_clk_ev = 1;
631 } else {
632
633 }
634 if ((int )main_clk_pos_edge == 0) {
635 main_clk_pos_edge = 1;
636 } else {
637
638 }
639 if ((int )main_clk_neg_edge == 0) {
640 main_clk_neg_edge = 1;
641 } else {
642
643 }
644 if ((int )main_clk_pos_edge == 1) {
645 N_generate_st = 0;
646 } else {
647
648 }
649 if ((int )main_clk_pos_edge == 1) {
650 S1_addsub_st = 0;
651 } else {
652
653 }
654 if ((int )main_clk_pos_edge == 1) {
655 S2_presdbl_st = 0;
656 } else {
657
658 }
659 if ((int )main_clk_pos_edge == 1) {
660 S3_zero_st = 0;
661 } else {
662
663 }
664 if ((int )main_clk_pos_edge == 1) {
665 D_print_st = 0;
666 } else {
667
668 }
669 if ((int )main_in1_ev == 1) {
670 main_in1_ev = 2;
671 } else {
672
673 }
674 if ((int )main_in2_ev == 1) {
675 main_in2_ev = 2;
676 } else {
677
678 }
679 if ((int )main_sum_ev == 1) {
680 main_sum_ev = 2;
681 } else {
682
683 }
684 if ((int )main_diff_ev == 1) {
685 main_diff_ev = 2;
686 } else {
687
688 }
689 if ((int )main_pres_ev == 1) {
690 main_pres_ev = 2;
691 } else {
692
693 }
694 if ((int )main_dbl_ev == 1) {
695 main_dbl_ev = 2;
696 } else {
697
698 }
699 if ((int )main_zero_ev == 1) {
700 main_zero_ev = 2;
701 } else {
702
703 }
704 if ((int )main_clk_ev == 1) {
705 main_clk_ev = 2;
706 } else {
707
708 }
709 if ((int )main_clk_pos_edge == 1) {
710 main_clk_pos_edge = 2;
711 } else {
712
713 }
714 if ((int )main_clk_neg_edge == 1) {
715 main_clk_neg_edge = 2;
716 } else {
717
718 }
719 if ((int )N_generate_st == 0) {
720
721 } else {
722 if ((int )S1_addsub_st == 0) {
723
724 } else {
725 if ((int )S2_presdbl_st == 0) {
726
727 } else {
728 if ((int )S3_zero_st == 0) {
729
730 } else {
731 if ((int )D_print_st == 0) {
732
733 } else {
734 goto while_1_break;
735 }
736 }
737 }
738 }
739 }
740 }
741 while_1_break: ;
742 }
743
744 return;
745}
746}
747int main(void)
748{ int count ;
749 int __retres2 ;
750
751 {
752 {
753
754 main_in1_ev = 2;
755 main_in1_req_up = 0;
756 main_in2_ev = 2;
757 main_in2_req_up = 0;
758 main_diff_ev = 2;
759 main_diff_req_up = 0;
760 main_sum_ev = 2;
761 main_sum_req_up = 0;
762 main_pres_ev = 2;
763 main_pres_req_up = 0;
764 main_dbl_ev = 2;
765 main_dbl_req_up = 0;
766 main_zero_ev = 2;
767 main_zero_req_up = 0;
768 main_clk_val = 0;
769 main_clk_ev = 2;
770 main_clk_req_up = 0;
771 main_clk_pos_edge = 2;
772 main_clk_neg_edge = 2;
773
774
775 count = 0;
776 N_generate_i = 0;
777 S1_addsub_i = 0;
778 S2_presdbl_i = 0;
779 S3_zero_i = 0;
780 D_print_i = 0;
781 start_simulation();
782 }
783 {
784 while (1) {
785 while_2_continue: ;
786 {
787 main_clk_val_t = 1;
788 main_clk_req_up = 1;
789 start_simulation();
790 count += 1;
791 }
792 if (count == 5) {
793 if ((D_z == 0)) {
794 {
795 error();
796 }
797 } else {
798
799 }
800 count = 0;
801 } else {
802
803 }
804 {
805 main_clk_val_t = 0;
806 main_clk_req_up = 1;
807 start_simulation();
808 }
809 }
810 while_2_break: ;
811 }
812 __retres2 = 0;
813 return (__retres2);
814}
815}