// This file is part of the SV-Benchmarks collection of verification tasks: // https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks // // SPDX-FileCopyrightText: 2013 Carnegie Mellon University // SPDX-FileCopyrightText: 2014-2021 The SV-Benchmarks Community // SPDX-FileCopyrightText: 2018 Marie-Christine Jakobs, LMU Munich // // SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU-LMU int __return_main; void abort(void); extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); void reach_error() { __assert_fail("0", "pals_floodmax.4.ufo.BOUNDED-8.pals.c.p+lhb-reducer.c", 4, "reach_error"); } char __VERIFIER_nondet_char(); _Bool __VERIFIER_nondet_bool(); void assert(_Bool arg); void abort(void); void assume_abort_if_not(int cond) { if(!cond) {abort();} } typedef char msg_t; typedef int port_t; void read(port_t p, msg_t m); void write(port_t p, msg_t m); msg_t nomsg = (msg_t )-1; port_t p12 = 0; char p12_old = '\x0'; char p12_new = '\x0'; _Bool ep12 = 0; port_t p13 = 0; char p13_old = '\x0'; char p13_new = '\x0'; _Bool ep13 = 0; port_t p14 = 0; char p14_old = '\x0'; char p14_new = '\x0'; _Bool ep14 = 0; port_t p21 = 0; char p21_old = '\x0'; char p21_new = '\x0'; _Bool ep21 = 0; port_t p23 = 0; char p23_old = '\x0'; char p23_new = '\x0'; _Bool ep23 = 0; port_t p24 = 0; char p24_old = '\x0'; char p24_new = '\x0'; _Bool ep24 = 0; port_t p31 = 0; char p31_old = '\x0'; char p31_new = '\x0'; _Bool ep31 = 0; port_t p32 = 0; char p32_old = '\x0'; char p32_new = '\x0'; _Bool ep32 = 0; port_t p34 = 0; char p34_old = '\x0'; char p34_new = '\x0'; _Bool ep34 = 0; port_t p41 = 0; char p41_old = '\x0'; char p41_new = '\x0'; _Bool ep41 = 0; port_t p42 = 0; char p42_old = '\x0'; char p42_new = '\x0'; _Bool ep42 = 0; port_t p43 = 0; char p43_old = '\x0'; char p43_new = '\x0'; _Bool ep43 = 0; char id1 = '\x0'; char r1 = '\x0'; char st1 = '\x0'; char nl1 = '\x0'; char m1 = '\x0'; char max1 = '\x0'; _Bool mode1 = 0; char id2 = '\x0'; char r2 = '\x0'; char st2 = '\x0'; char nl2 = '\x0'; char m2 = '\x0'; char max2 = '\x0'; _Bool mode2 = 0; char id3 = '\x0'; char r3 = '\x0'; char st3 = '\x0'; char nl3 = '\x0'; char m3 = '\x0'; char max3 = '\x0'; _Bool mode3 = 0; char id4 = '\x0'; char r4 = '\x0'; char st4 = '\x0'; char nl4 = '\x0'; char m4 = '\x0'; char max4 = '\x0'; _Bool mode4 = 0; void node1(); void node2(); void node3(); void node4(); void (*nodes[4])() = { &node1, &node2, &node3, &node4 }; int init(); int check(); int main(); int __return_4402; int __return_4592; int __return_4763; int __return_4934; int __return_5105; int __return_5276; int __return_5447; int __tmp_5454_0; int __return_5621; int __return_5461; int main() { int main__c1; int main__i2; main__c1 = 0; ep12 = __VERIFIER_nondet_bool(); ep13 = __VERIFIER_nondet_bool(); ep14 = __VERIFIER_nondet_bool(); ep21 = __VERIFIER_nondet_bool(); ep23 = __VERIFIER_nondet_bool(); ep24 = __VERIFIER_nondet_bool(); ep31 = __VERIFIER_nondet_bool(); ep32 = __VERIFIER_nondet_bool(); ep34 = __VERIFIER_nondet_bool(); ep41 = __VERIFIER_nondet_bool(); ep42 = __VERIFIER_nondet_bool(); ep43 = __VERIFIER_nondet_bool(); id1 = __VERIFIER_nondet_char(); r1 = __VERIFIER_nondet_char(); st1 = __VERIFIER_nondet_char(); nl1 = __VERIFIER_nondet_char(); m1 = __VERIFIER_nondet_char(); max1 = __VERIFIER_nondet_char(); mode1 = __VERIFIER_nondet_bool(); id2 = __VERIFIER_nondet_char(); r2 = __VERIFIER_nondet_char(); st2 = __VERIFIER_nondet_char(); nl2 = __VERIFIER_nondet_char(); m2 = __VERIFIER_nondet_char(); max2 = __VERIFIER_nondet_char(); mode2 = __VERIFIER_nondet_bool(); id3 = __VERIFIER_nondet_char(); r3 = __VERIFIER_nondet_char(); st3 = __VERIFIER_nondet_char(); nl3 = __VERIFIER_nondet_char(); m3 = __VERIFIER_nondet_char(); max3 = __VERIFIER_nondet_char(); mode3 = __VERIFIER_nondet_bool(); id4 = __VERIFIER_nondet_char(); r4 = __VERIFIER_nondet_char(); st4 = __VERIFIER_nondet_char(); nl4 = __VERIFIER_nondet_char(); m4 = __VERIFIER_nondet_char(); max4 = __VERIFIER_nondet_char(); mode4 = __VERIFIER_nondet_bool(); { _Bool init__r121; _Bool init__r131; _Bool init__r141; _Bool init__r211; _Bool init__r231; _Bool init__r241; _Bool init__r311; _Bool init__r321; _Bool init__r341; _Bool init__r411; _Bool init__r421; _Bool init__r431; _Bool init__r122; int init__tmp; _Bool init__r132; int init__tmp___0; _Bool init__r142; int init__tmp___1; _Bool init__r212; int init__tmp___2; _Bool init__r232; int init__tmp___3; _Bool init__r242; int init__tmp___4; _Bool init__r312; int init__tmp___5; _Bool init__r322; int init__tmp___6; _Bool init__r342; int init__tmp___7; _Bool init__r412; int init__tmp___8; _Bool init__r422; int init__tmp___9; _Bool init__r432; int init__tmp___10; _Bool init__r123; int init__tmp___11; _Bool init__r133; int init__tmp___12; _Bool init__r143; int init__tmp___13; _Bool init__r213; int init__tmp___14; _Bool init__r233; int init__tmp___15; _Bool init__r243; int init__tmp___16; _Bool init__r313; int init__tmp___17; _Bool init__r323; int init__tmp___18; _Bool init__r343; int init__tmp___19; _Bool init__r413; int init__tmp___20; _Bool init__r423; int init__tmp___21; _Bool init__r433; int init__tmp___22; int init__tmp___23; init__r121 = ep12; init__r131 = ep13; init__r141 = ep14; init__r211 = ep21; init__r231 = ep23; init__r241 = ep24; init__r311 = ep31; init__r321 = ep32; init__r341 = ep34; init__r411 = ep41; init__r421 = ep42; init__r431 = ep43; if (!(init__r121 == 0)) { init__tmp = 1; label_4281:; init__r122 = (_Bool)init__tmp; if (!(init__r131 == 0)) { init__tmp___0 = 1; label_4286:; init__r132 = (_Bool)init__tmp___0; if (!(init__r141 == 0)) { init__tmp___1 = 1; label_4291:; init__r142 = (_Bool)init__tmp___1; if (!(init__r211 == 0)) { init__tmp___2 = 1; label_4296:; init__r212 = (_Bool)init__tmp___2; if (!(init__r231 == 0)) { init__tmp___3 = 1; label_4301:; init__r232 = (_Bool)init__tmp___3; if (!(init__r241 == 0)) { init__tmp___4 = 1; label_4306:; init__r242 = (_Bool)init__tmp___4; if (!(init__r311 == 0)) { init__tmp___5 = 1; label_4311:; init__r312 = (_Bool)init__tmp___5; if (!(init__r321 == 0)) { init__tmp___6 = 1; label_4316:; init__r322 = (_Bool)init__tmp___6; if (!(init__r341 == 0)) { init__tmp___7 = 1; label_4321:; init__r342 = (_Bool)init__tmp___7; if (!(init__r411 == 0)) { init__tmp___8 = 1; label_4326:; init__r412 = (_Bool)init__tmp___8; if (!(init__r421 == 0)) { init__tmp___9 = 1; label_4331:; init__r422 = (_Bool)init__tmp___9; if (!(init__r431 == 0)) { init__tmp___10 = 1; label_4336:; init__r432 = (_Bool)init__tmp___10; if (!(init__r122 == 0)) { init__tmp___11 = 1; label_4341:; init__r123 = (_Bool)init__tmp___11; if (!(init__r132 == 0)) { init__tmp___12 = 1; label_4346:; init__r133 = (_Bool)init__tmp___12; if (!(init__r142 == 0)) { init__tmp___13 = 1; label_4351:; init__r143 = (_Bool)init__tmp___13; if (!(init__r212 == 0)) { init__tmp___14 = 1; label_4356:; init__r213 = (_Bool)init__tmp___14; if (!(init__r232 == 0)) { init__tmp___15 = 1; label_4361:; init__r233 = (_Bool)init__tmp___15; if (!(init__r242 == 0)) { init__tmp___16 = 1; label_4366:; init__r243 = (_Bool)init__tmp___16; if (!(init__r312 == 0)) { init__tmp___17 = 1; label_4371:; init__r313 = (_Bool)init__tmp___17; if (!(init__r322 == 0)) { init__tmp___18 = 1; label_4376:; init__r323 = (_Bool)init__tmp___18; if (!(init__r342 == 0)) { init__tmp___19 = 1; label_4381:; init__r343 = (_Bool)init__tmp___19; if (!(init__r412 == 0)) { init__tmp___20 = 1; label_4386:; init__r413 = (_Bool)init__tmp___20; if (!(init__r422 == 0)) { init__tmp___21 = 1; label_4391:; init__r423 = (_Bool)init__tmp___21; if (!(init__r432 == 0)) { init__tmp___22 = 1; label_4396:; init__r433 = (_Bool)init__tmp___22; if (((int)id1) != ((int)id2)) { if (((int)id1) != ((int)id3)) { if (((int)id1) != ((int)id4)) { if (((int)id2) != ((int)id3)) { if (((int)id2) != ((int)id4)) { if (((int)id3) != ((int)id4)) { if (((int)id1) >= 0) { if (((int)id2) >= 0) { if (((int)id3) >= 0) { if (((int)id4) >= 0) { if (((int)r1) == 0) { if (((int)r2) == 0) { if (((int)r3) == 0) { if (((int)r4) == 0) { if (!(init__r123 == 0)) { if (!(init__r133 == 0)) { if (!(init__r143 == 0)) { if (!(init__r213 == 0)) { if (!(init__r233 == 0)) { if (!(init__r243 == 0)) { if (!(init__r313 == 0)) { if (!(init__r323 == 0)) { if (!(init__r343 == 0)) { if (!(init__r413 == 0)) { if (!(init__r423 == 0)) { if (!(init__r433 == 0)) { if (((int)max1) == ((int)id1)) { if (((int)max2) == ((int)id2)) { if (((int)max3) == ((int)id3)) { if (((int)max4) == ((int)id4)) { if (((int)st1) == 0) { if (((int)st2) == 0) { if (((int)st3) == 0) { if (((int)st4) == 0) { if (((int)nl1) == 0) { if (((int)nl2) == 0) { if (((int)nl3) == 0) { if (((int)nl4) == 0) { if (((int)mode1) == 0) { if (((int)mode2) == 0) { if (((int)mode3) == 0) { if (((int)mode4) == 0) { init__tmp___23 = 1; label_6966:; label_6962:; label_6958:; label_6954:; label_6950:; label_6946:; label_6942:; label_6938:; label_6934:; label_6930:; label_6926:; label_6922:; label_6918:; label_6914:; label_6910:; label_6894:; label_6895:; label_6896:; label_6897:; label_6898:; label_6899:; label_6900:; label_6901:; label_6902:; label_6903:; label_6904:; label_6905:; label_6906:; label_6866:; label_6862:; label_6858:; label_6854:; label_6850:; label_6846:; label_6842:; label_6838:; label_6834:; label_6830:; label_6826:; label_6822:; label_6818:; label_4401:; __return_4402 = init__tmp___23; main__i2 = __return_4402; if (main__i2 != 0) { p12_old = nomsg; p12_new = nomsg; p13_old = nomsg; p13_new = nomsg; p14_old = nomsg; p14_new = nomsg; p21_old = nomsg; p21_new = nomsg; p23_old = nomsg; p23_new = nomsg; p24_old = nomsg; p24_new = nomsg; p31_old = nomsg; p31_new = nomsg; p32_old = nomsg; p32_new = nomsg; p34_old = nomsg; p34_new = nomsg; p41_old = nomsg; p41_new = nomsg; p42_old = nomsg; p42_new = nomsg; p43_old = nomsg; p43_new = nomsg; main__i2 = 0; if (main__i2 < 8) { { if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4438:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4445:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4452:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_4460:; mode1 = 0; label_4462:; { if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4470:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4477:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4484:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_4492:; mode2 = 0; label_4494:; { if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4502:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4509:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4516:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_4524:; mode3 = 0; label_4526:; { if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4534:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4541:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4548:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_4556:; mode4 = 0; label_4558:; p12_old = p12_new; p12_new = nomsg; p13_old = p13_new; p13_new = nomsg; p14_old = p14_new; p14_new = nomsg; p21_old = p21_new; p21_new = nomsg; p23_old = p23_new; p23_new = nomsg; p24_old = p24_new; p24_new = nomsg; p31_old = p31_new; p31_new = nomsg; p32_old = p32_new; p32_new = nomsg; p34_old = p34_new; p34_new = nomsg; p41_old = p41_new; p41_new = nomsg; p42_old = p42_new; p42_new = nomsg; p43_old = p43_new; p43_new = nomsg; { int check__tmp; if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) <= 1) { if ((((int)st1) + ((int)nl1)) <= 1) { if ((((int)st2) + ((int)nl2)) <= 1) { if ((((int)st3) + ((int)nl3)) <= 1) { if ((((int)st4) + ((int)nl4)) <= 1) { if (((int)r1) >= 3) { label_6668:; if (((int)r1) < 3) { label_6675:; if (((int)r1) >= 3) { label_6682:; if (((int)r1) < 3) { check__tmp = 1; label_6688:; label_6681:; label_6674:; label_6667:; label_6661:; label_6657:; label_6653:; label_6649:; label_4591:; __return_4592 = check__tmp; main__c1 = __return_4592; { _Bool __tmp_1; __tmp_1 = main__c1; _Bool assert__arg; assert__arg = __tmp_1; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4609:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4616:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4623:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_4631:; mode1 = 0; label_4633:; { if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4641:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4648:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4655:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_4663:; mode2 = 0; label_4665:; { if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4673:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4680:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4687:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_4695:; mode3 = 0; label_4697:; { if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4705:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4712:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4719:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_4727:; mode4 = 0; label_4729:; p12_old = p12_new; p12_new = nomsg; p13_old = p13_new; p13_new = nomsg; p14_old = p14_new; p14_new = nomsg; p21_old = p21_new; p21_new = nomsg; p23_old = p23_new; p23_new = nomsg; p24_old = p24_new; p24_new = nomsg; p31_old = p31_new; p31_new = nomsg; p32_old = p32_new; p32_new = nomsg; p34_old = p34_new; p34_new = nomsg; p41_old = p41_new; p41_new = nomsg; p42_old = p42_new; p42_new = nomsg; p43_old = p43_new; p43_new = nomsg; { int check__tmp; if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) <= 1) { if ((((int)st1) + ((int)nl1)) <= 1) { if ((((int)st2) + ((int)nl2)) <= 1) { if ((((int)st3) + ((int)nl3)) <= 1) { if ((((int)st4) + ((int)nl4)) <= 1) { if (((int)r1) >= 3) { label_6499:; if (((int)r1) < 3) { label_6506:; if (((int)r1) >= 3) { label_6513:; if (((int)r1) < 3) { check__tmp = 1; label_6519:; label_6512:; label_6505:; label_6498:; label_6492:; label_6488:; label_6484:; label_6480:; label_4762:; __return_4763 = check__tmp; main__c1 = __return_4763; { _Bool __tmp_2; __tmp_2 = main__c1; _Bool assert__arg; assert__arg = __tmp_2; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4780:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4787:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4794:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_4802:; mode1 = 0; label_4804:; { if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4812:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4819:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4826:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_4834:; mode2 = 0; label_4836:; { if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4844:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4851:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4858:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_4866:; mode3 = 0; label_4868:; { if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4876:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4883:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4890:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_4898:; mode4 = 0; label_4900:; p12_old = p12_new; p12_new = nomsg; p13_old = p13_new; p13_new = nomsg; p14_old = p14_new; p14_new = nomsg; p21_old = p21_new; p21_new = nomsg; p23_old = p23_new; p23_new = nomsg; p24_old = p24_new; p24_new = nomsg; p31_old = p31_new; p31_new = nomsg; p32_old = p32_new; p32_new = nomsg; p34_old = p34_new; p34_new = nomsg; p41_old = p41_new; p41_new = nomsg; p42_old = p42_new; p42_new = nomsg; p43_old = p43_new; p43_new = nomsg; { int check__tmp; if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) <= 1) { if ((((int)st1) + ((int)nl1)) <= 1) { if ((((int)st2) + ((int)nl2)) <= 1) { if ((((int)st3) + ((int)nl3)) <= 1) { if ((((int)st4) + ((int)nl4)) <= 1) { if (((int)r1) >= 3) { label_6330:; if (((int)r1) < 3) { label_6337:; if (((int)r1) >= 3) { label_6344:; if (((int)r1) < 3) { check__tmp = 1; label_6350:; label_6343:; label_6336:; label_6329:; label_6323:; label_6319:; label_6315:; label_6311:; label_4933:; __return_4934 = check__tmp; main__c1 = __return_4934; { _Bool __tmp_3; __tmp_3 = main__c1; _Bool assert__arg; assert__arg = __tmp_3; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4951:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4958:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4965:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_4973:; mode1 = 0; label_4975:; { if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4983:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4990:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4997:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5005:; mode2 = 0; label_5007:; { if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5015:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5022:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5029:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5037:; mode3 = 0; label_5039:; { if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5047:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5054:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5061:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5069:; mode4 = 0; label_5071:; p12_old = p12_new; p12_new = nomsg; p13_old = p13_new; p13_new = nomsg; p14_old = p14_new; p14_new = nomsg; p21_old = p21_new; p21_new = nomsg; p23_old = p23_new; p23_new = nomsg; p24_old = p24_new; p24_new = nomsg; p31_old = p31_new; p31_new = nomsg; p32_old = p32_new; p32_new = nomsg; p34_old = p34_new; p34_new = nomsg; p41_old = p41_new; p41_new = nomsg; p42_old = p42_new; p42_new = nomsg; p43_old = p43_new; p43_new = nomsg; { int check__tmp; if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) <= 1) { if ((((int)st1) + ((int)nl1)) <= 1) { if ((((int)st2) + ((int)nl2)) <= 1) { if ((((int)st3) + ((int)nl3)) <= 1) { if ((((int)st4) + ((int)nl4)) <= 1) { if (((int)r1) >= 3) { label_6161:; if (((int)r1) < 3) { label_6168:; if (((int)r1) >= 3) { label_6175:; if (((int)r1) < 3) { check__tmp = 1; label_6181:; label_6174:; label_6167:; label_6160:; label_6154:; label_6150:; label_6146:; label_6142:; label_5104:; __return_5105 = check__tmp; main__c1 = __return_5105; { _Bool __tmp_4; __tmp_4 = main__c1; _Bool assert__arg; assert__arg = __tmp_4; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5122:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5129:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5136:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5144:; mode1 = 0; label_5146:; { if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5154:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5161:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5168:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5176:; mode2 = 0; label_5178:; { if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5186:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5193:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5200:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5208:; mode3 = 0; label_5210:; { if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5218:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5225:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5232:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5240:; mode4 = 0; label_5242:; p12_old = p12_new; p12_new = nomsg; p13_old = p13_new; p13_new = nomsg; p14_old = p14_new; p14_new = nomsg; p21_old = p21_new; p21_new = nomsg; p23_old = p23_new; p23_new = nomsg; p24_old = p24_new; p24_new = nomsg; p31_old = p31_new; p31_new = nomsg; p32_old = p32_new; p32_new = nomsg; p34_old = p34_new; p34_new = nomsg; p41_old = p41_new; p41_new = nomsg; p42_old = p42_new; p42_new = nomsg; p43_old = p43_new; p43_new = nomsg; { int check__tmp; if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) <= 1) { if ((((int)st1) + ((int)nl1)) <= 1) { if ((((int)st2) + ((int)nl2)) <= 1) { if ((((int)st3) + ((int)nl3)) <= 1) { if ((((int)st4) + ((int)nl4)) <= 1) { if (((int)r1) >= 3) { label_5992:; if (((int)r1) < 3) { label_5999:; if (((int)r1) >= 3) { label_6006:; if (((int)r1) < 3) { check__tmp = 1; label_6012:; label_6005:; label_5998:; label_5991:; label_5985:; label_5981:; label_5977:; label_5973:; label_5275:; __return_5276 = check__tmp; main__c1 = __return_5276; { _Bool __tmp_5; __tmp_5 = main__c1; _Bool assert__arg; assert__arg = __tmp_5; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5293:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5300:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5307:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5315:; mode1 = 0; label_5317:; { if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5325:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5332:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5339:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5347:; mode2 = 0; label_5349:; { if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5357:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5364:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5371:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5379:; mode3 = 0; label_5381:; { if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5389:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5396:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5403:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5411:; mode4 = 0; label_5413:; p12_old = p12_new; p12_new = nomsg; p13_old = p13_new; p13_new = nomsg; p14_old = p14_new; p14_new = nomsg; p21_old = p21_new; p21_new = nomsg; p23_old = p23_new; p23_new = nomsg; p24_old = p24_new; p24_new = nomsg; p31_old = p31_new; p31_new = nomsg; p32_old = p32_new; p32_new = nomsg; p34_old = p34_new; p34_new = nomsg; p41_old = p41_new; p41_new = nomsg; p42_old = p42_new; p42_new = nomsg; p43_old = p43_new; p43_new = nomsg; { int check__tmp; if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) <= 1) { if ((((int)st1) + ((int)nl1)) <= 1) { if ((((int)st2) + ((int)nl2)) <= 1) { if ((((int)st3) + ((int)nl3)) <= 1) { if ((((int)st4) + ((int)nl4)) <= 1) { if (((int)r1) >= 3) { label_5823:; if (((int)r1) < 3) { label_5830:; if (((int)r1) >= 3) { label_5837:; if (((int)r1) < 3) { check__tmp = 1; label_5843:; label_5836:; label_5829:; label_5822:; label_5816:; label_5812:; label_5808:; label_5804:; label_5446:; __return_5447 = check__tmp; main__c1 = __return_5447; { _Bool __tmp_6; __tmp_6 = main__c1; _Bool assert__arg; assert__arg = __tmp_6; if (assert__arg == 0) { {reach_error();} return __return_main; } else { __tmp_5454_0 = main____CPAchecker_TMP_0; label_5454:; main____CPAchecker_TMP_0 = __tmp_5454_0; int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5467:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5474:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5481:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5489:; mode1 = 0; label_5491:; { if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5499:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5506:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5513:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5521:; mode2 = 0; label_5523:; { if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5531:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5538:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5545:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5553:; mode3 = 0; label_5555:; { if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5563:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5570:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5577:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5585:; mode4 = 0; label_5587:; p12_old = p12_new; p12_new = nomsg; p13_old = p13_new; p13_new = nomsg; p14_old = p14_new; p14_new = nomsg; p21_old = p21_new; p21_new = nomsg; p23_old = p23_new; p23_new = nomsg; p24_old = p24_new; p24_new = nomsg; p31_old = p31_new; p31_new = nomsg; p32_old = p32_new; p32_new = nomsg; p34_old = p34_new; p34_new = nomsg; p41_old = p41_new; p41_new = nomsg; p42_old = p42_new; p42_new = nomsg; p43_old = p43_new; p43_new = nomsg; { int check__tmp; if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) <= 1) { if ((((int)st1) + ((int)nl1)) <= 1) { if ((((int)st2) + ((int)nl2)) <= 1) { if ((((int)st3) + ((int)nl3)) <= 1) { if ((((int)st4) + ((int)nl4)) <= 1) { if (((int)r1) >= 3) { label_5652:; if (((int)r1) < 3) { label_5659:; if (((int)r1) >= 3) { label_5666:; if (((int)r1) < 3) { check__tmp = 1; label_5672:; label_5665:; label_5658:; label_5651:; label_5645:; label_5641:; label_5637:; label_5633:; label_5620:; __return_5621 = check__tmp; main__c1 = __return_5621; { _Bool __tmp_7; __tmp_7 = main__c1; _Bool assert__arg; assert__arg = __tmp_7; if (assert__arg == 0) { {reach_error();} return __return_main; } else { __tmp_5454_0 = main____CPAchecker_TMP_0; goto label_5454; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5672; } else { check__tmp = 0; goto label_5672; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5666; } else { check__tmp = 0; goto label_5665; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_5659; } else { check__tmp = 0; goto label_5658; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_5652; } else { check__tmp = 0; goto label_5651; } } } else { check__tmp = 0; goto label_5645; } } else { check__tmp = 0; goto label_5641; } } else { check__tmp = 0; goto label_5637; } } else { check__tmp = 0; goto label_5633; } } else { check__tmp = 0; goto label_5620; } } } else { nl4 = 1; goto label_5585; } } else { goto label_5585; } } else { goto label_5577; } } else { goto label_5577; } } else { goto label_5570; } } else { goto label_5570; } } else { goto label_5563; } } else { goto label_5563; } } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_5687:; p41_new = node4____CPAchecker_TMP_0; label_5682:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5695:; p42_new = node4____CPAchecker_TMP_1; label_5690:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5703:; p43_new = node4____CPAchecker_TMP_2; label_5680:; mode4 = 1; goto label_5587; } else { label_5702:; node4____CPAchecker_TMP_2 = p43_new; goto label_5703; } } else { goto label_5702; } } else { goto label_5680; } } else { label_5694:; node4____CPAchecker_TMP_1 = p42_new; goto label_5695; } } else { goto label_5694; } } else { goto label_5690; } } else { label_5686:; node4____CPAchecker_TMP_0 = p41_new; goto label_5687; } } else { goto label_5686; } } else { goto label_5682; } } else { goto label_5680; } } } } else { nl3 = 1; goto label_5553; } } else { goto label_5553; } } else { goto label_5545; } } else { goto label_5545; } } else { goto label_5538; } } else { goto label_5538; } } else { goto label_5531; } } else { goto label_5531; } } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_5718:; p31_new = node3____CPAchecker_TMP_0; label_5713:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5726:; p32_new = node3____CPAchecker_TMP_1; label_5721:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5734:; p34_new = node3____CPAchecker_TMP_2; label_5711:; mode3 = 1; goto label_5555; } else { label_5733:; node3____CPAchecker_TMP_2 = p34_new; goto label_5734; } } else { goto label_5733; } } else { goto label_5711; } } else { label_5725:; node3____CPAchecker_TMP_1 = p32_new; goto label_5726; } } else { goto label_5725; } } else { goto label_5721; } } else { label_5717:; node3____CPAchecker_TMP_0 = p31_new; goto label_5718; } } else { goto label_5717; } } else { goto label_5713; } } else { goto label_5711; } } } } else { nl2 = 1; goto label_5521; } } else { goto label_5521; } } else { goto label_5513; } } else { goto label_5513; } } else { goto label_5506; } } else { goto label_5506; } } else { goto label_5499; } } else { goto label_5499; } } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_5749:; p21_new = node2____CPAchecker_TMP_0; label_5744:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5757:; p23_new = node2____CPAchecker_TMP_1; label_5752:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5765:; p24_new = node2____CPAchecker_TMP_2; label_5742:; mode2 = 1; goto label_5523; } else { label_5764:; node2____CPAchecker_TMP_2 = p24_new; goto label_5765; } } else { goto label_5764; } } else { goto label_5742; } } else { label_5756:; node2____CPAchecker_TMP_1 = p23_new; goto label_5757; } } else { goto label_5756; } } else { goto label_5752; } } else { label_5748:; node2____CPAchecker_TMP_0 = p21_new; goto label_5749; } } else { goto label_5748; } } else { goto label_5744; } } else { goto label_5742; } } } } else { nl1 = 1; goto label_5489; } } else { goto label_5489; } } else { goto label_5481; } } else { goto label_5481; } } else { goto label_5474; } } else { goto label_5474; } } else { goto label_5467; } } else { goto label_5467; } } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_5780:; p12_new = node1____CPAchecker_TMP_0; label_5775:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5788:; p13_new = node1____CPAchecker_TMP_1; label_5783:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5796:; p14_new = node1____CPAchecker_TMP_2; label_5773:; mode1 = 1; goto label_5491; } else { label_5795:; node1____CPAchecker_TMP_2 = p14_new; goto label_5796; } } else { goto label_5795; } } else { goto label_5773; } } else { label_5787:; node1____CPAchecker_TMP_1 = p13_new; goto label_5788; } } else { goto label_5787; } } else { goto label_5783; } } else { label_5779:; node1____CPAchecker_TMP_0 = p12_new; goto label_5780; } } else { goto label_5779; } } else { goto label_5775; } } else { goto label_5773; } } } } else { __return_5461 = 0; return __return_5461; } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5843; } else { check__tmp = 0; goto label_5843; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5837; } else { check__tmp = 0; goto label_5836; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_5830; } else { check__tmp = 0; goto label_5829; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_5823; } else { check__tmp = 0; goto label_5822; } } } else { check__tmp = 0; goto label_5816; } } else { check__tmp = 0; goto label_5812; } } else { check__tmp = 0; goto label_5808; } } else { check__tmp = 0; goto label_5804; } } else { check__tmp = 0; goto label_5446; } } } else { nl4 = 1; goto label_5411; } } else { goto label_5411; } } else { goto label_5403; } } else { goto label_5403; } } else { goto label_5396; } } else { goto label_5396; } } else { goto label_5389; } } else { goto label_5389; } } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_5858:; p41_new = node4____CPAchecker_TMP_0; label_5853:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5866:; p42_new = node4____CPAchecker_TMP_1; label_5861:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5874:; p43_new = node4____CPAchecker_TMP_2; label_5851:; mode4 = 1; goto label_5413; } else { label_5873:; node4____CPAchecker_TMP_2 = p43_new; goto label_5874; } } else { goto label_5873; } } else { goto label_5851; } } else { label_5865:; node4____CPAchecker_TMP_1 = p42_new; goto label_5866; } } else { goto label_5865; } } else { goto label_5861; } } else { label_5857:; node4____CPAchecker_TMP_0 = p41_new; goto label_5858; } } else { goto label_5857; } } else { goto label_5853; } } else { goto label_5851; } } } } else { nl3 = 1; goto label_5379; } } else { goto label_5379; } } else { goto label_5371; } } else { goto label_5371; } } else { goto label_5364; } } else { goto label_5364; } } else { goto label_5357; } } else { goto label_5357; } } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_5889:; p31_new = node3____CPAchecker_TMP_0; label_5884:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5897:; p32_new = node3____CPAchecker_TMP_1; label_5892:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5905:; p34_new = node3____CPAchecker_TMP_2; label_5882:; mode3 = 1; goto label_5381; } else { label_5904:; node3____CPAchecker_TMP_2 = p34_new; goto label_5905; } } else { goto label_5904; } } else { goto label_5882; } } else { label_5896:; node3____CPAchecker_TMP_1 = p32_new; goto label_5897; } } else { goto label_5896; } } else { goto label_5892; } } else { label_5888:; node3____CPAchecker_TMP_0 = p31_new; goto label_5889; } } else { goto label_5888; } } else { goto label_5884; } } else { goto label_5882; } } } } else { nl2 = 1; goto label_5347; } } else { goto label_5347; } } else { goto label_5339; } } else { goto label_5339; } } else { goto label_5332; } } else { goto label_5332; } } else { goto label_5325; } } else { goto label_5325; } } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_5920:; p21_new = node2____CPAchecker_TMP_0; label_5915:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5928:; p23_new = node2____CPAchecker_TMP_1; label_5923:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5936:; p24_new = node2____CPAchecker_TMP_2; label_5913:; mode2 = 1; goto label_5349; } else { label_5935:; node2____CPAchecker_TMP_2 = p24_new; goto label_5936; } } else { goto label_5935; } } else { goto label_5913; } } else { label_5927:; node2____CPAchecker_TMP_1 = p23_new; goto label_5928; } } else { goto label_5927; } } else { goto label_5923; } } else { label_5919:; node2____CPAchecker_TMP_0 = p21_new; goto label_5920; } } else { goto label_5919; } } else { goto label_5915; } } else { goto label_5913; } } } } else { nl1 = 1; goto label_5315; } } else { goto label_5315; } } else { goto label_5307; } } else { goto label_5307; } } else { goto label_5300; } } else { goto label_5300; } } else { goto label_5293; } } else { goto label_5293; } } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_5951:; p12_new = node1____CPAchecker_TMP_0; label_5946:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5959:; p13_new = node1____CPAchecker_TMP_1; label_5954:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5967:; p14_new = node1____CPAchecker_TMP_2; label_5944:; mode1 = 1; goto label_5317; } else { label_5966:; node1____CPAchecker_TMP_2 = p14_new; goto label_5967; } } else { goto label_5966; } } else { goto label_5944; } } else { label_5958:; node1____CPAchecker_TMP_1 = p13_new; goto label_5959; } } else { goto label_5958; } } else { goto label_5954; } } else { label_5950:; node1____CPAchecker_TMP_0 = p12_new; goto label_5951; } } else { goto label_5950; } } else { goto label_5946; } } else { goto label_5944; } } } } else { return __return_main; } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6012; } else { check__tmp = 0; goto label_6012; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6006; } else { check__tmp = 0; goto label_6005; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_5999; } else { check__tmp = 0; goto label_5998; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_5992; } else { check__tmp = 0; goto label_5991; } } } else { check__tmp = 0; goto label_5985; } } else { check__tmp = 0; goto label_5981; } } else { check__tmp = 0; goto label_5977; } } else { check__tmp = 0; goto label_5973; } } else { check__tmp = 0; goto label_5275; } } } else { nl4 = 1; goto label_5240; } } else { goto label_5240; } } else { goto label_5232; } } else { goto label_5232; } } else { goto label_5225; } } else { goto label_5225; } } else { goto label_5218; } } else { goto label_5218; } } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_6027:; p41_new = node4____CPAchecker_TMP_0; label_6022:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_6035:; p42_new = node4____CPAchecker_TMP_1; label_6030:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_6043:; p43_new = node4____CPAchecker_TMP_2; label_6020:; mode4 = 1; goto label_5242; } else { label_6042:; node4____CPAchecker_TMP_2 = p43_new; goto label_6043; } } else { goto label_6042; } } else { goto label_6020; } } else { label_6034:; node4____CPAchecker_TMP_1 = p42_new; goto label_6035; } } else { goto label_6034; } } else { goto label_6030; } } else { label_6026:; node4____CPAchecker_TMP_0 = p41_new; goto label_6027; } } else { goto label_6026; } } else { goto label_6022; } } else { goto label_6020; } } } } else { nl3 = 1; goto label_5208; } } else { goto label_5208; } } else { goto label_5200; } } else { goto label_5200; } } else { goto label_5193; } } else { goto label_5193; } } else { goto label_5186; } } else { goto label_5186; } } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_6058:; p31_new = node3____CPAchecker_TMP_0; label_6053:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_6066:; p32_new = node3____CPAchecker_TMP_1; label_6061:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_6074:; p34_new = node3____CPAchecker_TMP_2; label_6051:; mode3 = 1; goto label_5210; } else { label_6073:; node3____CPAchecker_TMP_2 = p34_new; goto label_6074; } } else { goto label_6073; } } else { goto label_6051; } } else { label_6065:; node3____CPAchecker_TMP_1 = p32_new; goto label_6066; } } else { goto label_6065; } } else { goto label_6061; } } else { label_6057:; node3____CPAchecker_TMP_0 = p31_new; goto label_6058; } } else { goto label_6057; } } else { goto label_6053; } } else { goto label_6051; } } } } else { nl2 = 1; goto label_5176; } } else { goto label_5176; } } else { goto label_5168; } } else { goto label_5168; } } else { goto label_5161; } } else { goto label_5161; } } else { goto label_5154; } } else { goto label_5154; } } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_6089:; p21_new = node2____CPAchecker_TMP_0; label_6084:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_6097:; p23_new = node2____CPAchecker_TMP_1; label_6092:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_6105:; p24_new = node2____CPAchecker_TMP_2; label_6082:; mode2 = 1; goto label_5178; } else { label_6104:; node2____CPAchecker_TMP_2 = p24_new; goto label_6105; } } else { goto label_6104; } } else { goto label_6082; } } else { label_6096:; node2____CPAchecker_TMP_1 = p23_new; goto label_6097; } } else { goto label_6096; } } else { goto label_6092; } } else { label_6088:; node2____CPAchecker_TMP_0 = p21_new; goto label_6089; } } else { goto label_6088; } } else { goto label_6084; } } else { goto label_6082; } } } } else { nl1 = 1; goto label_5144; } } else { goto label_5144; } } else { goto label_5136; } } else { goto label_5136; } } else { goto label_5129; } } else { goto label_5129; } } else { goto label_5122; } } else { goto label_5122; } } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_6120:; p12_new = node1____CPAchecker_TMP_0; label_6115:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_6128:; p13_new = node1____CPAchecker_TMP_1; label_6123:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_6136:; p14_new = node1____CPAchecker_TMP_2; label_6113:; mode1 = 1; goto label_5146; } else { label_6135:; node1____CPAchecker_TMP_2 = p14_new; goto label_6136; } } else { goto label_6135; } } else { goto label_6113; } } else { label_6127:; node1____CPAchecker_TMP_1 = p13_new; goto label_6128; } } else { goto label_6127; } } else { goto label_6123; } } else { label_6119:; node1____CPAchecker_TMP_0 = p12_new; goto label_6120; } } else { goto label_6119; } } else { goto label_6115; } } else { goto label_6113; } } } } else { return __return_main; } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6181; } else { check__tmp = 0; goto label_6181; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6175; } else { check__tmp = 0; goto label_6174; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_6168; } else { check__tmp = 0; goto label_6167; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_6161; } else { check__tmp = 0; goto label_6160; } } } else { check__tmp = 0; goto label_6154; } } else { check__tmp = 0; goto label_6150; } } else { check__tmp = 0; goto label_6146; } } else { check__tmp = 0; goto label_6142; } } else { check__tmp = 0; goto label_5104; } } } else { nl4 = 1; goto label_5069; } } else { goto label_5069; } } else { goto label_5061; } } else { goto label_5061; } } else { goto label_5054; } } else { goto label_5054; } } else { goto label_5047; } } else { goto label_5047; } } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_6196:; p41_new = node4____CPAchecker_TMP_0; label_6191:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_6204:; p42_new = node4____CPAchecker_TMP_1; label_6199:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_6212:; p43_new = node4____CPAchecker_TMP_2; label_6189:; mode4 = 1; goto label_5071; } else { label_6211:; node4____CPAchecker_TMP_2 = p43_new; goto label_6212; } } else { goto label_6211; } } else { goto label_6189; } } else { label_6203:; node4____CPAchecker_TMP_1 = p42_new; goto label_6204; } } else { goto label_6203; } } else { goto label_6199; } } else { label_6195:; node4____CPAchecker_TMP_0 = p41_new; goto label_6196; } } else { goto label_6195; } } else { goto label_6191; } } else { goto label_6189; } } } } else { nl3 = 1; goto label_5037; } } else { goto label_5037; } } else { goto label_5029; } } else { goto label_5029; } } else { goto label_5022; } } else { goto label_5022; } } else { goto label_5015; } } else { goto label_5015; } } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_6227:; p31_new = node3____CPAchecker_TMP_0; label_6222:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_6235:; p32_new = node3____CPAchecker_TMP_1; label_6230:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_6243:; p34_new = node3____CPAchecker_TMP_2; label_6220:; mode3 = 1; goto label_5039; } else { label_6242:; node3____CPAchecker_TMP_2 = p34_new; goto label_6243; } } else { goto label_6242; } } else { goto label_6220; } } else { label_6234:; node3____CPAchecker_TMP_1 = p32_new; goto label_6235; } } else { goto label_6234; } } else { goto label_6230; } } else { label_6226:; node3____CPAchecker_TMP_0 = p31_new; goto label_6227; } } else { goto label_6226; } } else { goto label_6222; } } else { goto label_6220; } } } } else { nl2 = 1; goto label_5005; } } else { goto label_5005; } } else { goto label_4997; } } else { goto label_4997; } } else { goto label_4990; } } else { goto label_4990; } } else { goto label_4983; } } else { goto label_4983; } } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_6258:; p21_new = node2____CPAchecker_TMP_0; label_6253:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_6266:; p23_new = node2____CPAchecker_TMP_1; label_6261:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_6274:; p24_new = node2____CPAchecker_TMP_2; label_6251:; mode2 = 1; goto label_5007; } else { label_6273:; node2____CPAchecker_TMP_2 = p24_new; goto label_6274; } } else { goto label_6273; } } else { goto label_6251; } } else { label_6265:; node2____CPAchecker_TMP_1 = p23_new; goto label_6266; } } else { goto label_6265; } } else { goto label_6261; } } else { label_6257:; node2____CPAchecker_TMP_0 = p21_new; goto label_6258; } } else { goto label_6257; } } else { goto label_6253; } } else { goto label_6251; } } } } else { nl1 = 1; goto label_4973; } } else { goto label_4973; } } else { goto label_4965; } } else { goto label_4965; } } else { goto label_4958; } } else { goto label_4958; } } else { goto label_4951; } } else { goto label_4951; } } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_6289:; p12_new = node1____CPAchecker_TMP_0; label_6284:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_6297:; p13_new = node1____CPAchecker_TMP_1; label_6292:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_6305:; p14_new = node1____CPAchecker_TMP_2; label_6282:; mode1 = 1; goto label_4975; } else { label_6304:; node1____CPAchecker_TMP_2 = p14_new; goto label_6305; } } else { goto label_6304; } } else { goto label_6282; } } else { label_6296:; node1____CPAchecker_TMP_1 = p13_new; goto label_6297; } } else { goto label_6296; } } else { goto label_6292; } } else { label_6288:; node1____CPAchecker_TMP_0 = p12_new; goto label_6289; } } else { goto label_6288; } } else { goto label_6284; } } else { goto label_6282; } } } } else { return __return_main; } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6350; } else { check__tmp = 0; goto label_6350; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6344; } else { check__tmp = 0; goto label_6343; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_6337; } else { check__tmp = 0; goto label_6336; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_6330; } else { check__tmp = 0; goto label_6329; } } } else { check__tmp = 0; goto label_6323; } } else { check__tmp = 0; goto label_6319; } } else { check__tmp = 0; goto label_6315; } } else { check__tmp = 0; goto label_6311; } } else { check__tmp = 0; goto label_4933; } } } else { nl4 = 1; goto label_4898; } } else { goto label_4898; } } else { goto label_4890; } } else { goto label_4890; } } else { goto label_4883; } } else { goto label_4883; } } else { goto label_4876; } } else { goto label_4876; } } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_6365:; p41_new = node4____CPAchecker_TMP_0; label_6360:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_6373:; p42_new = node4____CPAchecker_TMP_1; label_6368:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_6381:; p43_new = node4____CPAchecker_TMP_2; label_6358:; mode4 = 1; goto label_4900; } else { label_6380:; node4____CPAchecker_TMP_2 = p43_new; goto label_6381; } } else { goto label_6380; } } else { goto label_6358; } } else { label_6372:; node4____CPAchecker_TMP_1 = p42_new; goto label_6373; } } else { goto label_6372; } } else { goto label_6368; } } else { label_6364:; node4____CPAchecker_TMP_0 = p41_new; goto label_6365; } } else { goto label_6364; } } else { goto label_6360; } } else { goto label_6358; } } } } else { nl3 = 1; goto label_4866; } } else { goto label_4866; } } else { goto label_4858; } } else { goto label_4858; } } else { goto label_4851; } } else { goto label_4851; } } else { goto label_4844; } } else { goto label_4844; } } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_6396:; p31_new = node3____CPAchecker_TMP_0; label_6391:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_6404:; p32_new = node3____CPAchecker_TMP_1; label_6399:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_6412:; p34_new = node3____CPAchecker_TMP_2; label_6389:; mode3 = 1; goto label_4868; } else { label_6411:; node3____CPAchecker_TMP_2 = p34_new; goto label_6412; } } else { goto label_6411; } } else { goto label_6389; } } else { label_6403:; node3____CPAchecker_TMP_1 = p32_new; goto label_6404; } } else { goto label_6403; } } else { goto label_6399; } } else { label_6395:; node3____CPAchecker_TMP_0 = p31_new; goto label_6396; } } else { goto label_6395; } } else { goto label_6391; } } else { goto label_6389; } } } } else { nl2 = 1; goto label_4834; } } else { goto label_4834; } } else { goto label_4826; } } else { goto label_4826; } } else { goto label_4819; } } else { goto label_4819; } } else { goto label_4812; } } else { goto label_4812; } } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_6427:; p21_new = node2____CPAchecker_TMP_0; label_6422:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_6435:; p23_new = node2____CPAchecker_TMP_1; label_6430:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_6443:; p24_new = node2____CPAchecker_TMP_2; label_6420:; mode2 = 1; goto label_4836; } else { label_6442:; node2____CPAchecker_TMP_2 = p24_new; goto label_6443; } } else { goto label_6442; } } else { goto label_6420; } } else { label_6434:; node2____CPAchecker_TMP_1 = p23_new; goto label_6435; } } else { goto label_6434; } } else { goto label_6430; } } else { label_6426:; node2____CPAchecker_TMP_0 = p21_new; goto label_6427; } } else { goto label_6426; } } else { goto label_6422; } } else { goto label_6420; } } } } else { nl1 = 1; goto label_4802; } } else { goto label_4802; } } else { goto label_4794; } } else { goto label_4794; } } else { goto label_4787; } } else { goto label_4787; } } else { goto label_4780; } } else { goto label_4780; } } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_6458:; p12_new = node1____CPAchecker_TMP_0; label_6453:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_6466:; p13_new = node1____CPAchecker_TMP_1; label_6461:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_6474:; p14_new = node1____CPAchecker_TMP_2; label_6451:; mode1 = 1; goto label_4804; } else { label_6473:; node1____CPAchecker_TMP_2 = p14_new; goto label_6474; } } else { goto label_6473; } } else { goto label_6451; } } else { label_6465:; node1____CPAchecker_TMP_1 = p13_new; goto label_6466; } } else { goto label_6465; } } else { goto label_6461; } } else { label_6457:; node1____CPAchecker_TMP_0 = p12_new; goto label_6458; } } else { goto label_6457; } } else { goto label_6453; } } else { goto label_6451; } } } } else { return __return_main; } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6519; } else { check__tmp = 0; goto label_6519; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6513; } else { check__tmp = 0; goto label_6512; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_6506; } else { check__tmp = 0; goto label_6505; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_6499; } else { check__tmp = 0; goto label_6498; } } } else { check__tmp = 0; goto label_6492; } } else { check__tmp = 0; goto label_6488; } } else { check__tmp = 0; goto label_6484; } } else { check__tmp = 0; goto label_6480; } } else { check__tmp = 0; goto label_4762; } } } else { nl4 = 1; goto label_4727; } } else { goto label_4727; } } else { goto label_4719; } } else { goto label_4719; } } else { goto label_4712; } } else { goto label_4712; } } else { goto label_4705; } } else { goto label_4705; } } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_6534:; p41_new = node4____CPAchecker_TMP_0; label_6529:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_6542:; p42_new = node4____CPAchecker_TMP_1; label_6537:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_6550:; p43_new = node4____CPAchecker_TMP_2; label_6527:; mode4 = 1; goto label_4729; } else { label_6549:; node4____CPAchecker_TMP_2 = p43_new; goto label_6550; } } else { goto label_6549; } } else { goto label_6527; } } else { label_6541:; node4____CPAchecker_TMP_1 = p42_new; goto label_6542; } } else { goto label_6541; } } else { goto label_6537; } } else { label_6533:; node4____CPAchecker_TMP_0 = p41_new; goto label_6534; } } else { goto label_6533; } } else { goto label_6529; } } else { goto label_6527; } } } } else { nl3 = 1; goto label_4695; } } else { goto label_4695; } } else { goto label_4687; } } else { goto label_4687; } } else { goto label_4680; } } else { goto label_4680; } } else { goto label_4673; } } else { goto label_4673; } } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_6565:; p31_new = node3____CPAchecker_TMP_0; label_6560:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_6573:; p32_new = node3____CPAchecker_TMP_1; label_6568:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_6581:; p34_new = node3____CPAchecker_TMP_2; label_6558:; mode3 = 1; goto label_4697; } else { label_6580:; node3____CPAchecker_TMP_2 = p34_new; goto label_6581; } } else { goto label_6580; } } else { goto label_6558; } } else { label_6572:; node3____CPAchecker_TMP_1 = p32_new; goto label_6573; } } else { goto label_6572; } } else { goto label_6568; } } else { label_6564:; node3____CPAchecker_TMP_0 = p31_new; goto label_6565; } } else { goto label_6564; } } else { goto label_6560; } } else { goto label_6558; } } } } else { nl2 = 1; goto label_4663; } } else { goto label_4663; } } else { goto label_4655; } } else { goto label_4655; } } else { goto label_4648; } } else { goto label_4648; } } else { goto label_4641; } } else { goto label_4641; } } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_6596:; p21_new = node2____CPAchecker_TMP_0; label_6591:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_6604:; p23_new = node2____CPAchecker_TMP_1; label_6599:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_6612:; p24_new = node2____CPAchecker_TMP_2; label_6589:; mode2 = 1; goto label_4665; } else { label_6611:; node2____CPAchecker_TMP_2 = p24_new; goto label_6612; } } else { goto label_6611; } } else { goto label_6589; } } else { label_6603:; node2____CPAchecker_TMP_1 = p23_new; goto label_6604; } } else { goto label_6603; } } else { goto label_6599; } } else { label_6595:; node2____CPAchecker_TMP_0 = p21_new; goto label_6596; } } else { goto label_6595; } } else { goto label_6591; } } else { goto label_6589; } } } } else { nl1 = 1; goto label_4631; } } else { goto label_4631; } } else { goto label_4623; } } else { goto label_4623; } } else { goto label_4616; } } else { goto label_4616; } } else { goto label_4609; } } else { goto label_4609; } } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_6627:; p12_new = node1____CPAchecker_TMP_0; label_6622:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_6635:; p13_new = node1____CPAchecker_TMP_1; label_6630:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_6643:; p14_new = node1____CPAchecker_TMP_2; label_6620:; mode1 = 1; goto label_4633; } else { label_6642:; node1____CPAchecker_TMP_2 = p14_new; goto label_6643; } } else { goto label_6642; } } else { goto label_6620; } } else { label_6634:; node1____CPAchecker_TMP_1 = p13_new; goto label_6635; } } else { goto label_6634; } } else { goto label_6630; } } else { label_6626:; node1____CPAchecker_TMP_0 = p12_new; goto label_6627; } } else { goto label_6626; } } else { goto label_6622; } } else { goto label_6620; } } } } else { return __return_main; } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6688; } else { check__tmp = 0; goto label_6688; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6682; } else { check__tmp = 0; goto label_6681; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_6675; } else { check__tmp = 0; goto label_6674; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_6668; } else { check__tmp = 0; goto label_6667; } } } else { check__tmp = 0; goto label_6661; } } else { check__tmp = 0; goto label_6657; } } else { check__tmp = 0; goto label_6653; } } else { check__tmp = 0; goto label_6649; } } else { check__tmp = 0; goto label_4591; } } } else { nl4 = 1; goto label_4556; } } else { goto label_4556; } } else { goto label_4548; } } else { goto label_4548; } } else { goto label_4541; } } else { goto label_4541; } } else { goto label_4534; } } else { goto label_4534; } } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_6703:; p41_new = node4____CPAchecker_TMP_0; label_6698:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_6711:; p42_new = node4____CPAchecker_TMP_1; label_6706:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_6719:; p43_new = node4____CPAchecker_TMP_2; label_6696:; mode4 = 1; goto label_4558; } else { label_6718:; node4____CPAchecker_TMP_2 = p43_new; goto label_6719; } } else { goto label_6718; } } else { goto label_6696; } } else { label_6710:; node4____CPAchecker_TMP_1 = p42_new; goto label_6711; } } else { goto label_6710; } } else { goto label_6706; } } else { label_6702:; node4____CPAchecker_TMP_0 = p41_new; goto label_6703; } } else { goto label_6702; } } else { goto label_6698; } } else { goto label_6696; } } } } else { nl3 = 1; goto label_4524; } } else { goto label_4524; } } else { goto label_4516; } } else { goto label_4516; } } else { goto label_4509; } } else { goto label_4509; } } else { goto label_4502; } } else { goto label_4502; } } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_6734:; p31_new = node3____CPAchecker_TMP_0; label_6729:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_6742:; p32_new = node3____CPAchecker_TMP_1; label_6737:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_6750:; p34_new = node3____CPAchecker_TMP_2; label_6727:; mode3 = 1; goto label_4526; } else { label_6749:; node3____CPAchecker_TMP_2 = p34_new; goto label_6750; } } else { goto label_6749; } } else { goto label_6727; } } else { label_6741:; node3____CPAchecker_TMP_1 = p32_new; goto label_6742; } } else { goto label_6741; } } else { goto label_6737; } } else { label_6733:; node3____CPAchecker_TMP_0 = p31_new; goto label_6734; } } else { goto label_6733; } } else { goto label_6729; } } else { goto label_6727; } } } } else { nl2 = 1; goto label_4492; } } else { goto label_4492; } } else { goto label_4484; } } else { goto label_4484; } } else { goto label_4477; } } else { goto label_4477; } } else { goto label_4470; } } else { goto label_4470; } } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_6765:; p21_new = node2____CPAchecker_TMP_0; label_6760:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_6773:; p23_new = node2____CPAchecker_TMP_1; label_6768:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_6781:; p24_new = node2____CPAchecker_TMP_2; label_6758:; mode2 = 1; goto label_4494; } else { label_6780:; node2____CPAchecker_TMP_2 = p24_new; goto label_6781; } } else { goto label_6780; } } else { goto label_6758; } } else { label_6772:; node2____CPAchecker_TMP_1 = p23_new; goto label_6773; } } else { goto label_6772; } } else { goto label_6768; } } else { label_6764:; node2____CPAchecker_TMP_0 = p21_new; goto label_6765; } } else { goto label_6764; } } else { goto label_6760; } } else { goto label_6758; } } } } else { nl1 = 1; goto label_4460; } } else { goto label_4460; } } else { goto label_4452; } } else { goto label_4452; } } else { goto label_4445; } } else { goto label_4445; } } else { goto label_4438; } } else { goto label_4438; } } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_6796:; p12_new = node1____CPAchecker_TMP_0; label_6791:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_6804:; p13_new = node1____CPAchecker_TMP_1; label_6799:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_6812:; p14_new = node1____CPAchecker_TMP_2; label_6789:; mode1 = 1; goto label_4462; } else { label_6811:; node1____CPAchecker_TMP_2 = p14_new; goto label_6812; } } else { goto label_6811; } } else { goto label_6789; } } else { label_6803:; node1____CPAchecker_TMP_1 = p13_new; goto label_6804; } } else { goto label_6803; } } else { goto label_6799; } } else { label_6795:; node1____CPAchecker_TMP_0 = p12_new; goto label_6796; } } else { goto label_6795; } } else { goto label_6791; } } else { goto label_6789; } } } } else { return __return_main; } } else { return __return_main; } } else { init__tmp___23 = 0; goto label_6966; } } else { init__tmp___23 = 0; goto label_6962; } } else { init__tmp___23 = 0; goto label_6958; } } else { init__tmp___23 = 0; goto label_6954; } } else { init__tmp___23 = 0; goto label_6950; } } else { init__tmp___23 = 0; goto label_6946; } } else { init__tmp___23 = 0; goto label_6942; } } else { init__tmp___23 = 0; goto label_6938; } } else { init__tmp___23 = 0; goto label_6934; } } else { init__tmp___23 = 0; goto label_6930; } } else { init__tmp___23 = 0; goto label_6926; } } else { init__tmp___23 = 0; goto label_6922; } } else { init__tmp___23 = 0; goto label_6918; } } else { init__tmp___23 = 0; goto label_6914; } } else { init__tmp___23 = 0; goto label_6910; } } else { init__tmp___23 = 0; goto label_6894; } } else { init__tmp___23 = 0; goto label_6895; } } else { init__tmp___23 = 0; goto label_6896; } } else { init__tmp___23 = 0; goto label_6897; } } else { init__tmp___23 = 0; goto label_6898; } } else { init__tmp___23 = 0; goto label_6899; } } else { init__tmp___23 = 0; goto label_6900; } } else { init__tmp___23 = 0; goto label_6901; } } else { init__tmp___23 = 0; goto label_6902; } } else { init__tmp___23 = 0; goto label_6903; } } else { init__tmp___23 = 0; goto label_6904; } } else { init__tmp___23 = 0; goto label_6905; } } else { init__tmp___23 = 0; goto label_6906; } } else { init__tmp___23 = 0; goto label_6866; } } else { init__tmp___23 = 0; goto label_6862; } } else { init__tmp___23 = 0; goto label_6858; } } else { init__tmp___23 = 0; goto label_6854; } } else { init__tmp___23 = 0; goto label_6850; } } else { init__tmp___23 = 0; goto label_6846; } } else { init__tmp___23 = 0; goto label_6842; } } else { init__tmp___23 = 0; goto label_6838; } } else { init__tmp___23 = 0; goto label_6834; } } else { init__tmp___23 = 0; goto label_6830; } } else { init__tmp___23 = 0; goto label_6826; } } else { init__tmp___23 = 0; goto label_6822; } } else { init__tmp___23 = 0; goto label_6818; } } else { init__tmp___23 = 0; goto label_4401; } } else { if (!(init__r412 == 0)) { if (!(ep13 == 0)) { init__tmp___22 = 1; goto label_4396; } else { label_6986:; if (!(init__r422 == 0)) { if (!(ep23 == 0)) { init__tmp___22 = 1; label_6992:; goto label_4396; } else { init__tmp___22 = 0; goto label_6992; } } else { init__tmp___22 = 0; goto label_4396; } } } else { goto label_6986; } } } else { if (!(init__r412 == 0)) { if (!(ep12 == 0)) { init__tmp___21 = 1; goto label_4391; } else { label_7001:; if (!(init__r432 == 0)) { if (!(ep32 == 0)) { init__tmp___21 = 1; label_7007:; goto label_4391; } else { init__tmp___21 = 0; goto label_7007; } } else { init__tmp___21 = 0; goto label_4391; } } } else { goto label_7001; } } } else { if (!(init__r422 == 0)) { if (!(ep21 == 0)) { init__tmp___20 = 1; goto label_4386; } else { label_7016:; if (!(init__r432 == 0)) { if (!(ep31 == 0)) { init__tmp___20 = 1; label_7022:; goto label_4386; } else { init__tmp___20 = 0; goto label_7022; } } else { init__tmp___20 = 0; goto label_4386; } } } else { goto label_7016; } } } else { if (!(init__r312 == 0)) { if (!(ep14 == 0)) { init__tmp___19 = 1; goto label_4381; } else { label_7031:; if (!(init__r322 == 0)) { if (!(ep24 == 0)) { init__tmp___19 = 1; label_7037:; goto label_4381; } else { init__tmp___19 = 0; goto label_7037; } } else { init__tmp___19 = 0; goto label_4381; } } } else { goto label_7031; } } } else { if (!(init__r312 == 0)) { if (!(ep12 == 0)) { init__tmp___18 = 1; goto label_4376; } else { label_7046:; if (!(init__r342 == 0)) { if (!(ep42 == 0)) { init__tmp___18 = 1; label_7052:; goto label_4376; } else { init__tmp___18 = 0; goto label_7052; } } else { init__tmp___18 = 0; goto label_4376; } } } else { goto label_7046; } } } else { if (!(init__r322 == 0)) { if (!(ep21 == 0)) { init__tmp___17 = 1; goto label_4371; } else { label_7061:; if (!(init__r342 == 0)) { if (!(ep41 == 0)) { init__tmp___17 = 1; label_7067:; goto label_4371; } else { init__tmp___17 = 0; goto label_7067; } } else { init__tmp___17 = 0; goto label_4371; } } } else { goto label_7061; } } } else { if (!(init__r212 == 0)) { if (!(ep14 == 0)) { init__tmp___16 = 1; goto label_4366; } else { label_7076:; if (!(init__r232 == 0)) { if (!(ep34 == 0)) { init__tmp___16 = 1; label_7082:; goto label_4366; } else { init__tmp___16 = 0; goto label_7082; } } else { init__tmp___16 = 0; goto label_4366; } } } else { goto label_7076; } } } else { if (!(init__r212 == 0)) { if (!(ep13 == 0)) { init__tmp___15 = 1; goto label_4361; } else { label_7091:; if (!(init__r242 == 0)) { if (!(ep43 == 0)) { init__tmp___15 = 1; label_7097:; goto label_4361; } else { init__tmp___15 = 0; goto label_7097; } } else { init__tmp___15 = 0; goto label_4361; } } } else { goto label_7091; } } } else { if (!(init__r232 == 0)) { if (!(ep31 == 0)) { init__tmp___14 = 1; goto label_4356; } else { label_7106:; if (!(init__r242 == 0)) { if (!(ep41 == 0)) { init__tmp___14 = 1; label_7112:; goto label_4356; } else { init__tmp___14 = 0; goto label_7112; } } else { init__tmp___14 = 0; goto label_4356; } } } else { goto label_7106; } } } else { if (!(init__r122 == 0)) { if (!(ep24 == 0)) { init__tmp___13 = 1; goto label_4351; } else { label_7121:; if (!(init__r132 == 0)) { if (!(ep34 == 0)) { init__tmp___13 = 1; label_7127:; goto label_4351; } else { init__tmp___13 = 0; goto label_7127; } } else { init__tmp___13 = 0; goto label_4351; } } } else { goto label_7121; } } } else { if (!(init__r122 == 0)) { if (!(ep23 == 0)) { init__tmp___12 = 1; goto label_4346; } else { label_7136:; if (!(init__r142 == 0)) { if (!(ep43 == 0)) { init__tmp___12 = 1; label_7142:; goto label_4346; } else { init__tmp___12 = 0; goto label_7142; } } else { init__tmp___12 = 0; goto label_4346; } } } else { goto label_7136; } } } else { if (!(init__r132 == 0)) { if (!(ep32 == 0)) { init__tmp___11 = 1; goto label_4341; } else { label_7151:; if (!(init__r142 == 0)) { if (!(ep42 == 0)) { init__tmp___11 = 1; label_7157:; goto label_4341; } else { init__tmp___11 = 0; goto label_7157; } } else { init__tmp___11 = 0; goto label_4341; } } } else { goto label_7151; } } } else { if (!(init__r411 == 0)) { if (!(ep13 == 0)) { init__tmp___10 = 1; goto label_4336; } else { label_7166:; if (!(init__r421 == 0)) { if (!(ep23 == 0)) { init__tmp___10 = 1; label_7172:; goto label_4336; } else { init__tmp___10 = 0; goto label_7172; } } else { init__tmp___10 = 0; goto label_4336; } } } else { goto label_7166; } } } else { if (!(init__r411 == 0)) { if (!(ep12 == 0)) { init__tmp___9 = 1; goto label_4331; } else { label_7181:; if (!(init__r431 == 0)) { if (!(ep32 == 0)) { init__tmp___9 = 1; label_7187:; goto label_4331; } else { init__tmp___9 = 0; goto label_7187; } } else { init__tmp___9 = 0; goto label_4331; } } } else { goto label_7181; } } } else { if (!(init__r421 == 0)) { if (!(ep21 == 0)) { init__tmp___8 = 1; goto label_4326; } else { label_7196:; if (!(init__r431 == 0)) { if (!(ep31 == 0)) { init__tmp___8 = 1; label_7202:; goto label_4326; } else { init__tmp___8 = 0; goto label_7202; } } else { init__tmp___8 = 0; goto label_4326; } } } else { goto label_7196; } } } else { if (!(init__r311 == 0)) { if (!(ep14 == 0)) { init__tmp___7 = 1; goto label_4321; } else { label_7211:; if (!(init__r321 == 0)) { if (!(ep24 == 0)) { init__tmp___7 = 1; label_7217:; goto label_4321; } else { init__tmp___7 = 0; goto label_7217; } } else { init__tmp___7 = 0; goto label_4321; } } } else { goto label_7211; } } } else { if (!(init__r311 == 0)) { if (!(ep12 == 0)) { init__tmp___6 = 1; goto label_4316; } else { label_7226:; if (!(init__r341 == 0)) { if (!(ep42 == 0)) { init__tmp___6 = 1; label_7232:; goto label_4316; } else { init__tmp___6 = 0; goto label_7232; } } else { init__tmp___6 = 0; goto label_4316; } } } else { goto label_7226; } } } else { if (!(init__r321 == 0)) { if (!(ep21 == 0)) { init__tmp___5 = 1; goto label_4311; } else { label_7241:; if (!(init__r341 == 0)) { if (!(ep41 == 0)) { init__tmp___5 = 1; label_7247:; goto label_4311; } else { init__tmp___5 = 0; goto label_7247; } } else { init__tmp___5 = 0; goto label_4311; } } } else { goto label_7241; } } } else { if (!(init__r211 == 0)) { if (!(ep14 == 0)) { init__tmp___4 = 1; goto label_4306; } else { label_7256:; if (!(init__r231 == 0)) { if (!(ep34 == 0)) { init__tmp___4 = 1; label_7262:; goto label_4306; } else { init__tmp___4 = 0; goto label_7262; } } else { init__tmp___4 = 0; goto label_4306; } } } else { goto label_7256; } } } else { if (!(init__r211 == 0)) { if (!(ep13 == 0)) { init__tmp___3 = 1; goto label_4301; } else { label_7271:; if (!(init__r241 == 0)) { if (!(ep43 == 0)) { init__tmp___3 = 1; label_7277:; goto label_4301; } else { init__tmp___3 = 0; goto label_7277; } } else { init__tmp___3 = 0; goto label_4301; } } } else { goto label_7271; } } } else { if (!(init__r231 == 0)) { if (!(ep31 == 0)) { init__tmp___2 = 1; goto label_4296; } else { label_7286:; if (!(init__r241 == 0)) { if (!(ep41 == 0)) { init__tmp___2 = 1; label_7292:; goto label_4296; } else { init__tmp___2 = 0; goto label_7292; } } else { init__tmp___2 = 0; goto label_4296; } } } else { goto label_7286; } } } else { if (!(init__r121 == 0)) { if (!(ep24 == 0)) { init__tmp___1 = 1; goto label_4291; } else { label_7301:; if (!(init__r131 == 0)) { if (!(ep34 == 0)) { init__tmp___1 = 1; label_7307:; goto label_4291; } else { init__tmp___1 = 0; goto label_7307; } } else { init__tmp___1 = 0; goto label_4291; } } } else { goto label_7301; } } } else { if (!(init__r121 == 0)) { if (!(ep23 == 0)) { init__tmp___0 = 1; goto label_4286; } else { label_7316:; if (!(init__r141 == 0)) { if (!(ep43 == 0)) { init__tmp___0 = 1; label_7322:; goto label_4286; } else { init__tmp___0 = 0; goto label_7322; } } else { init__tmp___0 = 0; goto label_4286; } } } else { goto label_7316; } } } else { if (!(init__r131 == 0)) { if (!(ep32 == 0)) { init__tmp = 1; goto label_4281; } else { label_7331:; if (!(init__r141 == 0)) { if (!(ep42 == 0)) { init__tmp = 1; label_7337:; goto label_4281; } else { init__tmp = 0; goto label_7337; } } else { init__tmp = 0; goto label_4281; } } } else { goto label_7331; } } } }