// 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.BOUNDED-8.pals.c.v+lhb-reducer.c", 4, "reach_error"); } char __VERIFIER_nondet_char(); _Bool __VERIFIER_nondet_bool(); void assert(_Bool arg); void abort(void); void assume_abort_if_not(int cond) { if(!cond) {abort();} } typedef char msg_t; typedef int port_t; void read(port_t p, msg_t m); void write(port_t p, msg_t m); msg_t nomsg = (msg_t )-1; port_t p12 = 0; char p12_old = '\x0'; char p12_new = '\x0'; _Bool ep12 = 0; port_t p13 = 0; char p13_old = '\x0'; char p13_new = '\x0'; _Bool ep13 = 0; port_t p14 = 0; char p14_old = '\x0'; char p14_new = '\x0'; _Bool ep14 = 0; port_t p21 = 0; char p21_old = '\x0'; char p21_new = '\x0'; _Bool ep21 = 0; port_t p23 = 0; char p23_old = '\x0'; char p23_new = '\x0'; _Bool ep23 = 0; port_t p24 = 0; char p24_old = '\x0'; char p24_new = '\x0'; _Bool ep24 = 0; port_t p31 = 0; char p31_old = '\x0'; char p31_new = '\x0'; _Bool ep31 = 0; port_t p32 = 0; char p32_old = '\x0'; char p32_new = '\x0'; _Bool ep32 = 0; port_t p34 = 0; char p34_old = '\x0'; char p34_new = '\x0'; _Bool ep34 = 0; port_t p41 = 0; char p41_old = '\x0'; char p41_new = '\x0'; _Bool ep41 = 0; port_t p42 = 0; char p42_old = '\x0'; char p42_new = '\x0'; _Bool ep42 = 0; port_t p43 = 0; char p43_old = '\x0'; char p43_new = '\x0'; _Bool ep43 = 0; char id1 = '\x0'; char r1 = '\x0'; char st1 = '\x0'; char nl1 = '\x0'; char m1 = '\x0'; char max1 = '\x0'; _Bool mode1 = 0; _Bool newmax1 = 0; char id2 = '\x0'; char r2 = '\x0'; char st2 = '\x0'; char nl2 = '\x0'; char m2 = '\x0'; char max2 = '\x0'; _Bool mode2 = 0; _Bool newmax2 = 0; char id3 = '\x0'; char r3 = '\x0'; char st3 = '\x0'; char nl3 = '\x0'; char m3 = '\x0'; char max3 = '\x0'; _Bool mode3 = 0; _Bool newmax3 = 0; char id4 = '\x0'; 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_4614; int __return_4856; int __return_5063; int __return_5286; int __return_5493; int __return_5686; int __return_7466; int __return_7423; int __return_7340; int __return_7297; int __return_7174; int __return_7131; int __return_7048; int __return_7002; int __tmp_5903_0; int __return_6100; int __return_5916; int __return_6819; int __return_6776; int __return_6693; int __return_6647; int __return_6504; int __return_6458; int __return_6352; int __return_5902; int main() { int main__c1; int main__i2; main__c1 = 0; ep12 = __VERIFIER_nondet_bool(); ep13 = __VERIFIER_nondet_bool(); ep14 = __VERIFIER_nondet_bool(); ep21 = __VERIFIER_nondet_bool(); ep23 = __VERIFIER_nondet_bool(); ep24 = __VERIFIER_nondet_bool(); ep31 = __VERIFIER_nondet_bool(); ep32 = __VERIFIER_nondet_bool(); ep34 = __VERIFIER_nondet_bool(); ep41 = __VERIFIER_nondet_bool(); ep42 = __VERIFIER_nondet_bool(); ep43 = __VERIFIER_nondet_bool(); id1 = __VERIFIER_nondet_char(); r1 = __VERIFIER_nondet_char(); st1 = __VERIFIER_nondet_char(); nl1 = __VERIFIER_nondet_char(); m1 = __VERIFIER_nondet_char(); max1 = __VERIFIER_nondet_char(); mode1 = __VERIFIER_nondet_bool(); newmax1 = __VERIFIER_nondet_bool(); id2 = __VERIFIER_nondet_char(); r2 = __VERIFIER_nondet_char(); st2 = __VERIFIER_nondet_char(); nl2 = __VERIFIER_nondet_char(); m2 = __VERIFIER_nondet_char(); max2 = __VERIFIER_nondet_char(); mode2 = __VERIFIER_nondet_bool(); newmax2 = __VERIFIER_nondet_bool(); id3 = __VERIFIER_nondet_char(); r3 = __VERIFIER_nondet_char(); st3 = __VERIFIER_nondet_char(); nl3 = __VERIFIER_nondet_char(); m3 = __VERIFIER_nondet_char(); max3 = __VERIFIER_nondet_char(); mode3 = __VERIFIER_nondet_bool(); newmax3 = __VERIFIER_nondet_bool(); id4 = __VERIFIER_nondet_char(); r4 = __VERIFIER_nondet_char(); st4 = __VERIFIER_nondet_char(); nl4 = __VERIFIER_nondet_char(); m4 = __VERIFIER_nondet_char(); max4 = __VERIFIER_nondet_char(); mode4 = __VERIFIER_nondet_bool(); 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_4404:; init__r122 = (_Bool)init__tmp; if (!(init__r131 == 0)) { init__tmp___0 = 1; label_4409:; init__r132 = (_Bool)init__tmp___0; if (!(init__r141 == 0)) { init__tmp___1 = 1; label_4414:; init__r142 = (_Bool)init__tmp___1; if (!(init__r211 == 0)) { init__tmp___2 = 1; label_4419:; init__r212 = (_Bool)init__tmp___2; if (!(init__r231 == 0)) { init__tmp___3 = 1; label_4424:; init__r232 = (_Bool)init__tmp___3; if (!(init__r241 == 0)) { init__tmp___4 = 1; label_4429:; init__r242 = (_Bool)init__tmp___4; if (!(init__r311 == 0)) { init__tmp___5 = 1; label_4434:; init__r312 = (_Bool)init__tmp___5; if (!(init__r321 == 0)) { init__tmp___6 = 1; label_4439:; init__r322 = (_Bool)init__tmp___6; if (!(init__r341 == 0)) { init__tmp___7 = 1; label_4444:; init__r342 = (_Bool)init__tmp___7; if (!(init__r411 == 0)) { init__tmp___8 = 1; label_4449:; init__r412 = (_Bool)init__tmp___8; if (!(init__r421 == 0)) { init__tmp___9 = 1; label_4454:; init__r422 = (_Bool)init__tmp___9; if (!(init__r431 == 0)) { init__tmp___10 = 1; label_4459:; init__r432 = (_Bool)init__tmp___10; if (!(init__r122 == 0)) { init__tmp___11 = 1; label_4464:; init__r123 = (_Bool)init__tmp___11; if (!(init__r132 == 0)) { init__tmp___12 = 1; label_4469:; init__r133 = (_Bool)init__tmp___12; if (!(init__r142 == 0)) { init__tmp___13 = 1; label_4474:; init__r143 = (_Bool)init__tmp___13; if (!(init__r212 == 0)) { init__tmp___14 = 1; label_4479:; init__r213 = (_Bool)init__tmp___14; if (!(init__r232 == 0)) { init__tmp___15 = 1; label_4484:; init__r233 = (_Bool)init__tmp___15; if (!(init__r242 == 0)) { init__tmp___16 = 1; label_4489:; init__r243 = (_Bool)init__tmp___16; if (!(init__r312 == 0)) { init__tmp___17 = 1; label_4494:; init__r313 = (_Bool)init__tmp___17; if (!(init__r322 == 0)) { init__tmp___18 = 1; label_4499:; init__r323 = (_Bool)init__tmp___18; if (!(init__r342 == 0)) { init__tmp___19 = 1; label_4504:; init__r343 = (_Bool)init__tmp___19; if (!(init__r412 == 0)) { init__tmp___20 = 1; label_4509:; init__r413 = (_Bool)init__tmp___20; if (!(init__r422 == 0)) { init__tmp___21 = 1; label_4514:; init__r423 = (_Bool)init__tmp___21; if (!(init__r432 == 0)) { init__tmp___22 = 1; label_4519:; 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_4614 = init__tmp___23; main__i2 = __return_4614; if (main__i2 != 0) { p12_old = nomsg; p12_new = nomsg; p13_old = nomsg; p13_new = nomsg; p14_old = nomsg; p14_new = nomsg; p21_old = nomsg; p21_new = nomsg; p23_old = nomsg; p23_new = nomsg; p24_old = nomsg; p24_new = nomsg; p31_old = nomsg; p31_new = nomsg; p32_old = nomsg; p32_new = nomsg; p34_old = nomsg; p34_new = nomsg; p41_old = nomsg; p41_new = nomsg; p42_old = nomsg; p42_new = nomsg; p43_old = nomsg; p43_new = nomsg; main__i2 = 0; if (main__i2 < 8) { { _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_4658:; p12_new = node1____CPAchecker_TMP_0; label_4651:; if (!(ep13 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4668:; p13_new = node1____CPAchecker_TMP_1; label_4661:; if (!(ep14 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4678:; p14_new = node1____CPAchecker_TMP_2; label_4680:; 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_4698:; p21_new = node2____CPAchecker_TMP_0; label_4691:; if (!(ep23 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4708:; p23_new = node2____CPAchecker_TMP_1; label_4701:; if (!(ep24 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4718:; p24_new = node2____CPAchecker_TMP_2; label_4720:; 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_4738:; p31_new = node3____CPAchecker_TMP_0; label_4731:; if (!(ep32 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4748:; p32_new = node3____CPAchecker_TMP_1; label_4741:; if (!(ep34 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4758:; p34_new = node3____CPAchecker_TMP_2; label_4760:; 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_4778:; p41_new = node4____CPAchecker_TMP_0; label_4771:; if (!(ep42 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4788:; p42_new = node4____CPAchecker_TMP_1; label_4781:; if (!(ep43 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4798:; p43_new = node4____CPAchecker_TMP_2; label_4800:; 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_4856 = check__tmp; main__c1 = __return_4856; { _Bool __tmp_1; __tmp_1 = main__c1; _Bool assert__arg; assert__arg = __tmp_1; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { _Bool node1__newmax; node1__newmax = 0; if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_4874:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_4882:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_4890:; newmax1 = node1__newmax; if (((int)r1) == 3) { return __return_main; } else { mode1 = 0; { _Bool node2__newmax; node2__newmax = 0; if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_4910:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_4918:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_4926:; newmax2 = node2__newmax; if (((int)r2) == 3) { return __return_main; } else { mode2 = 0; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_4946:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_4954:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_4962:; newmax3 = node3__newmax; if (((int)r3) == 3) { return __return_main; } else { mode3 = 0; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_4982:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_4990:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_4998:; 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_5063 = check__tmp; main__c1 = __return_5063; { _Bool __tmp_2; __tmp_2 = main__c1; _Bool assert__arg; assert__arg = __tmp_2; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { _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_5088:; p12_new = node1____CPAchecker_TMP_0; label_5081:; if (!(ep13 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5098:; p13_new = node1____CPAchecker_TMP_1; label_5091:; if (!(ep14 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5108:; p14_new = node1____CPAchecker_TMP_2; label_5110:; 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_5128:; p21_new = node2____CPAchecker_TMP_0; label_5121:; if (!(ep23 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5138:; p23_new = node2____CPAchecker_TMP_1; label_5131:; if (!(ep24 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5148:; p24_new = node2____CPAchecker_TMP_2; label_5150:; 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_5168:; p31_new = node3____CPAchecker_TMP_0; label_5161:; if (!(ep32 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5178:; p32_new = node3____CPAchecker_TMP_1; label_5171:; if (!(ep34 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5188:; p34_new = node3____CPAchecker_TMP_2; label_5190:; 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_5208:; p41_new = node4____CPAchecker_TMP_0; label_5201:; if (!(ep42 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5218:; p42_new = node4____CPAchecker_TMP_1; label_5211:; if (!(ep43 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5228:; p43_new = node4____CPAchecker_TMP_2; label_5230:; 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_5286 = check__tmp; main__c1 = __return_5286; { _Bool __tmp_3; __tmp_3 = main__c1; _Bool assert__arg; assert__arg = __tmp_3; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { _Bool node1__newmax; node1__newmax = 0; if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5304:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5312:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5320:; newmax1 = node1__newmax; if (((int)r1) == 3) { return __return_main; } else { mode1 = 0; { _Bool node2__newmax; node2__newmax = 0; if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5340:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5348:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5356:; newmax2 = node2__newmax; if (((int)r2) == 3) { return __return_main; } else { mode2 = 0; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5376:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5384:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5392:; newmax3 = node3__newmax; if (((int)r3) == 3) { return __return_main; } else { mode3 = 0; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5412:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5420:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5428:; 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_5493 = check__tmp; main__c1 = __return_5493; { _Bool __tmp_4; __tmp_4 = main__c1; _Bool assert__arg; assert__arg = __tmp_4; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { _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_5528:; p21_new = node2____CPAchecker_TMP_0; label_5521:; if (!(ep23 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5538:; p23_new = node2____CPAchecker_TMP_1; label_5531:; if (!(ep24 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5548:; p24_new = node2____CPAchecker_TMP_2; label_5550:; 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_5568:; p31_new = node3____CPAchecker_TMP_0; label_5561:; if (!(ep32 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5578:; p32_new = node3____CPAchecker_TMP_1; label_5571:; if (!(ep34 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5588:; p34_new = node3____CPAchecker_TMP_2; label_5590:; 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_5608:; p41_new = node4____CPAchecker_TMP_0; label_5601:; if (!(ep42 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5618:; p42_new = node4____CPAchecker_TMP_1; label_5611:; if (!(ep43 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5628:; p43_new = node4____CPAchecker_TMP_2; label_5630:; 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_5686 = check__tmp; main__c1 = __return_5686; { _Bool __tmp_5; __tmp_5 = main__c1; _Bool assert__arg; assert__arg = __tmp_5; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { _Bool node1__newmax; node1__newmax = 0; if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5704:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5712:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5720:; newmax1 = node1__newmax; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; mode1 = 0; { _Bool node2__newmax; node2__newmax = 0; if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_6838:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_6846:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_6854:; newmax2 = node2__newmax; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; mode2 = 0; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_7193:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_7201:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_7209:; newmax3 = node3__newmax; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; mode3 = 0; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_7359:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_7367:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_7375:; newmax4 = node4__newmax; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; 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) { return __return_main; } else { check__tmp = 0; __return_7466 = check__tmp; main__c1 = __return_7466; { _Bool __tmp_6; __tmp_6 = main__c1; _Bool assert__arg; assert__arg = __tmp_6; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { nl4 = 1; 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) { return __return_main; } else { check__tmp = 0; __return_7423 = check__tmp; main__c1 = __return_7423; { _Bool __tmp_7; __tmp_7 = main__c1; _Bool assert__arg; assert__arg = __tmp_7; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } } else { return __return_main; } } else { goto label_7375; } } else { goto label_7375; } } else { goto label_7367; } } else { goto label_7367; } } else { goto label_7359; } } else { goto label_7359; } } else { return __return_main; } } } else { nl3 = 1; mode3 = 0; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_7233:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_7241:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_7249:; newmax4 = node4__newmax; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; 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) { return __return_main; } else { check__tmp = 0; __return_7340 = check__tmp; main__c1 = __return_7340; { _Bool __tmp_8; __tmp_8 = main__c1; _Bool assert__arg; assert__arg = __tmp_8; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { nl4 = 1; 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) { return __return_main; } else { check__tmp = 0; __return_7297 = check__tmp; main__c1 = __return_7297; { _Bool __tmp_9; __tmp_9 = main__c1; _Bool assert__arg; assert__arg = __tmp_9; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } } else { return __return_main; } } else { goto label_7249; } } else { goto label_7249; } } else { goto label_7241; } } else { goto label_7241; } } else { goto label_7233; } } else { goto label_7233; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_7209; } } else { goto label_7209; } } else { goto label_7201; } } else { goto label_7201; } } else { goto label_7193; } } else { goto label_7193; } } else { return __return_main; } } } else { nl2 = 1; mode2 = 0; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6878:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6886:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6894:; newmax3 = node3__newmax; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; mode3 = 0; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_7067:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_7075:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_7083:; newmax4 = node4__newmax; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; 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) { return __return_main; } else { check__tmp = 0; __return_7174 = check__tmp; main__c1 = __return_7174; { _Bool __tmp_10; __tmp_10 = main__c1; _Bool assert__arg; assert__arg = __tmp_10; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { nl4 = 1; 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) { return __return_main; } else { check__tmp = 0; __return_7131 = check__tmp; main__c1 = __return_7131; { _Bool __tmp_11; __tmp_11 = main__c1; _Bool assert__arg; assert__arg = __tmp_11; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } } else { return __return_main; } } else { goto label_7083; } } else { goto label_7083; } } else { goto label_7075; } } else { goto label_7075; } } else { goto label_7067; } } else { goto label_7067; } } else { return __return_main; } } } else { nl3 = 1; mode3 = 0; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6918:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6926:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6934:; newmax4 = node4__newmax; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; 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) { return __return_main; } else { check__tmp = 0; __return_7048 = check__tmp; main__c1 = __return_7048; { _Bool __tmp_12; __tmp_12 = main__c1; _Bool assert__arg; assert__arg = __tmp_12; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { nl4 = 1; 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_7003:; if (((int)r1) < 3) { check__tmp = 1; label_7009:; label_6994:; __return_7002 = check__tmp; main__c1 = __return_7002; __tmp_5903_0 = main____CPAchecker_TMP_0; label_5903:; main____CPAchecker_TMP_0 = __tmp_5903_0; { _Bool __tmp_13; __tmp_13 = main__c1; _Bool assert__arg; assert__arg = __tmp_13; if (assert__arg == 0) { {reach_error();} return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { _Bool node1__newmax; node1__newmax = 0; if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5924:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5932:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; node1__newmax = 1; label_5940:; newmax1 = node1__newmax; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5950:; mode1 = 0; label_5952:; { _Bool node2__newmax; node2__newmax = 0; if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5962:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5970:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5978:; newmax2 = node2__newmax; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5988:; mode2 = 0; label_5990:; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6000:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6008:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6016:; newmax3 = node3__newmax; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_6026:; mode3 = 0; label_6028:; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6038:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6046:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6054:; newmax4 = node4__newmax; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_6064:; mode4 = 0; label_6066:; 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_6123:; if (((int)r1) < 3) { label_6130:; if (((int)r1) >= 3) { label_6137:; if (((int)r1) < 3) { check__tmp = 1; label_6143:; label_6136:; label_6129:; label_6122:; label_6116:; label_6112:; label_6108:; label_6104:; label_6099:; __return_6100 = check__tmp; main__c1 = __return_6100; __tmp_5903_0 = main____CPAchecker_TMP_0; goto label_5903; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6143; } else { check__tmp = 0; goto label_6143; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6137; } else { check__tmp = 0; goto label_6136; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_6130; } else { check__tmp = 0; goto label_6129; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_6123; } else { check__tmp = 0; goto label_6122; } } } else { check__tmp = 0; goto label_6116; } } else { check__tmp = 0; goto label_6112; } } else { check__tmp = 0; goto label_6108; } } else { check__tmp = 0; goto label_6104; } } else { check__tmp = 0; goto label_6099; } } } else { nl4 = 1; goto label_6064; } } else { goto label_6064; } } else { goto label_6054; } } else { goto label_6054; } } else { goto label_6046; } } else { goto label_6046; } } else { goto label_6038; } } else { goto label_6038; } } 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_6160:; p41_new = node4____CPAchecker_TMP_0; label_6153:; if (!(ep42 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_6170:; p42_new = node4____CPAchecker_TMP_1; label_6163:; if (!(ep43 == 0)) { if (!(newmax4 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_6180:; p43_new = node4____CPAchecker_TMP_2; label_6151:; mode4 = 1; goto label_6066; } else { label_6179:; node4____CPAchecker_TMP_2 = p43_new; goto label_6180; } } else { goto label_6179; } } else { goto label_6151; } } else { goto label_6151; } } else { label_6169:; node4____CPAchecker_TMP_1 = p42_new; goto label_6170; } } else { goto label_6169; } } else { goto label_6163; } } else { goto label_6163; } } else { label_6159:; node4____CPAchecker_TMP_0 = p41_new; goto label_6160; } } else { goto label_6159; } } else { goto label_6153; } } else { goto label_6153; } } else { goto label_6151; } } } } else { nl3 = 1; goto label_6026; } } else { goto label_6026; } } else { goto label_6016; } } else { goto label_6016; } } else { goto label_6008; } } else { goto label_6008; } } else { goto label_6000; } } else { goto label_6000; } } 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_6197:; p31_new = node3____CPAchecker_TMP_0; label_6190:; if (!(ep32 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_6207:; p32_new = node3____CPAchecker_TMP_1; label_6200:; if (!(ep34 == 0)) { if (!(newmax3 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_6217:; p34_new = node3____CPAchecker_TMP_2; label_6188:; mode3 = 1; goto label_6028; } else { label_6216:; node3____CPAchecker_TMP_2 = p34_new; goto label_6217; } } else { goto label_6216; } } else { goto label_6188; } } else { goto label_6188; } } else { label_6206:; node3____CPAchecker_TMP_1 = p32_new; goto label_6207; } } else { goto label_6206; } } else { goto label_6200; } } else { goto label_6200; } } else { label_6196:; node3____CPAchecker_TMP_0 = p31_new; goto label_6197; } } else { goto label_6196; } } else { goto label_6190; } } else { goto label_6190; } } else { goto label_6188; } } } } else { nl2 = 1; goto label_5988; } } else { goto label_5988; } } else { goto label_5978; } } else { goto label_5978; } } else { goto label_5970; } } else { goto label_5970; } } else { goto label_5962; } } else { goto label_5962; } } 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_6234:; p21_new = node2____CPAchecker_TMP_0; label_6227:; if (!(ep23 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_6244:; p23_new = node2____CPAchecker_TMP_1; label_6237:; if (!(ep24 == 0)) { if (!(newmax2 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_6254:; p24_new = node2____CPAchecker_TMP_2; label_6225:; mode2 = 1; goto label_5990; } else { label_6253:; node2____CPAchecker_TMP_2 = p24_new; goto label_6254; } } else { goto label_6253; } } else { goto label_6225; } } else { goto label_6225; } } else { label_6243:; node2____CPAchecker_TMP_1 = p23_new; goto label_6244; } } else { goto label_6243; } } else { goto label_6237; } } else { goto label_6237; } } else { label_6233:; node2____CPAchecker_TMP_0 = p21_new; goto label_6234; } } else { goto label_6233; } } else { goto label_6227; } } else { goto label_6227; } } else { goto label_6225; } } } } else { nl1 = 1; goto label_5950; } } else { goto label_5950; } } else { goto label_5940; } } else { goto label_5940; } } else { goto label_5932; } } else { goto label_5932; } } else { goto label_5924; } } else { goto label_5924; } } 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_6271:; p12_new = node1____CPAchecker_TMP_0; label_6264:; if (!(ep13 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_6281:; p13_new = node1____CPAchecker_TMP_1; label_6274:; if (!(ep14 == 0)) { if (!(newmax1 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_6291:; p14_new = node1____CPAchecker_TMP_2; label_6262:; mode1 = 1; goto label_5952; } else { label_6290:; node1____CPAchecker_TMP_2 = p14_new; goto label_6291; } } else { goto label_6290; } } else { goto label_6262; } } else { goto label_6262; } } else { label_6280:; node1____CPAchecker_TMP_1 = p13_new; goto label_6281; } } else { goto label_6280; } } else { goto label_6274; } } else { goto label_6274; } } else { label_6270:; node1____CPAchecker_TMP_0 = p12_new; goto label_6271; } } else { goto label_6270; } } else { goto label_6264; } } else { goto label_6264; } } else { goto label_6262; } } } } else { __return_5916 = 0; return __return_5916; } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_7009; } else { check__tmp = 0; goto label_7009; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_7003; } else { check__tmp = 0; goto label_6994; } } } 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_6934; } } else { goto label_6934; } } else { goto label_6926; } } else { goto label_6926; } } else { goto label_6918; } } else { goto label_6918; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6894; } } else { goto label_6894; } } else { goto label_6886; } } else { goto label_6886; } } else { goto label_6878; } } else { goto label_6878; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6854; } } else { goto label_6854; } } else { goto label_6846; } } else { goto label_6846; } } else { goto label_6838; } } else { goto label_6838; } } else { return __return_main; } } } else { nl1 = 1; mode1 = 0; { _Bool node2__newmax; node2__newmax = 0; if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5744:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5752:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; node2__newmax = 1; label_5760:; newmax2 = node2__newmax; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; mode2 = 0; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6523:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6531:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_6539:; newmax3 = node3__newmax; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; mode3 = 0; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6712:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6720:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6728:; newmax4 = node4__newmax; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; 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) { return __return_main; } else { check__tmp = 0; __return_6819 = check__tmp; main__c1 = __return_6819; { _Bool __tmp_14; __tmp_14 = main__c1; _Bool assert__arg; assert__arg = __tmp_14; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { nl4 = 1; 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) { return __return_main; } else { check__tmp = 0; __return_6776 = check__tmp; main__c1 = __return_6776; { _Bool __tmp_15; __tmp_15 = main__c1; _Bool assert__arg; assert__arg = __tmp_15; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } } else { return __return_main; } } else { goto label_6728; } } else { goto label_6728; } } else { goto label_6720; } } else { goto label_6720; } } else { goto label_6712; } } else { goto label_6712; } } else { return __return_main; } } } else { nl3 = 1; mode3 = 0; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6563:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6571:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6579:; newmax4 = node4__newmax; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; 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) { return __return_main; } else { check__tmp = 0; __return_6693 = check__tmp; main__c1 = __return_6693; { _Bool __tmp_16; __tmp_16 = main__c1; _Bool assert__arg; assert__arg = __tmp_16; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { nl4 = 1; 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_6648:; if (((int)r1) < 3) { check__tmp = 1; label_6654:; label_6639:; __return_6647 = check__tmp; main__c1 = __return_6647; __tmp_5903_0 = main____CPAchecker_TMP_0; goto label_5903; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6654; } else { check__tmp = 0; goto label_6654; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6648; } else { check__tmp = 0; goto label_6639; } } } 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_6579; } } else { goto label_6579; } } else { goto label_6571; } } else { goto label_6571; } } else { goto label_6563; } } else { goto label_6563; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6539; } } else { goto label_6539; } } else { goto label_6531; } } else { goto label_6531; } } else { goto label_6523; } } else { goto label_6523; } } else { return __return_main; } } } else { nl2 = 1; mode2 = 0; { _Bool node3__newmax; node3__newmax = 0; if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5784:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5792:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; node3__newmax = 1; label_5800:; newmax3 = node3__newmax; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; mode3 = 0; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6374:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6382:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_6390:; newmax4 = node4__newmax; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; 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) { return __return_main; } else { check__tmp = 0; __return_6504 = check__tmp; main__c1 = __return_6504; { _Bool __tmp_17; __tmp_17 = main__c1; _Bool assert__arg; assert__arg = __tmp_17; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { nl4 = 1; 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_6459:; if (((int)r1) < 3) { check__tmp = 1; label_6465:; label_6450:; __return_6458 = check__tmp; main__c1 = __return_6458; __tmp_5903_0 = main____CPAchecker_TMP_0; goto label_5903; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6465; } else { check__tmp = 0; goto label_6465; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6459; } else { check__tmp = 0; goto label_6450; } } } 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_6390; } } else { goto label_6390; } } else { goto label_6382; } } else { goto label_6382; } } else { goto label_6374; } } else { goto label_6374; } } else { return __return_main; } } } else { nl3 = 1; mode3 = 0; { _Bool node4__newmax; node4__newmax = 0; if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5824:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5832:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; node4__newmax = 1; label_5840:; newmax4 = node4__newmax; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; 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_6353:; if (((int)r1) < 3) { check__tmp = 1; label_6359:; label_6344:; __return_6352 = check__tmp; main__c1 = __return_6352; __tmp_5903_0 = main____CPAchecker_TMP_0; goto label_5903; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6359; } else { check__tmp = 0; goto label_6359; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6353; } else { check__tmp = 0; goto label_6344; } } } 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 { nl4 = 1; 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) { return __return_main; } else { check__tmp = 0; __return_5902 = check__tmp; main__c1 = __return_5902; __tmp_5903_0 = main____CPAchecker_TMP_0; goto label_5903; } } } 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_5840; } } else { goto label_5840; } } else { goto label_5832; } } else { goto label_5832; } } else { goto label_5824; } } else { goto label_5824; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5800; } } else { goto label_5800; } } else { goto label_5792; } } else { goto label_5792; } } else { goto label_5784; } } else { goto label_5784; } } else { return __return_main; } } } } 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 { goto label_5720; } } else { goto label_5720; } } else { goto label_5712; } } else { goto label_5712; } } else { goto label_5704; } } else { goto label_5704; } } 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 { label_5627:; node4____CPAchecker_TMP_2 = p43_new; goto label_5628; } } else { goto label_5627; } } else { goto label_5630; } } else { goto label_5630; } } else { label_5617:; node4____CPAchecker_TMP_1 = p42_new; goto label_5618; } } else { goto label_5617; } } else { goto label_5611; } } else { goto label_5611; } } else { label_5607:; node4____CPAchecker_TMP_0 = p41_new; goto label_5608; } } else { goto label_5607; } } else { goto label_5601; } } else { goto label_5601; } } else { return __return_main; } } } } else { label_5587:; node3____CPAchecker_TMP_2 = p34_new; goto label_5588; } } else { goto label_5587; } } else { goto label_5590; } } else { goto label_5590; } } else { label_5577:; node3____CPAchecker_TMP_1 = p32_new; goto label_5578; } } else { goto label_5577; } } else { goto label_5571; } } else { goto label_5571; } } else { label_5567:; node3____CPAchecker_TMP_0 = p31_new; goto label_5568; } } else { goto label_5567; } } else { goto label_5561; } } else { goto label_5561; } } else { return __return_main; } } } } else { label_5547:; node2____CPAchecker_TMP_2 = p24_new; goto label_5548; } } else { goto label_5547; } } else { goto label_5550; } } else { goto label_5550; } } else { label_5537:; node2____CPAchecker_TMP_1 = p23_new; goto label_5538; } } else { goto label_5537; } } else { goto label_5531; } } else { goto label_5531; } } else { label_5527:; node2____CPAchecker_TMP_0 = p21_new; goto label_5528; } } else { goto label_5527; } } else { goto label_5521; } } else { goto label_5521; } } 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 { goto label_5428; } } else { goto label_5428; } } else { goto label_5420; } } else { goto label_5420; } } else { goto label_5412; } } else { goto label_5412; } } else { return __return_main; } } } } else { goto label_5392; } } else { goto label_5392; } } else { goto label_5384; } } else { goto label_5384; } } else { goto label_5376; } } else { goto label_5376; } } else { return __return_main; } } } } else { goto label_5356; } } else { goto label_5356; } } else { goto label_5348; } } else { goto label_5348; } } else { goto label_5340; } } else { goto label_5340; } } else { return __return_main; } } } } else { goto label_5320; } } else { goto label_5320; } } else { goto label_5312; } } else { goto label_5312; } } else { goto label_5304; } } else { goto label_5304; } } 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 { label_5227:; node4____CPAchecker_TMP_2 = p43_new; goto label_5228; } } else { goto label_5227; } } else { goto label_5230; } } else { goto label_5230; } } else { label_5217:; node4____CPAchecker_TMP_1 = p42_new; goto label_5218; } } else { goto label_5217; } } else { goto label_5211; } } else { goto label_5211; } } else { label_5207:; node4____CPAchecker_TMP_0 = p41_new; goto label_5208; } } else { goto label_5207; } } else { goto label_5201; } } else { goto label_5201; } } else { return __return_main; } } } } else { label_5187:; node3____CPAchecker_TMP_2 = p34_new; goto label_5188; } } else { goto label_5187; } } else { goto label_5190; } } else { goto label_5190; } } else { label_5177:; node3____CPAchecker_TMP_1 = p32_new; goto label_5178; } } else { goto label_5177; } } else { goto label_5171; } } else { goto label_5171; } } else { label_5167:; node3____CPAchecker_TMP_0 = p31_new; goto label_5168; } } else { goto label_5167; } } else { goto label_5161; } } else { goto label_5161; } } else { return __return_main; } } } } else { label_5147:; node2____CPAchecker_TMP_2 = p24_new; goto label_5148; } } else { goto label_5147; } } else { goto label_5150; } } else { goto label_5150; } } else { label_5137:; node2____CPAchecker_TMP_1 = p23_new; goto label_5138; } } else { goto label_5137; } } else { goto label_5131; } } else { goto label_5131; } } else { label_5127:; node2____CPAchecker_TMP_0 = p21_new; goto label_5128; } } else { goto label_5127; } } else { goto label_5121; } } else { goto label_5121; } } else { return __return_main; } } } } else { label_5107:; node1____CPAchecker_TMP_2 = p14_new; goto label_5108; } } else { goto label_5107; } } else { goto label_5110; } } else { goto label_5110; } } else { label_5097:; node1____CPAchecker_TMP_1 = p13_new; goto label_5098; } } else { goto label_5097; } } else { goto label_5091; } } else { goto label_5091; } } else { label_5087:; node1____CPAchecker_TMP_0 = p12_new; goto label_5088; } } else { goto label_5087; } } else { goto label_5081; } } else { goto label_5081; } } 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 { goto label_4998; } } else { goto label_4998; } } else { goto label_4990; } } else { goto label_4990; } } else { goto label_4982; } } else { goto label_4982; } } else { return __return_main; } } } } else { goto label_4962; } } else { goto label_4962; } } else { goto label_4954; } } else { goto label_4954; } } else { goto label_4946; } } else { goto label_4946; } } else { return __return_main; } } } } else { goto label_4926; } } else { goto label_4926; } } else { goto label_4918; } } else { goto label_4918; } } else { goto label_4910; } } else { goto label_4910; } } else { return __return_main; } } } } else { goto label_4890; } } else { goto label_4890; } } else { goto label_4882; } } else { goto label_4882; } } else { goto label_4874; } } else { goto label_4874; } } 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 { label_4797:; node4____CPAchecker_TMP_2 = p43_new; goto label_4798; } } else { goto label_4797; } } else { goto label_4800; } } else { goto label_4800; } } else { label_4787:; node4____CPAchecker_TMP_1 = p42_new; goto label_4788; } } else { goto label_4787; } } else { goto label_4781; } } else { goto label_4781; } } else { label_4777:; node4____CPAchecker_TMP_0 = p41_new; goto label_4778; } } else { goto label_4777; } } else { goto label_4771; } } else { goto label_4771; } } else { return __return_main; } } } } else { label_4757:; node3____CPAchecker_TMP_2 = p34_new; goto label_4758; } } else { goto label_4757; } } else { goto label_4760; } } else { goto label_4760; } } else { label_4747:; node3____CPAchecker_TMP_1 = p32_new; goto label_4748; } } else { goto label_4747; } } else { goto label_4741; } } else { goto label_4741; } } else { label_4737:; node3____CPAchecker_TMP_0 = p31_new; goto label_4738; } } else { goto label_4737; } } else { goto label_4731; } } else { goto label_4731; } } else { return __return_main; } } } } else { label_4717:; node2____CPAchecker_TMP_2 = p24_new; goto label_4718; } } else { goto label_4717; } } else { goto label_4720; } } else { goto label_4720; } } else { label_4707:; node2____CPAchecker_TMP_1 = p23_new; goto label_4708; } } else { goto label_4707; } } else { goto label_4701; } } else { goto label_4701; } } else { label_4697:; node2____CPAchecker_TMP_0 = p21_new; goto label_4698; } } else { goto label_4697; } } else { goto label_4691; } } else { goto label_4691; } } else { return __return_main; } } } } else { label_4677:; node1____CPAchecker_TMP_2 = p14_new; goto label_4678; } } else { goto label_4677; } } else { goto label_4680; } } else { goto label_4680; } } else { label_4667:; node1____CPAchecker_TMP_1 = p13_new; goto label_4668; } } else { goto label_4667; } } else { goto label_4661; } } else { goto label_4661; } } else { label_4657:; node1____CPAchecker_TMP_0 = p12_new; goto label_4658; } } else { goto label_4657; } } else { goto label_4651; } } else { goto label_4651; } } 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 { return __return_main; } } else { if (!(init__r412 == 0)) { if (!(ep13 == 0)) { init__tmp___22 = 1; goto label_4519; } else { label_7490:; if (!(init__r422 == 0)) { if (!(ep23 == 0)) { init__tmp___22 = 1; label_7496:; goto label_4519; } else { init__tmp___22 = 0; goto label_7496; } } else { init__tmp___22 = 0; goto label_4519; } } } else { goto label_7490; } } } else { if (!(init__r412 == 0)) { if (!(ep12 == 0)) { init__tmp___21 = 1; goto label_4514; } else { label_7505:; if (!(init__r432 == 0)) { if (!(ep32 == 0)) { init__tmp___21 = 1; label_7511:; goto label_4514; } else { init__tmp___21 = 0; goto label_7511; } } else { init__tmp___21 = 0; goto label_4514; } } } else { goto label_7505; } } } else { if (!(init__r422 == 0)) { if (!(ep21 == 0)) { init__tmp___20 = 1; goto label_4509; } else { label_7520:; if (!(init__r432 == 0)) { if (!(ep31 == 0)) { init__tmp___20 = 1; label_7526:; goto label_4509; } else { init__tmp___20 = 0; goto label_7526; } } else { init__tmp___20 = 0; goto label_4509; } } } else { goto label_7520; } } } else { if (!(init__r312 == 0)) { if (!(ep14 == 0)) { init__tmp___19 = 1; goto label_4504; } else { label_7535:; if (!(init__r322 == 0)) { if (!(ep24 == 0)) { init__tmp___19 = 1; label_7541:; goto label_4504; } else { init__tmp___19 = 0; goto label_7541; } } else { init__tmp___19 = 0; goto label_4504; } } } else { goto label_7535; } } } else { if (!(init__r312 == 0)) { if (!(ep12 == 0)) { init__tmp___18 = 1; goto label_4499; } else { label_7550:; if (!(init__r342 == 0)) { if (!(ep42 == 0)) { init__tmp___18 = 1; label_7556:; goto label_4499; } else { init__tmp___18 = 0; goto label_7556; } } else { init__tmp___18 = 0; goto label_4499; } } } else { goto label_7550; } } } else { if (!(init__r322 == 0)) { if (!(ep21 == 0)) { init__tmp___17 = 1; goto label_4494; } else { label_7565:; if (!(init__r342 == 0)) { if (!(ep41 == 0)) { init__tmp___17 = 1; label_7571:; goto label_4494; } else { init__tmp___17 = 0; goto label_7571; } } else { init__tmp___17 = 0; goto label_4494; } } } else { goto label_7565; } } } else { if (!(init__r212 == 0)) { if (!(ep14 == 0)) { init__tmp___16 = 1; goto label_4489; } else { label_7580:; if (!(init__r232 == 0)) { if (!(ep34 == 0)) { init__tmp___16 = 1; label_7586:; goto label_4489; } else { init__tmp___16 = 0; goto label_7586; } } else { init__tmp___16 = 0; goto label_4489; } } } else { goto label_7580; } } } else { if (!(init__r212 == 0)) { if (!(ep13 == 0)) { init__tmp___15 = 1; goto label_4484; } else { label_7595:; if (!(init__r242 == 0)) { if (!(ep43 == 0)) { init__tmp___15 = 1; label_7601:; goto label_4484; } else { init__tmp___15 = 0; goto label_7601; } } else { init__tmp___15 = 0; goto label_4484; } } } else { goto label_7595; } } } else { if (!(init__r232 == 0)) { if (!(ep31 == 0)) { init__tmp___14 = 1; goto label_4479; } else { label_7610:; if (!(init__r242 == 0)) { if (!(ep41 == 0)) { init__tmp___14 = 1; label_7616:; goto label_4479; } else { init__tmp___14 = 0; goto label_7616; } } else { init__tmp___14 = 0; goto label_4479; } } } else { goto label_7610; } } } else { if (!(init__r122 == 0)) { if (!(ep24 == 0)) { init__tmp___13 = 1; goto label_4474; } else { label_7625:; if (!(init__r132 == 0)) { if (!(ep34 == 0)) { init__tmp___13 = 1; label_7631:; goto label_4474; } else { init__tmp___13 = 0; goto label_7631; } } else { init__tmp___13 = 0; goto label_4474; } } } else { goto label_7625; } } } else { if (!(init__r122 == 0)) { if (!(ep23 == 0)) { init__tmp___12 = 1; goto label_4469; } else { label_7640:; if (!(init__r142 == 0)) { if (!(ep43 == 0)) { init__tmp___12 = 1; label_7646:; goto label_4469; } else { init__tmp___12 = 0; goto label_7646; } } else { init__tmp___12 = 0; goto label_4469; } } } else { goto label_7640; } } } else { if (!(init__r132 == 0)) { if (!(ep32 == 0)) { init__tmp___11 = 1; goto label_4464; } else { label_7655:; if (!(init__r142 == 0)) { if (!(ep42 == 0)) { init__tmp___11 = 1; label_7661:; goto label_4464; } else { init__tmp___11 = 0; goto label_7661; } } else { init__tmp___11 = 0; goto label_4464; } } } else { goto label_7655; } } } else { if (!(init__r411 == 0)) { if (!(ep13 == 0)) { init__tmp___10 = 1; goto label_4459; } else { label_7670:; if (!(init__r421 == 0)) { if (!(ep23 == 0)) { init__tmp___10 = 1; label_7676:; goto label_4459; } else { init__tmp___10 = 0; goto label_7676; } } else { init__tmp___10 = 0; goto label_4459; } } } else { goto label_7670; } } } else { if (!(init__r411 == 0)) { if (!(ep12 == 0)) { init__tmp___9 = 1; goto label_4454; } else { label_7685:; if (!(init__r431 == 0)) { if (!(ep32 == 0)) { init__tmp___9 = 1; label_7691:; goto label_4454; } else { init__tmp___9 = 0; goto label_7691; } } else { init__tmp___9 = 0; goto label_4454; } } } else { goto label_7685; } } } else { if (!(init__r421 == 0)) { if (!(ep21 == 0)) { init__tmp___8 = 1; goto label_4449; } else { label_7700:; if (!(init__r431 == 0)) { if (!(ep31 == 0)) { init__tmp___8 = 1; label_7706:; goto label_4449; } else { init__tmp___8 = 0; goto label_7706; } } else { init__tmp___8 = 0; goto label_4449; } } } else { goto label_7700; } } } else { if (!(init__r311 == 0)) { if (!(ep14 == 0)) { init__tmp___7 = 1; goto label_4444; } else { label_7715:; if (!(init__r321 == 0)) { if (!(ep24 == 0)) { init__tmp___7 = 1; label_7721:; goto label_4444; } else { init__tmp___7 = 0; goto label_7721; } } else { init__tmp___7 = 0; goto label_4444; } } } else { goto label_7715; } } } else { if (!(init__r311 == 0)) { if (!(ep12 == 0)) { init__tmp___6 = 1; goto label_4439; } else { label_7730:; if (!(init__r341 == 0)) { if (!(ep42 == 0)) { init__tmp___6 = 1; label_7736:; goto label_4439; } else { init__tmp___6 = 0; goto label_7736; } } else { init__tmp___6 = 0; goto label_4439; } } } else { goto label_7730; } } } else { if (!(init__r321 == 0)) { if (!(ep21 == 0)) { init__tmp___5 = 1; goto label_4434; } else { label_7745:; if (!(init__r341 == 0)) { if (!(ep41 == 0)) { init__tmp___5 = 1; label_7751:; goto label_4434; } else { init__tmp___5 = 0; goto label_7751; } } else { init__tmp___5 = 0; goto label_4434; } } } else { goto label_7745; } } } else { if (!(init__r211 == 0)) { if (!(ep14 == 0)) { init__tmp___4 = 1; goto label_4429; } else { label_7760:; if (!(init__r231 == 0)) { if (!(ep34 == 0)) { init__tmp___4 = 1; label_7766:; goto label_4429; } else { init__tmp___4 = 0; goto label_7766; } } else { init__tmp___4 = 0; goto label_4429; } } } else { goto label_7760; } } } else { if (!(init__r211 == 0)) { if (!(ep13 == 0)) { init__tmp___3 = 1; goto label_4424; } else { label_7775:; if (!(init__r241 == 0)) { if (!(ep43 == 0)) { init__tmp___3 = 1; label_7781:; goto label_4424; } else { init__tmp___3 = 0; goto label_7781; } } else { init__tmp___3 = 0; goto label_4424; } } } else { goto label_7775; } } } else { if (!(init__r231 == 0)) { if (!(ep31 == 0)) { init__tmp___2 = 1; goto label_4419; } else { label_7790:; if (!(init__r241 == 0)) { if (!(ep41 == 0)) { init__tmp___2 = 1; label_7796:; goto label_4419; } else { init__tmp___2 = 0; goto label_7796; } } else { init__tmp___2 = 0; goto label_4419; } } } else { goto label_7790; } } } else { if (!(init__r121 == 0)) { if (!(ep24 == 0)) { init__tmp___1 = 1; goto label_4414; } else { label_7805:; if (!(init__r131 == 0)) { if (!(ep34 == 0)) { init__tmp___1 = 1; label_7811:; goto label_4414; } else { init__tmp___1 = 0; goto label_7811; } } else { init__tmp___1 = 0; goto label_4414; } } } else { goto label_7805; } } } else { if (!(init__r121 == 0)) { if (!(ep23 == 0)) { init__tmp___0 = 1; goto label_4409; } else { label_7820:; if (!(init__r141 == 0)) { if (!(ep43 == 0)) { init__tmp___0 = 1; label_7826:; goto label_4409; } else { init__tmp___0 = 0; goto label_7826; } } else { init__tmp___0 = 0; goto label_4409; } } } else { goto label_7820; } } } else { if (!(init__r131 == 0)) { if (!(ep32 == 0)) { init__tmp = 1; goto label_4404; } else { label_7835:; if (!(init__r141 == 0)) { if (!(ep42 == 0)) { init__tmp = 1; label_7841:; goto label_4404; } else { init__tmp = 0; goto label_7841; } } else { init__tmp = 0; goto label_4404; } } } else { goto label_7835; } } } }