// 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.4.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_4635; int __return_4877; int __return_5085; int __return_5305; int __return_5513; int __return_5703; int __return_5920; int __return_6121; 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_4425:; init__r122 = (_Bool)init__tmp; if (!(init__r131 == 0)) { init__tmp___0 = 1; label_4430:; init__r132 = (_Bool)init__tmp___0; if (!(init__r141 == 0)) { init__tmp___1 = 1; label_4435:; init__r142 = (_Bool)init__tmp___1; if (!(init__r211 == 0)) { init__tmp___2 = 1; label_4440:; init__r212 = (_Bool)init__tmp___2; if (!(init__r231 == 0)) { init__tmp___3 = 1; label_4445:; init__r232 = (_Bool)init__tmp___3; if (!(init__r241 == 0)) { init__tmp___4 = 1; label_4450:; init__r242 = (_Bool)init__tmp___4; if (!(init__r311 == 0)) { init__tmp___5 = 1; label_4455:; init__r312 = (_Bool)init__tmp___5; if (!(init__r321 == 0)) { init__tmp___6 = 1; label_4460:; init__r322 = (_Bool)init__tmp___6; if (!(init__r341 == 0)) { init__tmp___7 = 1; label_4465:; init__r342 = (_Bool)init__tmp___7; if (!(init__r411 == 0)) { init__tmp___8 = 1; label_4470:; init__r412 = (_Bool)init__tmp___8; if (!(init__r421 == 0)) { init__tmp___9 = 1; label_4475:; init__r422 = (_Bool)init__tmp___9; if (!(init__r431 == 0)) { init__tmp___10 = 1; label_4480:; init__r432 = (_Bool)init__tmp___10; if (!(init__r122 == 0)) { init__tmp___11 = 1; label_4485:; init__r123 = (_Bool)init__tmp___11; if (!(init__r132 == 0)) { init__tmp___12 = 1; label_4490:; init__r133 = (_Bool)init__tmp___12; if (!(init__r142 == 0)) { init__tmp___13 = 1; label_4495:; init__r143 = (_Bool)init__tmp___13; if (!(init__r212 == 0)) { init__tmp___14 = 1; label_4500:; init__r213 = (_Bool)init__tmp___14; if (!(init__r232 == 0)) { init__tmp___15 = 1; label_4505:; init__r233 = (_Bool)init__tmp___15; if (!(init__r242 == 0)) { init__tmp___16 = 1; label_4510:; init__r243 = (_Bool)init__tmp___16; if (!(init__r312 == 0)) { init__tmp___17 = 1; label_4515:; init__r313 = (_Bool)init__tmp___17; if (!(init__r322 == 0)) { init__tmp___18 = 1; label_4520:; init__r323 = (_Bool)init__tmp___18; if (!(init__r342 == 0)) { init__tmp___19 = 1; label_4525:; init__r343 = (_Bool)init__tmp___19; if (!(init__r412 == 0)) { init__tmp___20 = 1; label_4530:; init__r413 = (_Bool)init__tmp___20; if (!(init__r422 == 0)) { init__tmp___21 = 1; label_4535:; init__r423 = (_Bool)init__tmp___21; if (!(init__r432 == 0)) { init__tmp___22 = 1; label_4540:; 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) { if (!(newmax1 == 0)) { if (!(newmax2 == 0)) { if (!(newmax3 == 0)) { if (!(newmax4 == 0)) { init__tmp___23 = 1; __return_4635 = init__tmp___23; main__i2 = __return_4635; 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) < 2) { if (!(ep12 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_4679:; p12_new = node1____CPAchecker_TMP_0; label_4672:; if (!(ep13 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4689:; p13_new = node1____CPAchecker_TMP_1; label_4682:; if (!(ep14 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4699:; p14_new = node1____CPAchecker_TMP_2; label_4701:; 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_4719:; p21_new = node2____CPAchecker_TMP_0; label_4712:; if (!(ep23 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4729:; p23_new = node2____CPAchecker_TMP_1; label_4722:; if (!(ep24 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4739:; p24_new = node2____CPAchecker_TMP_2; label_4741:; 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_4759:; p31_new = node3____CPAchecker_TMP_0; label_4752:; if (!(ep32 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4769:; p32_new = node3____CPAchecker_TMP_1; label_4762:; if (!(ep34 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4779:; p34_new = node3____CPAchecker_TMP_2; label_4781:; 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_4799:; p41_new = node4____CPAchecker_TMP_0; label_4792:; if (!(ep42 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4809:; p42_new = node4____CPAchecker_TMP_1; label_4802:; if (!(ep43 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4819:; p43_new = node4____CPAchecker_TMP_2; label_4821:; 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_4877 = check__tmp; main__c1 = __return_4877; { _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_4893:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_4901:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_4909:; 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_4930:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_4938:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_4946:; 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_4967:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_4975:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_4983:; 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_5004:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5012:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5020:; 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_5085 = check__tmp; main__c1 = __return_5085; { _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) < 2) { if (!(ep12 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_5107:; p12_new = node1____CPAchecker_TMP_0; label_5100:; if (!(ep13 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5117:; p13_new = node1____CPAchecker_TMP_1; label_5110:; if (!(ep14 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5127:; p14_new = node1____CPAchecker_TMP_2; label_5129:; 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_5147:; p21_new = node2____CPAchecker_TMP_0; label_5140:; if (!(ep23 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5157:; p23_new = node2____CPAchecker_TMP_1; label_5150:; if (!(ep24 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5167:; p24_new = node2____CPAchecker_TMP_2; label_5169:; 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_5187:; p31_new = node3____CPAchecker_TMP_0; label_5180:; if (!(ep32 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5197:; p32_new = node3____CPAchecker_TMP_1; label_5190:; if (!(ep34 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5207:; p34_new = node3____CPAchecker_TMP_2; label_5209:; 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_5227:; p41_new = node4____CPAchecker_TMP_0; label_5220:; if (!(ep42 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5237:; p42_new = node4____CPAchecker_TMP_1; label_5230:; if (!(ep43 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5247:; p43_new = node4____CPAchecker_TMP_2; label_5249:; 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_5305 = check__tmp; main__c1 = __return_5305; { _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_5321:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5329:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5337:; 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_5358:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5366:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5374:; 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_5395:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5403:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5411:; 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_5432:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5440:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5448:; 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_5513 = check__tmp; main__c1 = __return_5513; { _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) < 2) { return __return_main; } else { 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_5545:; p21_new = node2____CPAchecker_TMP_0; label_5538:; if (!(ep23 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5555:; p23_new = node2____CPAchecker_TMP_1; label_5548:; if (!(ep24 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5565:; p24_new = node2____CPAchecker_TMP_2; label_5567:; 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_5585:; p31_new = node3____CPAchecker_TMP_0; label_5578:; if (!(ep32 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5595:; p32_new = node3____CPAchecker_TMP_1; label_5588:; if (!(ep34 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5605:; p34_new = node3____CPAchecker_TMP_2; label_5607:; 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_5625:; p41_new = node4____CPAchecker_TMP_0; label_5618:; if (!(ep42 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5635:; p42_new = node4____CPAchecker_TMP_1; label_5628:; if (!(ep43 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5645:; p43_new = node4____CPAchecker_TMP_2; label_5647:; 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_5703 = check__tmp; main__c1 = __return_5703; { _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_5719:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5727:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5735:; newmax1 = node1__newmax; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5748:; 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_5760:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5768:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5776:; newmax2 = node2__newmax; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5789:; 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_5801:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5809:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5817:; newmax3 = node3__newmax; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5830:; 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_5842:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5850:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5858:; newmax4 = node4__newmax; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5871:; 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_6330:; if (((int)r1) < 3) { check__tmp = 1; label_6336:; label_6329:; label_5913:; label_5919:; __return_5920 = check__tmp; main__c1 = __return_5920; label_5921:; { _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_5937:; r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5939:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5947:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5955:; newmax1 = node1__newmax; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5965:; mode1 = 0; label_5967:; { _Bool node2__newmax; node2__newmax = 0; if (!(mode2 == 0)) { if (r2 == 255) { r2 = 3; label_5977:; r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5979:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5987:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5995:; newmax2 = node2__newmax; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_6005:; mode2 = 0; label_6007:; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { if (r3 == 255) { r3 = 3; label_6017:; r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6019:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6027:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6035:; newmax3 = node3__newmax; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_6045:; mode3 = 0; label_6047:; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { if (r4 == 255) { r4 = 3; label_6057:; r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6059:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6067:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6075:; newmax4 = node4__newmax; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_6085:; mode4 = 0; label_6087:; 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_6144:; if (((int)r1) < 3) { label_6151:; if (((int)r1) >= 3) { label_6158:; if (((int)r1) < 3) { check__tmp = 1; label_6164:; label_6157:; label_6150:; label_6143:; label_6137:; label_6133:; label_6129:; label_6125:; label_6120:; __return_6121 = check__tmp; main__c1 = __return_6121; goto label_5921; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6164; } else { check__tmp = 0; goto label_6164; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6158; } else { check__tmp = 0; goto label_6157; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_6151; } else { check__tmp = 0; goto label_6150; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_6144; } else { check__tmp = 0; goto label_6143; } } } else { check__tmp = 0; goto label_6137; } } else { check__tmp = 0; goto label_6133; } } else { check__tmp = 0; goto label_6129; } } else { check__tmp = 0; goto label_6125; } } else { check__tmp = 0; goto label_6120; } } } else { nl4 = 1; goto label_6085; } } else { goto label_6085; } } else { goto label_6075; } } else { goto label_6075; } } else { goto label_6067; } } else { goto label_6067; } } else { goto label_6059; } } else { goto label_6059; } } else { goto label_6057; } } 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_6182:; p41_new = node4____CPAchecker_TMP_0; label_6175:; if (!(ep42 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_6192:; p42_new = node4____CPAchecker_TMP_1; label_6185:; if (!(ep43 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_6202:; p43_new = node4____CPAchecker_TMP_2; label_6173:; mode4 = 1; goto label_6087; } else { label_6201:; node4____CPAchecker_TMP_2 = p43_new; goto label_6202; } } else { goto label_6201; } } else { goto label_6173; } } else { goto label_6173; } } else { label_6191:; node4____CPAchecker_TMP_1 = p42_new; goto label_6192; } } else { goto label_6191; } } else { goto label_6185; } } else { goto label_6185; } } else { label_6181:; node4____CPAchecker_TMP_0 = p41_new; goto label_6182; } } else { goto label_6181; } } else { goto label_6175; } } else { goto label_6175; } } else { goto label_6173; } } } } else { nl3 = 1; goto label_6045; } } else { goto label_6045; } } else { goto label_6035; } } else { goto label_6035; } } else { goto label_6027; } } else { goto label_6027; } } else { goto label_6019; } } else { goto label_6019; } } else { goto label_6017; } } 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_6220:; p31_new = node3____CPAchecker_TMP_0; label_6213:; if (!(ep32 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_6230:; p32_new = node3____CPAchecker_TMP_1; label_6223:; if (!(ep34 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_6240:; p34_new = node3____CPAchecker_TMP_2; label_6211:; mode3 = 1; goto label_6047; } else { label_6239:; node3____CPAchecker_TMP_2 = p34_new; goto label_6240; } } else { goto label_6239; } } else { goto label_6211; } } else { goto label_6211; } } else { label_6229:; node3____CPAchecker_TMP_1 = p32_new; goto label_6230; } } else { goto label_6229; } } else { goto label_6223; } } else { goto label_6223; } } else { label_6219:; node3____CPAchecker_TMP_0 = p31_new; goto label_6220; } } else { goto label_6219; } } else { goto label_6213; } } else { goto label_6213; } } else { goto label_6211; } } } } else { nl2 = 1; goto label_6005; } } else { goto label_6005; } } else { goto label_5995; } } else { goto label_5995; } } else { goto label_5987; } } else { goto label_5987; } } else { goto label_5979; } } else { goto label_5979; } } else { goto label_5977; } } 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_6258:; p21_new = node2____CPAchecker_TMP_0; label_6251:; if (!(ep23 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_6268:; p23_new = node2____CPAchecker_TMP_1; label_6261:; if (!(ep24 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_6278:; p24_new = node2____CPAchecker_TMP_2; label_6249:; mode2 = 1; goto label_6007; } else { label_6277:; node2____CPAchecker_TMP_2 = p24_new; goto label_6278; } } else { goto label_6277; } } else { goto label_6249; } } else { goto label_6249; } } else { label_6267:; node2____CPAchecker_TMP_1 = p23_new; goto label_6268; } } else { goto label_6267; } } else { goto label_6261; } } else { goto label_6261; } } else { label_6257:; node2____CPAchecker_TMP_0 = p21_new; goto label_6258; } } else { goto label_6257; } } else { goto label_6251; } } else { goto label_6251; } } else { goto label_6249; } } } } else { nl1 = 1; goto label_5965; } } else { goto label_5965; } } else { goto label_5955; } } else { goto label_5955; } } else { goto label_5947; } } else { goto label_5947; } } else { goto label_5939; } } else { goto label_5939; } } else { goto label_5937; } } else { if (((int)r1) < 2) { if (!(ep12 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_6296:; p12_new = node1____CPAchecker_TMP_0; label_6289:; if (!(ep13 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_6306:; p13_new = node1____CPAchecker_TMP_1; label_6299:; if (!(ep14 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_6316:; p14_new = node1____CPAchecker_TMP_2; label_6287:; mode1 = 1; goto label_5967; } else { label_6315:; node1____CPAchecker_TMP_2 = p14_new; goto label_6316; } } else { goto label_6315; } } else { goto label_6287; } } else { goto label_6287; } } else { label_6305:; node1____CPAchecker_TMP_1 = p13_new; goto label_6306; } } else { goto label_6305; } } else { goto label_6299; } } else { goto label_6299; } } else { label_6295:; node1____CPAchecker_TMP_0 = p12_new; goto label_6296; } } else { goto label_6295; } } else { goto label_6289; } } else { goto label_6289; } } else { goto label_6287; } } } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6336; } else { check__tmp = 0; goto label_6336; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6330; } else { check__tmp = 0; goto label_6329; } } } else { check__tmp = 0; goto label_5913; } } } 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_5919; } } } else { nl4 = 1; goto label_5871; } } else { return __return_main; } } else { goto label_5858; } } else { goto label_5858; } } else { goto label_5850; } } else { goto label_5850; } } else { goto label_5842; } } else { goto label_5842; } } } else { return __return_main; } } } else { nl3 = 1; goto label_5830; } } else { return __return_main; } } else { goto label_5817; } } else { goto label_5817; } } else { goto label_5809; } } else { goto label_5809; } } else { goto label_5801; } } else { goto label_5801; } } } else { return __return_main; } } } else { nl2 = 1; goto label_5789; } } else { return __return_main; } } else { goto label_5776; } } else { goto label_5776; } } else { goto label_5768; } } else { goto label_5768; } } else { goto label_5760; } } else { goto label_5760; } } } else { return __return_main; } } } else { nl1 = 1; goto label_5748; } } else { return __return_main; } } else { goto label_5735; } } else { goto label_5735; } } else { goto label_5727; } } else { goto label_5727; } } else { goto label_5719; } } else { goto label_5719; } } } 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_5644:; node4____CPAchecker_TMP_2 = p43_new; goto label_5645; } } else { goto label_5644; } } else { goto label_5647; } } else { goto label_5647; } } else { label_5634:; node4____CPAchecker_TMP_1 = p42_new; goto label_5635; } } else { goto label_5634; } } else { goto label_5628; } } else { goto label_5628; } } else { label_5624:; node4____CPAchecker_TMP_0 = p41_new; goto label_5625; } } else { goto label_5624; } } else { goto label_5618; } } else { goto label_5618; } } else { return __return_main; } } } } else { label_5604:; node3____CPAchecker_TMP_2 = p34_new; goto label_5605; } } else { goto label_5604; } } else { goto label_5607; } } else { goto label_5607; } } else { label_5594:; node3____CPAchecker_TMP_1 = p32_new; goto label_5595; } } else { goto label_5594; } } else { goto label_5588; } } else { goto label_5588; } } else { label_5584:; node3____CPAchecker_TMP_0 = p31_new; goto label_5585; } } else { goto label_5584; } } else { goto label_5578; } } else { goto label_5578; } } else { return __return_main; } } } } else { label_5564:; node2____CPAchecker_TMP_2 = p24_new; goto label_5565; } } else { goto label_5564; } } else { goto label_5567; } } else { goto label_5567; } } else { label_5554:; node2____CPAchecker_TMP_1 = p23_new; goto label_5555; } } else { goto label_5554; } } else { goto label_5548; } } else { goto label_5548; } } else { label_5544:; node2____CPAchecker_TMP_0 = p21_new; goto label_5545; } } else { goto label_5544; } } else { goto label_5538; } } else { goto label_5538; } } 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_5448; } } else { goto label_5448; } } else { goto label_5440; } } else { goto label_5440; } } else { goto label_5432; } } else { goto label_5432; } } } else { return __return_main; } } } } else { goto label_5411; } } else { goto label_5411; } } else { goto label_5403; } } else { goto label_5403; } } else { goto label_5395; } } else { goto label_5395; } } } else { return __return_main; } } } } else { goto label_5374; } } else { goto label_5374; } } else { goto label_5366; } } else { goto label_5366; } } else { goto label_5358; } } else { goto label_5358; } } } else { return __return_main; } } } } else { goto label_5337; } } else { goto label_5337; } } else { goto label_5329; } } else { goto label_5329; } } else { goto label_5321; } } else { goto label_5321; } } } 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_5246:; node4____CPAchecker_TMP_2 = p43_new; goto label_5247; } } else { goto label_5246; } } else { goto label_5249; } } else { goto label_5249; } } else { label_5236:; node4____CPAchecker_TMP_1 = p42_new; goto label_5237; } } else { goto label_5236; } } else { goto label_5230; } } else { goto label_5230; } } else { label_5226:; node4____CPAchecker_TMP_0 = p41_new; goto label_5227; } } else { goto label_5226; } } else { goto label_5220; } } else { goto label_5220; } } else { return __return_main; } } } } else { label_5206:; node3____CPAchecker_TMP_2 = p34_new; goto label_5207; } } else { goto label_5206; } } else { goto label_5209; } } else { goto label_5209; } } else { label_5196:; node3____CPAchecker_TMP_1 = p32_new; goto label_5197; } } else { goto label_5196; } } else { goto label_5190; } } else { goto label_5190; } } else { label_5186:; node3____CPAchecker_TMP_0 = p31_new; goto label_5187; } } else { goto label_5186; } } else { goto label_5180; } } else { goto label_5180; } } else { return __return_main; } } } } else { label_5166:; node2____CPAchecker_TMP_2 = p24_new; goto label_5167; } } else { goto label_5166; } } else { goto label_5169; } } else { goto label_5169; } } else { label_5156:; node2____CPAchecker_TMP_1 = p23_new; goto label_5157; } } else { goto label_5156; } } else { goto label_5150; } } else { goto label_5150; } } else { label_5146:; node2____CPAchecker_TMP_0 = p21_new; goto label_5147; } } else { goto label_5146; } } else { goto label_5140; } } else { goto label_5140; } } else { return __return_main; } } } } else { label_5126:; node1____CPAchecker_TMP_2 = p14_new; goto label_5127; } } else { goto label_5126; } } else { goto label_5129; } } else { goto label_5129; } } else { label_5116:; node1____CPAchecker_TMP_1 = p13_new; goto label_5117; } } else { goto label_5116; } } else { goto label_5110; } } else { goto label_5110; } } else { label_5106:; node1____CPAchecker_TMP_0 = p12_new; goto label_5107; } } else { goto label_5106; } } else { goto label_5100; } } else { goto label_5100; } } 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_5020; } } else { goto label_5020; } } else { goto label_5012; } } else { goto label_5012; } } else { goto label_5004; } } else { goto label_5004; } } } else { return __return_main; } } } } else { goto label_4983; } } else { goto label_4983; } } else { goto label_4975; } } else { goto label_4975; } } else { goto label_4967; } } else { goto label_4967; } } } else { return __return_main; } } } } else { goto label_4946; } } else { goto label_4946; } } else { goto label_4938; } } else { goto label_4938; } } else { goto label_4930; } } else { goto label_4930; } } } else { return __return_main; } } } } else { goto label_4909; } } else { goto label_4909; } } else { goto label_4901; } } else { goto label_4901; } } else { goto label_4893; } } else { goto label_4893; } } } 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_4818:; node4____CPAchecker_TMP_2 = p43_new; goto label_4819; } } else { goto label_4818; } } else { goto label_4821; } } else { goto label_4821; } } else { label_4808:; node4____CPAchecker_TMP_1 = p42_new; goto label_4809; } } else { goto label_4808; } } else { goto label_4802; } } else { goto label_4802; } } else { label_4798:; node4____CPAchecker_TMP_0 = p41_new; goto label_4799; } } else { goto label_4798; } } else { goto label_4792; } } else { goto label_4792; } } else { return __return_main; } } } } else { label_4778:; node3____CPAchecker_TMP_2 = p34_new; goto label_4779; } } else { goto label_4778; } } else { goto label_4781; } } else { goto label_4781; } } else { label_4768:; node3____CPAchecker_TMP_1 = p32_new; goto label_4769; } } else { goto label_4768; } } else { goto label_4762; } } else { goto label_4762; } } else { label_4758:; node3____CPAchecker_TMP_0 = p31_new; goto label_4759; } } else { goto label_4758; } } else { goto label_4752; } } else { goto label_4752; } } else { return __return_main; } } } } else { label_4738:; node2____CPAchecker_TMP_2 = p24_new; goto label_4739; } } else { goto label_4738; } } else { goto label_4741; } } else { goto label_4741; } } else { label_4728:; node2____CPAchecker_TMP_1 = p23_new; goto label_4729; } } else { goto label_4728; } } else { goto label_4722; } } else { goto label_4722; } } else { label_4718:; node2____CPAchecker_TMP_0 = p21_new; goto label_4719; } } else { goto label_4718; } } else { goto label_4712; } } else { goto label_4712; } } else { return __return_main; } } } } else { label_4698:; node1____CPAchecker_TMP_2 = p14_new; goto label_4699; } } else { goto label_4698; } } else { goto label_4701; } } else { goto label_4701; } } else { label_4688:; node1____CPAchecker_TMP_1 = p13_new; goto label_4689; } } else { goto label_4688; } } else { goto label_4682; } } else { goto label_4682; } } else { label_4678:; node1____CPAchecker_TMP_0 = p12_new; goto label_4679; } } else { goto label_4678; } } else { goto label_4672; } } else { goto label_4672; } } 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 { 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_4540; } else { label_6361:; if (!(init__r422 == 0)) { if (!(ep23 == 0)) { init__tmp___22 = 1; label_6367:; goto label_4540; } else { init__tmp___22 = 0; goto label_6367; } } else { init__tmp___22 = 0; goto label_4540; } } } else { goto label_6361; } } } else { if (!(init__r412 == 0)) { if (!(ep12 == 0)) { init__tmp___21 = 1; goto label_4535; } else { label_6376:; if (!(init__r432 == 0)) { if (!(ep32 == 0)) { init__tmp___21 = 1; label_6382:; goto label_4535; } else { init__tmp___21 = 0; goto label_6382; } } else { init__tmp___21 = 0; goto label_4535; } } } else { goto label_6376; } } } else { if (!(init__r422 == 0)) { if (!(ep21 == 0)) { init__tmp___20 = 1; goto label_4530; } else { label_6391:; if (!(init__r432 == 0)) { if (!(ep31 == 0)) { init__tmp___20 = 1; label_6397:; goto label_4530; } else { init__tmp___20 = 0; goto label_6397; } } else { init__tmp___20 = 0; goto label_4530; } } } else { goto label_6391; } } } else { if (!(init__r312 == 0)) { if (!(ep14 == 0)) { init__tmp___19 = 1; goto label_4525; } else { label_6406:; if (!(init__r322 == 0)) { if (!(ep24 == 0)) { init__tmp___19 = 1; label_6412:; goto label_4525; } else { init__tmp___19 = 0; goto label_6412; } } else { init__tmp___19 = 0; goto label_4525; } } } else { goto label_6406; } } } else { if (!(init__r312 == 0)) { if (!(ep12 == 0)) { init__tmp___18 = 1; goto label_4520; } else { label_6421:; if (!(init__r342 == 0)) { if (!(ep42 == 0)) { init__tmp___18 = 1; label_6427:; goto label_4520; } else { init__tmp___18 = 0; goto label_6427; } } else { init__tmp___18 = 0; goto label_4520; } } } else { goto label_6421; } } } else { if (!(init__r322 == 0)) { if (!(ep21 == 0)) { init__tmp___17 = 1; goto label_4515; } else { label_6436:; if (!(init__r342 == 0)) { if (!(ep41 == 0)) { init__tmp___17 = 1; label_6442:; goto label_4515; } else { init__tmp___17 = 0; goto label_6442; } } else { init__tmp___17 = 0; goto label_4515; } } } else { goto label_6436; } } } else { if (!(init__r212 == 0)) { if (!(ep14 == 0)) { init__tmp___16 = 1; goto label_4510; } else { label_6451:; if (!(init__r232 == 0)) { if (!(ep34 == 0)) { init__tmp___16 = 1; label_6457:; goto label_4510; } else { init__tmp___16 = 0; goto label_6457; } } else { init__tmp___16 = 0; goto label_4510; } } } else { goto label_6451; } } } else { if (!(init__r212 == 0)) { if (!(ep13 == 0)) { init__tmp___15 = 1; goto label_4505; } else { label_6466:; if (!(init__r242 == 0)) { if (!(ep43 == 0)) { init__tmp___15 = 1; label_6472:; goto label_4505; } else { init__tmp___15 = 0; goto label_6472; } } else { init__tmp___15 = 0; goto label_4505; } } } else { goto label_6466; } } } else { if (!(init__r232 == 0)) { if (!(ep31 == 0)) { init__tmp___14 = 1; goto label_4500; } else { label_6481:; if (!(init__r242 == 0)) { if (!(ep41 == 0)) { init__tmp___14 = 1; label_6487:; goto label_4500; } else { init__tmp___14 = 0; goto label_6487; } } else { init__tmp___14 = 0; goto label_4500; } } } else { goto label_6481; } } } else { if (!(init__r122 == 0)) { if (!(ep24 == 0)) { init__tmp___13 = 1; goto label_4495; } else { label_6496:; if (!(init__r132 == 0)) { if (!(ep34 == 0)) { init__tmp___13 = 1; label_6502:; goto label_4495; } else { init__tmp___13 = 0; goto label_6502; } } else { init__tmp___13 = 0; goto label_4495; } } } else { goto label_6496; } } } else { if (!(init__r122 == 0)) { if (!(ep23 == 0)) { init__tmp___12 = 1; goto label_4490; } else { label_6511:; if (!(init__r142 == 0)) { if (!(ep43 == 0)) { init__tmp___12 = 1; label_6517:; goto label_4490; } else { init__tmp___12 = 0; goto label_6517; } } else { init__tmp___12 = 0; goto label_4490; } } } else { goto label_6511; } } } else { if (!(init__r132 == 0)) { if (!(ep32 == 0)) { init__tmp___11 = 1; goto label_4485; } else { label_6526:; if (!(init__r142 == 0)) { if (!(ep42 == 0)) { init__tmp___11 = 1; label_6532:; goto label_4485; } else { init__tmp___11 = 0; goto label_6532; } } else { init__tmp___11 = 0; goto label_4485; } } } else { goto label_6526; } } } else { if (!(init__r411 == 0)) { if (!(ep13 == 0)) { init__tmp___10 = 1; goto label_4480; } else { label_6541:; if (!(init__r421 == 0)) { if (!(ep23 == 0)) { init__tmp___10 = 1; label_6547:; goto label_4480; } else { init__tmp___10 = 0; goto label_6547; } } else { init__tmp___10 = 0; goto label_4480; } } } else { goto label_6541; } } } else { if (!(init__r411 == 0)) { if (!(ep12 == 0)) { init__tmp___9 = 1; goto label_4475; } else { label_6556:; if (!(init__r431 == 0)) { if (!(ep32 == 0)) { init__tmp___9 = 1; label_6562:; goto label_4475; } else { init__tmp___9 = 0; goto label_6562; } } else { init__tmp___9 = 0; goto label_4475; } } } else { goto label_6556; } } } else { if (!(init__r421 == 0)) { if (!(ep21 == 0)) { init__tmp___8 = 1; goto label_4470; } else { label_6571:; if (!(init__r431 == 0)) { if (!(ep31 == 0)) { init__tmp___8 = 1; label_6577:; goto label_4470; } else { init__tmp___8 = 0; goto label_6577; } } else { init__tmp___8 = 0; goto label_4470; } } } else { goto label_6571; } } } else { if (!(init__r311 == 0)) { if (!(ep14 == 0)) { init__tmp___7 = 1; goto label_4465; } else { label_6586:; if (!(init__r321 == 0)) { if (!(ep24 == 0)) { init__tmp___7 = 1; label_6592:; goto label_4465; } else { init__tmp___7 = 0; goto label_6592; } } else { init__tmp___7 = 0; goto label_4465; } } } else { goto label_6586; } } } else { if (!(init__r311 == 0)) { if (!(ep12 == 0)) { init__tmp___6 = 1; goto label_4460; } else { label_6601:; if (!(init__r341 == 0)) { if (!(ep42 == 0)) { init__tmp___6 = 1; label_6607:; goto label_4460; } else { init__tmp___6 = 0; goto label_6607; } } else { init__tmp___6 = 0; goto label_4460; } } } else { goto label_6601; } } } else { if (!(init__r321 == 0)) { if (!(ep21 == 0)) { init__tmp___5 = 1; goto label_4455; } else { label_6616:; if (!(init__r341 == 0)) { if (!(ep41 == 0)) { init__tmp___5 = 1; label_6622:; goto label_4455; } else { init__tmp___5 = 0; goto label_6622; } } else { init__tmp___5 = 0; goto label_4455; } } } else { goto label_6616; } } } else { if (!(init__r211 == 0)) { if (!(ep14 == 0)) { init__tmp___4 = 1; goto label_4450; } else { label_6631:; if (!(init__r231 == 0)) { if (!(ep34 == 0)) { init__tmp___4 = 1; label_6637:; goto label_4450; } else { init__tmp___4 = 0; goto label_6637; } } else { init__tmp___4 = 0; goto label_4450; } } } else { goto label_6631; } } } else { if (!(init__r211 == 0)) { if (!(ep13 == 0)) { init__tmp___3 = 1; goto label_4445; } else { label_6646:; if (!(init__r241 == 0)) { if (!(ep43 == 0)) { init__tmp___3 = 1; label_6652:; goto label_4445; } else { init__tmp___3 = 0; goto label_6652; } } else { init__tmp___3 = 0; goto label_4445; } } } else { goto label_6646; } } } else { if (!(init__r231 == 0)) { if (!(ep31 == 0)) { init__tmp___2 = 1; goto label_4440; } else { label_6661:; if (!(init__r241 == 0)) { if (!(ep41 == 0)) { init__tmp___2 = 1; label_6667:; goto label_4440; } else { init__tmp___2 = 0; goto label_6667; } } else { init__tmp___2 = 0; goto label_4440; } } } else { goto label_6661; } } } else { if (!(init__r121 == 0)) { if (!(ep24 == 0)) { init__tmp___1 = 1; goto label_4435; } else { label_6676:; if (!(init__r131 == 0)) { if (!(ep34 == 0)) { init__tmp___1 = 1; label_6682:; goto label_4435; } else { init__tmp___1 = 0; goto label_6682; } } else { init__tmp___1 = 0; goto label_4435; } } } else { goto label_6676; } } } else { if (!(init__r121 == 0)) { if (!(ep23 == 0)) { init__tmp___0 = 1; goto label_4430; } else { label_6691:; if (!(init__r141 == 0)) { if (!(ep43 == 0)) { init__tmp___0 = 1; label_6697:; goto label_4430; } else { init__tmp___0 = 0; goto label_6697; } } else { init__tmp___0 = 0; goto label_4430; } } } else { goto label_6691; } } } else { if (!(init__r131 == 0)) { if (!(ep32 == 0)) { init__tmp = 1; goto label_4425; } else { label_6706:; if (!(init__r141 == 0)) { if (!(ep42 == 0)) { init__tmp = 1; label_6712:; goto label_4425; } else { init__tmp = 0; goto label_6712; } } else { init__tmp = 0; goto label_4425; } } } else { goto label_6706; } } } }