// 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_opt-floodmax.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c", 4, "reach_error"); } char __VERIFIER_nondet_char(); unsigned char __VERIFIER_nondet_uchar(); _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'; unsigned char r1 = '\x0'; char st1 = '\x0'; char nl1 = '\x0'; char m1 = '\x0'; char max1 = '\x0'; _Bool mode1 = 0; _Bool newmax1 = 0; char id2 = '\x0'; unsigned char r2 = '\x0'; char st2 = '\x0'; char nl2 = '\x0'; char m2 = '\x0'; char max2 = '\x0'; _Bool mode2 = 0; _Bool newmax2 = 0; char id3 = '\x0'; unsigned char r3 = '\x0'; char st3 = '\x0'; char nl3 = '\x0'; char m3 = '\x0'; char max3 = '\x0'; _Bool mode3 = 0; _Bool newmax3 = 0; char id4 = '\x0'; unsigned char r4 = '\x0'; char st4 = '\x0'; char nl4 = '\x0'; char m4 = '\x0'; char max4 = '\x0'; _Bool mode4 = 0; _Bool newmax4 = 0; void node1(); void node2(); void node3(); void node4(); void (*nodes[4])() = { &node1, &node2, &node3, &node4 }; int init(); int check(); int main(); int __return_4630; int __return_4872; int __return_5080; int __return_5300; int __return_5508; int __return_5728; int __return_5945; int __return_6146; 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_uchar(); st1 = __VERIFIER_nondet_char(); nl1 = __VERIFIER_nondet_char(); m1 = __VERIFIER_nondet_char(); max1 = __VERIFIER_nondet_char(); mode1 = __VERIFIER_nondet_bool(); newmax1 = __VERIFIER_nondet_bool(); id2 = __VERIFIER_nondet_char(); r2 = __VERIFIER_nondet_uchar(); st2 = __VERIFIER_nondet_char(); nl2 = __VERIFIER_nondet_char(); m2 = __VERIFIER_nondet_char(); max2 = __VERIFIER_nondet_char(); mode2 = __VERIFIER_nondet_bool(); newmax2 = __VERIFIER_nondet_bool(); id3 = __VERIFIER_nondet_char(); r3 = __VERIFIER_nondet_uchar(); st3 = __VERIFIER_nondet_char(); nl3 = __VERIFIER_nondet_char(); m3 = __VERIFIER_nondet_char(); max3 = __VERIFIER_nondet_char(); mode3 = __VERIFIER_nondet_bool(); newmax3 = __VERIFIER_nondet_bool(); id4 = __VERIFIER_nondet_char(); r4 = __VERIFIER_nondet_uchar(); st4 = __VERIFIER_nondet_char(); nl4 = __VERIFIER_nondet_char(); m4 = __VERIFIER_nondet_char(); max4 = __VERIFIER_nondet_char(); mode4 = __VERIFIER_nondet_bool(); newmax4 = __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_4444:; init__r122 = (_Bool)init__tmp; if (!(init__r131 == 0)) { init__tmp___0 = 1; label_4449:; init__r132 = (_Bool)init__tmp___0; if (!(init__r141 == 0)) { init__tmp___1 = 1; label_4454:; init__r142 = (_Bool)init__tmp___1; if (!(init__r211 == 0)) { init__tmp___2 = 1; label_4459:; init__r212 = (_Bool)init__tmp___2; if (!(init__r231 == 0)) { init__tmp___3 = 1; label_4464:; init__r232 = (_Bool)init__tmp___3; if (!(init__r241 == 0)) { init__tmp___4 = 1; label_4469:; init__r242 = (_Bool)init__tmp___4; if (!(init__r311 == 0)) { init__tmp___5 = 1; label_4474:; init__r312 = (_Bool)init__tmp___5; if (!(init__r321 == 0)) { init__tmp___6 = 1; label_4479:; init__r322 = (_Bool)init__tmp___6; if (!(init__r341 == 0)) { init__tmp___7 = 1; label_4484:; init__r342 = (_Bool)init__tmp___7; if (!(init__r411 == 0)) { init__tmp___8 = 1; label_4489:; init__r412 = (_Bool)init__tmp___8; if (!(init__r421 == 0)) { init__tmp___9 = 1; label_4494:; init__r422 = (_Bool)init__tmp___9; if (!(init__r431 == 0)) { init__tmp___10 = 1; label_4499:; init__r432 = (_Bool)init__tmp___10; if (!(init__r122 == 0)) { init__tmp___11 = 1; label_4504:; init__r123 = (_Bool)init__tmp___11; if (!(init__r132 == 0)) { init__tmp___12 = 1; label_4509:; init__r133 = (_Bool)init__tmp___12; if (!(init__r142 == 0)) { init__tmp___13 = 1; label_4514:; init__r143 = (_Bool)init__tmp___13; if (!(init__r212 == 0)) { init__tmp___14 = 1; label_4519:; init__r213 = (_Bool)init__tmp___14; if (!(init__r232 == 0)) { init__tmp___15 = 1; label_4524:; init__r233 = (_Bool)init__tmp___15; if (!(init__r242 == 0)) { init__tmp___16 = 1; label_4529:; init__r243 = (_Bool)init__tmp___16; if (!(init__r312 == 0)) { init__tmp___17 = 1; label_4534:; init__r313 = (_Bool)init__tmp___17; if (!(init__r322 == 0)) { init__tmp___18 = 1; label_4539:; init__r323 = (_Bool)init__tmp___18; if (!(init__r342 == 0)) { init__tmp___19 = 1; label_4544:; init__r343 = (_Bool)init__tmp___19; if (!(init__r412 == 0)) { init__tmp___20 = 1; label_4549:; init__r413 = (_Bool)init__tmp___20; if (!(init__r422 == 0)) { init__tmp___21 = 1; label_4554:; init__r423 = (_Bool)init__tmp___21; if (!(init__r432 == 0)) { init__tmp___22 = 1; label_4559:; 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 (((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) { if (!(newmax1 == 0)) { if (!(newmax2 == 0)) { if (!(newmax3 == 0)) { if (!(newmax4 == 0)) { init__tmp___23 = 1; __return_4630 = init__tmp___23; main__i2 = __return_4630; 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; { _Bool node1__newmax; node1__newmax = 0; if (!(mode1 == 0)) { return __return_main; } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_4674:; p12_new = node1____CPAchecker_TMP_0; label_4667:; if (!(ep13 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4684:; p13_new = node1____CPAchecker_TMP_1; label_4677:; if (!(ep14 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4694:; p14_new = node1____CPAchecker_TMP_2; label_4696:; mode1 = 1; { _Bool node2__newmax; node2__newmax = 0; if (!(mode2 == 0)) { return __return_main; } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_4714:; p21_new = node2____CPAchecker_TMP_0; label_4707:; if (!(ep23 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4724:; p23_new = node2____CPAchecker_TMP_1; label_4717:; if (!(ep24 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4734:; p24_new = node2____CPAchecker_TMP_2; label_4736:; mode2 = 1; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { return __return_main; } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_4754:; p31_new = node3____CPAchecker_TMP_0; label_4747:; if (!(ep32 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4764:; p32_new = node3____CPAchecker_TMP_1; label_4757:; if (!(ep34 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4774:; p34_new = node3____CPAchecker_TMP_2; label_4776:; mode3 = 1; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { return __return_main; } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_4794:; p41_new = node4____CPAchecker_TMP_0; label_4787:; if (!(ep42 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4804:; p42_new = node4____CPAchecker_TMP_1; label_4797:; if (!(ep43 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4814:; p43_new = node4____CPAchecker_TMP_2; label_4816:; mode4 = 1; 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) { return __return_main; } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { if (((int)r1) < 3) { if (((int)r1) >= 3) { return __return_main; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { if (((int)r1) < 3) { check__tmp = 1; __return_4872 = check__tmp; main__c1 = __return_4872; { _Bool __tmp_1; __tmp_1 = main__c1; _Bool assert__arg; assert__arg = __tmp_1; if (assert__arg == 0) { return __return_main; } else { { _Bool node1__newmax; node1__newmax = 0; if (!(mode1 == 0)) { if (r1 == 255) { return __return_main; } else { r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_4888:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_4896:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_4904:; newmax1 = node1__newmax; if (((int)r1) == 3) { return __return_main; } else { mode1 = 0; { _Bool node2__newmax; node2__newmax = 0; if (!(mode2 == 0)) { if (r2 == 255) { return __return_main; } else { r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_4925:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_4933:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_4941:; newmax2 = node2__newmax; if (((int)r2) == 3) { return __return_main; } else { mode2 = 0; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_4962:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_4970:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_4978:; newmax3 = node3__newmax; if (((int)r3) == 3) { return __return_main; } else { mode3 = 0; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_4999:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5007:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5015:; newmax4 = node4__newmax; if (((int)r4) == 3) { return __return_main; } else { mode4 = 0; 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) { return __return_main; } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { if (((int)r1) < 3) { if (((int)r1) >= 3) { return __return_main; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { if (((int)r1) < 3) { check__tmp = 1; __return_5080 = check__tmp; main__c1 = __return_5080; { _Bool __tmp_2; __tmp_2 = main__c1; _Bool assert__arg; assert__arg = __tmp_2; if (assert__arg == 0) { return __return_main; } else { { _Bool node1__newmax; node1__newmax = 0; if (!(mode1 == 0)) { return __return_main; } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_5102:; p12_new = node1____CPAchecker_TMP_0; label_5095:; if (!(ep13 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5112:; p13_new = node1____CPAchecker_TMP_1; label_5105:; if (!(ep14 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5122:; p14_new = node1____CPAchecker_TMP_2; label_5124:; mode1 = 1; { _Bool node2__newmax; node2__newmax = 0; if (!(mode2 == 0)) { return __return_main; } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_5142:; p21_new = node2____CPAchecker_TMP_0; label_5135:; if (!(ep23 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5152:; p23_new = node2____CPAchecker_TMP_1; label_5145:; if (!(ep24 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5162:; p24_new = node2____CPAchecker_TMP_2; label_5164:; mode2 = 1; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { return __return_main; } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_5182:; p31_new = node3____CPAchecker_TMP_0; label_5175:; if (!(ep32 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5192:; p32_new = node3____CPAchecker_TMP_1; label_5185:; if (!(ep34 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5202:; p34_new = node3____CPAchecker_TMP_2; label_5204:; mode3 = 1; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { return __return_main; } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_5222:; p41_new = node4____CPAchecker_TMP_0; label_5215:; if (!(ep42 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5232:; p42_new = node4____CPAchecker_TMP_1; label_5225:; if (!(ep43 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5242:; p43_new = node4____CPAchecker_TMP_2; label_5244:; mode4 = 1; 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) { return __return_main; } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { if (((int)r1) < 3) { if (((int)r1) >= 3) { return __return_main; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { if (((int)r1) < 3) { check__tmp = 1; __return_5300 = check__tmp; main__c1 = __return_5300; { _Bool __tmp_3; __tmp_3 = main__c1; _Bool assert__arg; assert__arg = __tmp_3; if (assert__arg == 0) { return __return_main; } else { { _Bool node1__newmax; node1__newmax = 0; if (!(mode1 == 0)) { if (r1 == 255) { return __return_main; } else { r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5316:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5324:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5332:; newmax1 = node1__newmax; if (((int)r1) == 3) { return __return_main; } else { mode1 = 0; { _Bool node2__newmax; node2__newmax = 0; if (!(mode2 == 0)) { if (r2 == 255) { return __return_main; } else { r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5353:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5361:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5369:; newmax2 = node2__newmax; if (((int)r2) == 3) { return __return_main; } else { mode2 = 0; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5390:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5398:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5406:; newmax3 = node3__newmax; if (((int)r3) == 3) { return __return_main; } else { mode3 = 0; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5427:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5435:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5443:; newmax4 = node4__newmax; if (((int)r4) == 3) { return __return_main; } else { mode4 = 0; 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) { return __return_main; } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { if (((int)r1) < 3) { if (((int)r1) >= 3) { return __return_main; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { if (((int)r1) < 3) { check__tmp = 1; __return_5508 = check__tmp; main__c1 = __return_5508; { _Bool __tmp_4; __tmp_4 = main__c1; _Bool assert__arg; assert__arg = __tmp_4; if (assert__arg == 0) { return __return_main; } else { { _Bool node1__newmax; node1__newmax = 0; if (!(mode1 == 0)) { return __return_main; } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_5530:; p12_new = node1____CPAchecker_TMP_0; label_5523:; if (!(ep13 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5540:; p13_new = node1____CPAchecker_TMP_1; label_5533:; if (!(ep14 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5550:; p14_new = node1____CPAchecker_TMP_2; label_5552:; mode1 = 1; { _Bool node2__newmax; node2__newmax = 0; if (!(mode2 == 0)) { return __return_main; } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_5570:; p21_new = node2____CPAchecker_TMP_0; label_5563:; if (!(ep23 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5580:; p23_new = node2____CPAchecker_TMP_1; label_5573:; if (!(ep24 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5590:; p24_new = node2____CPAchecker_TMP_2; label_5592:; mode2 = 1; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { return __return_main; } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_5610:; p31_new = node3____CPAchecker_TMP_0; label_5603:; if (!(ep32 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5620:; p32_new = node3____CPAchecker_TMP_1; label_5613:; if (!(ep34 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5630:; p34_new = node3____CPAchecker_TMP_2; label_5632:; mode3 = 1; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { return __return_main; } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_5650:; p41_new = node4____CPAchecker_TMP_0; label_5643:; if (!(ep42 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5660:; p42_new = node4____CPAchecker_TMP_1; label_5653:; if (!(ep43 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5670:; p43_new = node4____CPAchecker_TMP_2; label_5672:; mode4 = 1; 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) { return __return_main; } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { if (((int)r1) < 3) { if (((int)r1) >= 3) { return __return_main; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { if (((int)r1) < 3) { check__tmp = 1; __return_5728 = check__tmp; main__c1 = __return_5728; { _Bool __tmp_5; __tmp_5 = main__c1; _Bool assert__arg; assert__arg = __tmp_5; if (assert__arg == 0) { return __return_main; } else { { _Bool node1__newmax; node1__newmax = 0; if (!(mode1 == 0)) { if (r1 == 255) { return __return_main; } else { r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5744:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5752:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5760:; newmax1 = node1__newmax; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5773:; mode1 = 0; { _Bool node2__newmax; node2__newmax = 0; if (!(mode2 == 0)) { if (r2 == 255) { return __return_main; } else { r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5785:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5793:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5801:; newmax2 = node2__newmax; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5814:; mode2 = 0; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5826:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5834:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5842:; newmax3 = node3__newmax; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5855:; mode3 = 0; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5867:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5875:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5883:; newmax4 = node4__newmax; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5896:; mode4 = 0; 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) { if (((int)r1) < 3) { return __return_main; } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { if (((int)r1) >= 3) { label_6355:; if (((int)r1) < 3) { check__tmp = 1; label_6361:; label_6354:; label_5938:; label_5944:; __return_5945 = check__tmp; main__c1 = __return_5945; label_5946:; { _Bool __tmp_6; __tmp_6 = main__c1; _Bool assert__arg; assert__arg = __tmp_6; if (assert__arg == 0) { {reach_error();} return __return_main; } else { { _Bool node1__newmax; node1__newmax = 0; if (!(mode1 == 0)) { if (r1 == 255) { r1 = 3; label_5962:; r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5964:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5972:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5980:; newmax1 = node1__newmax; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5990:; mode1 = 0; label_5992:; { _Bool node2__newmax; node2__newmax = 0; if (!(mode2 == 0)) { if (r2 == 255) { r2 = 3; label_6002:; r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_6004:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_6012:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_6020:; newmax2 = node2__newmax; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_6030:; mode2 = 0; label_6032:; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { if (r3 == 255) { r3 = 3; label_6042:; r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6044:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6052:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6060:; newmax3 = node3__newmax; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_6070:; mode3 = 0; label_6072:; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { if (r4 == 255) { r4 = 3; label_6082:; r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6084:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6092:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6100:; newmax4 = node4__newmax; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_6110:; mode4 = 0; label_6112:; 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_6169:; if (((int)r1) < 3) { label_6176:; if (((int)r1) >= 3) { label_6183:; if (((int)r1) < 3) { check__tmp = 1; label_6189:; label_6182:; label_6175:; label_6168:; label_6162:; label_6158:; label_6154:; label_6150:; label_6145:; __return_6146 = check__tmp; main__c1 = __return_6146; goto label_5946; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6189; } else { check__tmp = 0; goto label_6189; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6183; } else { check__tmp = 0; goto label_6182; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_6176; } else { check__tmp = 0; goto label_6175; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_6169; } else { check__tmp = 0; goto label_6168; } } } else { check__tmp = 0; goto label_6162; } } else { check__tmp = 0; goto label_6158; } } else { check__tmp = 0; goto label_6154; } } else { check__tmp = 0; goto label_6150; } } else { check__tmp = 0; goto label_6145; } } } else { nl4 = 1; goto label_6110; } } else { goto label_6110; } } else { goto label_6100; } } else { goto label_6100; } } else { goto label_6092; } } else { goto label_6092; } } else { goto label_6084; } } else { goto label_6084; } } else { goto label_6082; } } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_6207:; p41_new = node4____CPAchecker_TMP_0; label_6200:; if (!(ep42 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_6217:; p42_new = node4____CPAchecker_TMP_1; label_6210:; if (!(ep43 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_6227:; p43_new = node4____CPAchecker_TMP_2; label_6198:; mode4 = 1; goto label_6112; } else { label_6226:; node4____CPAchecker_TMP_2 = p43_new; goto label_6227; } } else { goto label_6226; } } else { goto label_6198; } } else { goto label_6198; } } else { label_6216:; node4____CPAchecker_TMP_1 = p42_new; goto label_6217; } } else { goto label_6216; } } else { goto label_6210; } } else { goto label_6210; } } else { label_6206:; node4____CPAchecker_TMP_0 = p41_new; goto label_6207; } } else { goto label_6206; } } else { goto label_6200; } } else { goto label_6200; } } else { goto label_6198; } } } } else { nl3 = 1; goto label_6070; } } else { goto label_6070; } } else { goto label_6060; } } else { goto label_6060; } } else { goto label_6052; } } else { goto label_6052; } } else { goto label_6044; } } else { goto label_6044; } } else { goto label_6042; } } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_6245:; p31_new = node3____CPAchecker_TMP_0; label_6238:; if (!(ep32 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_6255:; p32_new = node3____CPAchecker_TMP_1; label_6248:; if (!(ep34 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_6265:; p34_new = node3____CPAchecker_TMP_2; label_6236:; mode3 = 1; goto label_6072; } else { label_6264:; node3____CPAchecker_TMP_2 = p34_new; goto label_6265; } } else { goto label_6264; } } else { goto label_6236; } } else { goto label_6236; } } else { label_6254:; node3____CPAchecker_TMP_1 = p32_new; goto label_6255; } } else { goto label_6254; } } else { goto label_6248; } } else { goto label_6248; } } else { label_6244:; node3____CPAchecker_TMP_0 = p31_new; goto label_6245; } } else { goto label_6244; } } else { goto label_6238; } } else { goto label_6238; } } else { goto label_6236; } } } } else { nl2 = 1; goto label_6030; } } else { goto label_6030; } } else { goto label_6020; } } else { goto label_6020; } } else { goto label_6012; } } else { goto label_6012; } } else { goto label_6004; } } else { goto label_6004; } } else { goto label_6002; } } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_6283:; p21_new = node2____CPAchecker_TMP_0; label_6276:; if (!(ep23 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_6293:; p23_new = node2____CPAchecker_TMP_1; label_6286:; if (!(ep24 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_6303:; p24_new = node2____CPAchecker_TMP_2; label_6274:; mode2 = 1; goto label_6032; } else { label_6302:; node2____CPAchecker_TMP_2 = p24_new; goto label_6303; } } else { goto label_6302; } } else { goto label_6274; } } else { goto label_6274; } } else { label_6292:; node2____CPAchecker_TMP_1 = p23_new; goto label_6293; } } else { goto label_6292; } } else { goto label_6286; } } else { goto label_6286; } } else { label_6282:; node2____CPAchecker_TMP_0 = p21_new; goto label_6283; } } else { goto label_6282; } } else { goto label_6276; } } else { goto label_6276; } } else { goto label_6274; } } } } else { nl1 = 1; goto label_5990; } } else { goto label_5990; } } else { goto label_5980; } } else { goto label_5980; } } else { goto label_5972; } } else { goto label_5972; } } else { goto label_5964; } } else { goto label_5964; } } else { goto label_5962; } } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_6321:; p12_new = node1____CPAchecker_TMP_0; label_6314:; if (!(ep13 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_6331:; p13_new = node1____CPAchecker_TMP_1; label_6324:; if (!(ep14 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_6341:; p14_new = node1____CPAchecker_TMP_2; label_6312:; mode1 = 1; goto label_5992; } else { label_6340:; node1____CPAchecker_TMP_2 = p14_new; goto label_6341; } } else { goto label_6340; } } else { goto label_6312; } } else { goto label_6312; } } else { label_6330:; node1____CPAchecker_TMP_1 = p13_new; goto label_6331; } } else { goto label_6330; } } else { goto label_6324; } } else { goto label_6324; } } else { label_6320:; node1____CPAchecker_TMP_0 = p12_new; goto label_6321; } } else { goto label_6320; } } else { goto label_6314; } } else { goto label_6314; } } else { goto label_6312; } } } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6361; } else { check__tmp = 0; goto label_6361; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6355; } else { check__tmp = 0; goto label_6354; } } } else { check__tmp = 0; goto label_5938; } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { check__tmp = 0; goto label_5944; } } } else { nl4 = 1; goto label_5896; } } else { return __return_main; } } else { goto label_5883; } } else { goto label_5883; } } else { goto label_5875; } } else { goto label_5875; } } else { goto label_5867; } } else { goto label_5867; } } } else { return __return_main; } } } else { nl3 = 1; goto label_5855; } } else { return __return_main; } } else { goto label_5842; } } else { goto label_5842; } } else { goto label_5834; } } else { goto label_5834; } } else { goto label_5826; } } else { goto label_5826; } } } else { return __return_main; } } } else { nl2 = 1; goto label_5814; } } else { return __return_main; } } else { goto label_5801; } } else { goto label_5801; } } else { goto label_5793; } } else { goto label_5793; } } else { goto label_5785; } } else { goto label_5785; } } } else { return __return_main; } } } else { nl1 = 1; goto label_5773; } } else { return __return_main; } } else { goto label_5760; } } else { goto label_5760; } } else { goto label_5752; } } else { goto label_5752; } } else { goto label_5744; } } else { goto label_5744; } } } else { return __return_main; } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } } else { label_5669:; node4____CPAchecker_TMP_2 = p43_new; goto label_5670; } } else { goto label_5669; } } else { goto label_5672; } } else { goto label_5672; } } else { label_5659:; node4____CPAchecker_TMP_1 = p42_new; goto label_5660; } } else { goto label_5659; } } else { goto label_5653; } } else { goto label_5653; } } else { label_5649:; node4____CPAchecker_TMP_0 = p41_new; goto label_5650; } } else { goto label_5649; } } else { goto label_5643; } } else { goto label_5643; } } else { return __return_main; } } } } else { label_5629:; node3____CPAchecker_TMP_2 = p34_new; goto label_5630; } } else { goto label_5629; } } else { goto label_5632; } } else { goto label_5632; } } else { label_5619:; node3____CPAchecker_TMP_1 = p32_new; goto label_5620; } } else { goto label_5619; } } else { goto label_5613; } } else { goto label_5613; } } else { label_5609:; node3____CPAchecker_TMP_0 = p31_new; goto label_5610; } } else { goto label_5609; } } else { goto label_5603; } } else { goto label_5603; } } else { return __return_main; } } } } else { label_5589:; node2____CPAchecker_TMP_2 = p24_new; goto label_5590; } } else { goto label_5589; } } else { goto label_5592; } } else { goto label_5592; } } else { label_5579:; node2____CPAchecker_TMP_1 = p23_new; goto label_5580; } } else { goto label_5579; } } else { goto label_5573; } } else { goto label_5573; } } else { label_5569:; node2____CPAchecker_TMP_0 = p21_new; goto label_5570; } } else { goto label_5569; } } else { goto label_5563; } } else { goto label_5563; } } else { return __return_main; } } } } else { label_5549:; node1____CPAchecker_TMP_2 = p14_new; goto label_5550; } } else { goto label_5549; } } else { goto label_5552; } } else { goto label_5552; } } else { label_5539:; node1____CPAchecker_TMP_1 = p13_new; goto label_5540; } } else { goto label_5539; } } else { goto label_5533; } } else { goto label_5533; } } else { label_5529:; node1____CPAchecker_TMP_0 = p12_new; goto label_5530; } } else { goto label_5529; } } else { goto label_5523; } } else { goto label_5523; } } else { return __return_main; } } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } } } else { goto label_5443; } } else { goto label_5443; } } else { goto label_5435; } } else { goto label_5435; } } else { goto label_5427; } } else { goto label_5427; } } } else { return __return_main; } } } } else { goto label_5406; } } else { goto label_5406; } } else { goto label_5398; } } else { goto label_5398; } } else { goto label_5390; } } else { goto label_5390; } } } else { return __return_main; } } } } else { goto label_5369; } } else { goto label_5369; } } else { goto label_5361; } } else { goto label_5361; } } else { goto label_5353; } } else { goto label_5353; } } } else { return __return_main; } } } } else { goto label_5332; } } else { goto label_5332; } } else { goto label_5324; } } else { goto label_5324; } } else { goto label_5316; } } else { goto label_5316; } } } else { return __return_main; } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } } else { label_5241:; node4____CPAchecker_TMP_2 = p43_new; goto label_5242; } } else { goto label_5241; } } else { goto label_5244; } } else { goto label_5244; } } else { label_5231:; node4____CPAchecker_TMP_1 = p42_new; goto label_5232; } } else { goto label_5231; } } else { goto label_5225; } } else { goto label_5225; } } else { label_5221:; node4____CPAchecker_TMP_0 = p41_new; goto label_5222; } } else { goto label_5221; } } else { goto label_5215; } } else { goto label_5215; } } else { return __return_main; } } } } else { label_5201:; node3____CPAchecker_TMP_2 = p34_new; goto label_5202; } } else { goto label_5201; } } else { goto label_5204; } } else { goto label_5204; } } else { label_5191:; node3____CPAchecker_TMP_1 = p32_new; goto label_5192; } } else { goto label_5191; } } else { goto label_5185; } } else { goto label_5185; } } else { label_5181:; node3____CPAchecker_TMP_0 = p31_new; goto label_5182; } } else { goto label_5181; } } else { goto label_5175; } } else { goto label_5175; } } else { return __return_main; } } } } else { label_5161:; node2____CPAchecker_TMP_2 = p24_new; goto label_5162; } } else { goto label_5161; } } else { goto label_5164; } } else { goto label_5164; } } else { label_5151:; node2____CPAchecker_TMP_1 = p23_new; goto label_5152; } } else { goto label_5151; } } else { goto label_5145; } } else { goto label_5145; } } else { label_5141:; node2____CPAchecker_TMP_0 = p21_new; goto label_5142; } } else { goto label_5141; } } else { goto label_5135; } } else { goto label_5135; } } else { return __return_main; } } } } else { label_5121:; node1____CPAchecker_TMP_2 = p14_new; goto label_5122; } } else { goto label_5121; } } else { goto label_5124; } } else { goto label_5124; } } else { label_5111:; node1____CPAchecker_TMP_1 = p13_new; goto label_5112; } } else { goto label_5111; } } else { goto label_5105; } } else { goto label_5105; } } else { label_5101:; node1____CPAchecker_TMP_0 = p12_new; goto label_5102; } } else { goto label_5101; } } else { goto label_5095; } } else { goto label_5095; } } else { return __return_main; } } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } } } else { goto label_5015; } } else { goto label_5015; } } else { goto label_5007; } } else { goto label_5007; } } else { goto label_4999; } } else { goto label_4999; } } } else { return __return_main; } } } } else { goto label_4978; } } else { goto label_4978; } } else { goto label_4970; } } else { goto label_4970; } } else { goto label_4962; } } else { goto label_4962; } } } else { return __return_main; } } } } else { goto label_4941; } } else { goto label_4941; } } else { goto label_4933; } } else { goto label_4933; } } else { goto label_4925; } } else { goto label_4925; } } } else { return __return_main; } } } } else { goto label_4904; } } else { goto label_4904; } } else { goto label_4896; } } else { goto label_4896; } } else { goto label_4888; } } else { goto label_4888; } } } else { return __return_main; } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } } else { label_4813:; node4____CPAchecker_TMP_2 = p43_new; goto label_4814; } } else { goto label_4813; } } else { goto label_4816; } } else { goto label_4816; } } else { label_4803:; node4____CPAchecker_TMP_1 = p42_new; goto label_4804; } } else { goto label_4803; } } else { goto label_4797; } } else { goto label_4797; } } else { label_4793:; node4____CPAchecker_TMP_0 = p41_new; goto label_4794; } } else { goto label_4793; } } else { goto label_4787; } } else { goto label_4787; } } else { return __return_main; } } } } else { label_4773:; node3____CPAchecker_TMP_2 = p34_new; goto label_4774; } } else { goto label_4773; } } else { goto label_4776; } } else { goto label_4776; } } else { label_4763:; node3____CPAchecker_TMP_1 = p32_new; goto label_4764; } } else { goto label_4763; } } else { goto label_4757; } } else { goto label_4757; } } else { label_4753:; node3____CPAchecker_TMP_0 = p31_new; goto label_4754; } } else { goto label_4753; } } else { goto label_4747; } } else { goto label_4747; } } else { return __return_main; } } } } else { label_4733:; node2____CPAchecker_TMP_2 = p24_new; goto label_4734; } } else { goto label_4733; } } else { goto label_4736; } } else { goto label_4736; } } else { label_4723:; node2____CPAchecker_TMP_1 = p23_new; goto label_4724; } } else { goto label_4723; } } else { goto label_4717; } } else { goto label_4717; } } else { label_4713:; node2____CPAchecker_TMP_0 = p21_new; goto label_4714; } } else { goto label_4713; } } else { goto label_4707; } } else { goto label_4707; } } else { return __return_main; } } } } else { label_4693:; node1____CPAchecker_TMP_2 = p14_new; goto label_4694; } } else { goto label_4693; } } else { goto label_4696; } } else { goto label_4696; } } else { label_4683:; node1____CPAchecker_TMP_1 = p13_new; goto label_4684; } } else { goto label_4683; } } else { goto label_4677; } } else { goto label_4677; } } else { label_4673:; node1____CPAchecker_TMP_0 = p12_new; goto label_4674; } } else { goto label_4673; } } else { goto label_4667; } } else { goto label_4667; } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { if (!(init__r412 == 0)) { if (!(ep13 == 0)) { init__tmp___22 = 1; goto label_4559; } else { label_6387:; if (!(init__r422 == 0)) { if (!(ep23 == 0)) { init__tmp___22 = 1; label_6393:; goto label_4559; } else { init__tmp___22 = 0; goto label_6393; } } else { init__tmp___22 = 0; goto label_4559; } } } else { goto label_6387; } } } else { if (!(init__r412 == 0)) { if (!(ep12 == 0)) { init__tmp___21 = 1; goto label_4554; } else { label_6402:; if (!(init__r432 == 0)) { if (!(ep32 == 0)) { init__tmp___21 = 1; label_6408:; goto label_4554; } else { init__tmp___21 = 0; goto label_6408; } } else { init__tmp___21 = 0; goto label_4554; } } } else { goto label_6402; } } } else { if (!(init__r422 == 0)) { if (!(ep21 == 0)) { init__tmp___20 = 1; goto label_4549; } else { label_6417:; if (!(init__r432 == 0)) { if (!(ep31 == 0)) { init__tmp___20 = 1; label_6423:; goto label_4549; } else { init__tmp___20 = 0; goto label_6423; } } else { init__tmp___20 = 0; goto label_4549; } } } else { goto label_6417; } } } else { if (!(init__r312 == 0)) { if (!(ep14 == 0)) { init__tmp___19 = 1; goto label_4544; } else { label_6432:; if (!(init__r322 == 0)) { if (!(ep24 == 0)) { init__tmp___19 = 1; label_6438:; goto label_4544; } else { init__tmp___19 = 0; goto label_6438; } } else { init__tmp___19 = 0; goto label_4544; } } } else { goto label_6432; } } } else { if (!(init__r312 == 0)) { if (!(ep12 == 0)) { init__tmp___18 = 1; goto label_4539; } else { label_6447:; if (!(init__r342 == 0)) { if (!(ep42 == 0)) { init__tmp___18 = 1; label_6453:; goto label_4539; } else { init__tmp___18 = 0; goto label_6453; } } else { init__tmp___18 = 0; goto label_4539; } } } else { goto label_6447; } } } else { if (!(init__r322 == 0)) { if (!(ep21 == 0)) { init__tmp___17 = 1; goto label_4534; } else { label_6462:; if (!(init__r342 == 0)) { if (!(ep41 == 0)) { init__tmp___17 = 1; label_6468:; goto label_4534; } else { init__tmp___17 = 0; goto label_6468; } } else { init__tmp___17 = 0; goto label_4534; } } } else { goto label_6462; } } } else { if (!(init__r212 == 0)) { if (!(ep14 == 0)) { init__tmp___16 = 1; goto label_4529; } else { label_6477:; if (!(init__r232 == 0)) { if (!(ep34 == 0)) { init__tmp___16 = 1; label_6483:; goto label_4529; } else { init__tmp___16 = 0; goto label_6483; } } else { init__tmp___16 = 0; goto label_4529; } } } else { goto label_6477; } } } else { if (!(init__r212 == 0)) { if (!(ep13 == 0)) { init__tmp___15 = 1; goto label_4524; } else { label_6492:; if (!(init__r242 == 0)) { if (!(ep43 == 0)) { init__tmp___15 = 1; label_6498:; goto label_4524; } else { init__tmp___15 = 0; goto label_6498; } } else { init__tmp___15 = 0; goto label_4524; } } } else { goto label_6492; } } } else { if (!(init__r232 == 0)) { if (!(ep31 == 0)) { init__tmp___14 = 1; goto label_4519; } else { label_6507:; if (!(init__r242 == 0)) { if (!(ep41 == 0)) { init__tmp___14 = 1; label_6513:; goto label_4519; } else { init__tmp___14 = 0; goto label_6513; } } else { init__tmp___14 = 0; goto label_4519; } } } else { goto label_6507; } } } else { if (!(init__r122 == 0)) { if (!(ep24 == 0)) { init__tmp___13 = 1; goto label_4514; } else { label_6522:; if (!(init__r132 == 0)) { if (!(ep34 == 0)) { init__tmp___13 = 1; label_6528:; goto label_4514; } else { init__tmp___13 = 0; goto label_6528; } } else { init__tmp___13 = 0; goto label_4514; } } } else { goto label_6522; } } } else { if (!(init__r122 == 0)) { if (!(ep23 == 0)) { init__tmp___12 = 1; goto label_4509; } else { label_6537:; if (!(init__r142 == 0)) { if (!(ep43 == 0)) { init__tmp___12 = 1; label_6543:; goto label_4509; } else { init__tmp___12 = 0; goto label_6543; } } else { init__tmp___12 = 0; goto label_4509; } } } else { goto label_6537; } } } else { if (!(init__r132 == 0)) { if (!(ep32 == 0)) { init__tmp___11 = 1; goto label_4504; } else { label_6552:; if (!(init__r142 == 0)) { if (!(ep42 == 0)) { init__tmp___11 = 1; label_6558:; goto label_4504; } else { init__tmp___11 = 0; goto label_6558; } } else { init__tmp___11 = 0; goto label_4504; } } } else { goto label_6552; } } } else { if (!(init__r411 == 0)) { if (!(ep13 == 0)) { init__tmp___10 = 1; goto label_4499; } else { label_6567:; if (!(init__r421 == 0)) { if (!(ep23 == 0)) { init__tmp___10 = 1; label_6573:; goto label_4499; } else { init__tmp___10 = 0; goto label_6573; } } else { init__tmp___10 = 0; goto label_4499; } } } else { goto label_6567; } } } else { if (!(init__r411 == 0)) { if (!(ep12 == 0)) { init__tmp___9 = 1; goto label_4494; } else { label_6582:; if (!(init__r431 == 0)) { if (!(ep32 == 0)) { init__tmp___9 = 1; label_6588:; goto label_4494; } else { init__tmp___9 = 0; goto label_6588; } } else { init__tmp___9 = 0; goto label_4494; } } } else { goto label_6582; } } } else { if (!(init__r421 == 0)) { if (!(ep21 == 0)) { init__tmp___8 = 1; goto label_4489; } else { label_6597:; if (!(init__r431 == 0)) { if (!(ep31 == 0)) { init__tmp___8 = 1; label_6603:; goto label_4489; } else { init__tmp___8 = 0; goto label_6603; } } else { init__tmp___8 = 0; goto label_4489; } } } else { goto label_6597; } } } else { if (!(init__r311 == 0)) { if (!(ep14 == 0)) { init__tmp___7 = 1; goto label_4484; } else { label_6612:; if (!(init__r321 == 0)) { if (!(ep24 == 0)) { init__tmp___7 = 1; label_6618:; goto label_4484; } else { init__tmp___7 = 0; goto label_6618; } } else { init__tmp___7 = 0; goto label_4484; } } } else { goto label_6612; } } } else { if (!(init__r311 == 0)) { if (!(ep12 == 0)) { init__tmp___6 = 1; goto label_4479; } else { label_6627:; if (!(init__r341 == 0)) { if (!(ep42 == 0)) { init__tmp___6 = 1; label_6633:; goto label_4479; } else { init__tmp___6 = 0; goto label_6633; } } else { init__tmp___6 = 0; goto label_4479; } } } else { goto label_6627; } } } else { if (!(init__r321 == 0)) { if (!(ep21 == 0)) { init__tmp___5 = 1; goto label_4474; } else { label_6642:; if (!(init__r341 == 0)) { if (!(ep41 == 0)) { init__tmp___5 = 1; label_6648:; goto label_4474; } else { init__tmp___5 = 0; goto label_6648; } } else { init__tmp___5 = 0; goto label_4474; } } } else { goto label_6642; } } } else { if (!(init__r211 == 0)) { if (!(ep14 == 0)) { init__tmp___4 = 1; goto label_4469; } else { label_6657:; if (!(init__r231 == 0)) { if (!(ep34 == 0)) { init__tmp___4 = 1; label_6663:; goto label_4469; } else { init__tmp___4 = 0; goto label_6663; } } else { init__tmp___4 = 0; goto label_4469; } } } else { goto label_6657; } } } else { if (!(init__r211 == 0)) { if (!(ep13 == 0)) { init__tmp___3 = 1; goto label_4464; } else { label_6672:; if (!(init__r241 == 0)) { if (!(ep43 == 0)) { init__tmp___3 = 1; label_6678:; goto label_4464; } else { init__tmp___3 = 0; goto label_6678; } } else { init__tmp___3 = 0; goto label_4464; } } } else { goto label_6672; } } } else { if (!(init__r231 == 0)) { if (!(ep31 == 0)) { init__tmp___2 = 1; goto label_4459; } else { label_6687:; if (!(init__r241 == 0)) { if (!(ep41 == 0)) { init__tmp___2 = 1; label_6693:; goto label_4459; } else { init__tmp___2 = 0; goto label_6693; } } else { init__tmp___2 = 0; goto label_4459; } } } else { goto label_6687; } } } else { if (!(init__r121 == 0)) { if (!(ep24 == 0)) { init__tmp___1 = 1; goto label_4454; } else { label_6702:; if (!(init__r131 == 0)) { if (!(ep34 == 0)) { init__tmp___1 = 1; label_6708:; goto label_4454; } else { init__tmp___1 = 0; goto label_6708; } } else { init__tmp___1 = 0; goto label_4454; } } } else { goto label_6702; } } } else { if (!(init__r121 == 0)) { if (!(ep23 == 0)) { init__tmp___0 = 1; goto label_4449; } else { label_6717:; if (!(init__r141 == 0)) { if (!(ep43 == 0)) { init__tmp___0 = 1; label_6723:; goto label_4449; } else { init__tmp___0 = 0; goto label_6723; } } else { init__tmp___0 = 0; goto label_4449; } } } else { goto label_6717; } } } else { if (!(init__r131 == 0)) { if (!(ep32 == 0)) { init__tmp = 1; goto label_4444; } else { label_6732:; if (!(init__r141 == 0)) { if (!(ep42 == 0)) { init__tmp = 1; label_6738:; goto label_4444; } else { init__tmp = 0; goto label_6738; } } else { init__tmp = 0; goto label_4444; } } } else { goto label_6732; } } } }