// This file is part of the SV-Benchmarks collection of verification tasks: // https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks // // SPDX-FileCopyrightText: 2013 Carnegie Mellon University // SPDX-FileCopyrightText: 2014-2021 The SV-Benchmarks Community // SPDX-FileCopyrightText: 2018 Marie-Christine Jakobs, LMU Munich // // SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU-LMU int __return_main; void abort(void); extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); void reach_error() { __assert_fail("0", "pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c", 4, "reach_error"); } char __VERIFIER_nondet_char(); _Bool __VERIFIER_nondet_bool(); void assert(_Bool arg); void abort(void); void assume_abort_if_not(int cond) { if(!cond) {abort();} } typedef char msg_t; typedef int port_t; void read(port_t p, msg_t m); void write(port_t p, msg_t m); msg_t nomsg = (msg_t )-1; port_t p12 = 0; char p12_old = '\x0'; char p12_new = '\x0'; _Bool ep12 = 0; port_t p13 = 0; char p13_old = '\x0'; char p13_new = '\x0'; _Bool ep13 = 0; port_t p14 = 0; char p14_old = '\x0'; char p14_new = '\x0'; _Bool ep14 = 0; port_t p21 = 0; char p21_old = '\x0'; char p21_new = '\x0'; _Bool ep21 = 0; port_t p23 = 0; char p23_old = '\x0'; char p23_new = '\x0'; _Bool ep23 = 0; port_t p24 = 0; char p24_old = '\x0'; char p24_new = '\x0'; _Bool ep24 = 0; port_t p31 = 0; char p31_old = '\x0'; char p31_new = '\x0'; _Bool ep31 = 0; port_t p32 = 0; char p32_old = '\x0'; char p32_new = '\x0'; _Bool ep32 = 0; port_t p34 = 0; char p34_old = '\x0'; char p34_new = '\x0'; _Bool ep34 = 0; port_t p41 = 0; char p41_old = '\x0'; char p41_new = '\x0'; _Bool ep41 = 0; port_t p42 = 0; char p42_old = '\x0'; char p42_new = '\x0'; _Bool ep42 = 0; port_t p43 = 0; char p43_old = '\x0'; char p43_new = '\x0'; _Bool ep43 = 0; char id1 = '\x0'; char r1 = '\x0'; char st1 = '\x0'; char nl1 = '\x0'; char m1 = '\x0'; char max1 = '\x0'; _Bool mode1 = 0; char id2 = '\x0'; char r2 = '\x0'; char st2 = '\x0'; char nl2 = '\x0'; char m2 = '\x0'; char max2 = '\x0'; _Bool mode2 = 0; char id3 = '\x0'; char r3 = '\x0'; char st3 = '\x0'; char nl3 = '\x0'; char m3 = '\x0'; char max3 = '\x0'; _Bool mode3 = 0; char id4 = '\x0'; char r4 = '\x0'; char st4 = '\x0'; char nl4 = '\x0'; char m4 = '\x0'; char max4 = '\x0'; _Bool mode4 = 0; void node1(); void node2(); void node3(); void node4(); void (*nodes[4])() = { &node1, &node2, &node3, &node4 }; int init(); int check(); int main(); int __return_4261; int __return_4471; int __return_4654; int __return_4845; int __return_5028; int __return_5195; int __return_5387; int __tmp_5388_0; int __return_5561; int __return_5401; int main() { int main__c1; int main__i2; main__c1 = 0; ep12 = __VERIFIER_nondet_bool(); ep13 = __VERIFIER_nondet_bool(); ep14 = __VERIFIER_nondet_bool(); ep21 = __VERIFIER_nondet_bool(); ep23 = __VERIFIER_nondet_bool(); ep24 = __VERIFIER_nondet_bool(); ep31 = __VERIFIER_nondet_bool(); ep32 = __VERIFIER_nondet_bool(); ep34 = __VERIFIER_nondet_bool(); ep41 = __VERIFIER_nondet_bool(); ep42 = __VERIFIER_nondet_bool(); ep43 = __VERIFIER_nondet_bool(); id1 = __VERIFIER_nondet_char(); r1 = __VERIFIER_nondet_char(); st1 = __VERIFIER_nondet_char(); nl1 = __VERIFIER_nondet_char(); m1 = __VERIFIER_nondet_char(); max1 = __VERIFIER_nondet_char(); mode1 = __VERIFIER_nondet_bool(); id2 = __VERIFIER_nondet_char(); r2 = __VERIFIER_nondet_char(); st2 = __VERIFIER_nondet_char(); nl2 = __VERIFIER_nondet_char(); m2 = __VERIFIER_nondet_char(); max2 = __VERIFIER_nondet_char(); mode2 = __VERIFIER_nondet_bool(); id3 = __VERIFIER_nondet_char(); r3 = __VERIFIER_nondet_char(); st3 = __VERIFIER_nondet_char(); nl3 = __VERIFIER_nondet_char(); m3 = __VERIFIER_nondet_char(); max3 = __VERIFIER_nondet_char(); mode3 = __VERIFIER_nondet_bool(); id4 = __VERIFIER_nondet_char(); r4 = __VERIFIER_nondet_char(); st4 = __VERIFIER_nondet_char(); nl4 = __VERIFIER_nondet_char(); m4 = __VERIFIER_nondet_char(); max4 = __VERIFIER_nondet_char(); mode4 = __VERIFIER_nondet_bool(); { _Bool init__r121; _Bool init__r131; _Bool init__r141; _Bool init__r211; _Bool init__r231; _Bool init__r241; _Bool init__r311; _Bool init__r321; _Bool init__r341; _Bool init__r411; _Bool init__r421; _Bool init__r431; _Bool init__r122; int init__tmp; _Bool init__r132; int init__tmp___0; _Bool init__r142; int init__tmp___1; _Bool init__r212; int init__tmp___2; _Bool init__r232; int init__tmp___3; _Bool init__r242; int init__tmp___4; _Bool init__r312; int init__tmp___5; _Bool init__r322; int init__tmp___6; _Bool init__r342; int init__tmp___7; _Bool init__r412; int init__tmp___8; _Bool init__r422; int init__tmp___9; _Bool init__r432; int init__tmp___10; _Bool init__r123; int init__tmp___11; _Bool init__r133; int init__tmp___12; _Bool init__r143; int init__tmp___13; _Bool init__r213; int init__tmp___14; _Bool init__r233; int init__tmp___15; _Bool init__r243; int init__tmp___16; _Bool init__r313; int init__tmp___17; _Bool init__r323; int init__tmp___18; _Bool init__r343; int init__tmp___19; _Bool init__r413; int init__tmp___20; _Bool init__r423; int init__tmp___21; _Bool init__r433; int init__tmp___22; int init__tmp___23; init__r121 = ep12; init__r131 = ep13; init__r141 = ep14; init__r211 = ep21; init__r231 = ep23; init__r241 = ep24; init__r311 = ep31; init__r321 = ep32; init__r341 = ep34; init__r411 = ep41; init__r421 = ep42; init__r431 = ep43; if (!(init__r121 == 0)) { init__tmp = 1; label_4059:; init__r122 = (_Bool)init__tmp; if (!(init__r131 == 0)) { init__tmp___0 = 1; label_4064:; init__r132 = (_Bool)init__tmp___0; if (!(init__r141 == 0)) { init__tmp___1 = 1; label_4069:; init__r142 = (_Bool)init__tmp___1; if (!(init__r211 == 0)) { init__tmp___2 = 1; label_4074:; init__r212 = (_Bool)init__tmp___2; if (!(init__r231 == 0)) { init__tmp___3 = 1; label_4079:; init__r232 = (_Bool)init__tmp___3; if (!(init__r241 == 0)) { init__tmp___4 = 1; label_4084:; init__r242 = (_Bool)init__tmp___4; if (!(init__r311 == 0)) { init__tmp___5 = 1; label_4089:; init__r312 = (_Bool)init__tmp___5; if (!(init__r321 == 0)) { init__tmp___6 = 1; label_4094:; init__r322 = (_Bool)init__tmp___6; if (!(init__r341 == 0)) { init__tmp___7 = 1; label_4099:; init__r342 = (_Bool)init__tmp___7; if (!(init__r411 == 0)) { init__tmp___8 = 1; label_4104:; init__r412 = (_Bool)init__tmp___8; if (!(init__r421 == 0)) { init__tmp___9 = 1; label_4109:; init__r422 = (_Bool)init__tmp___9; if (!(init__r431 == 0)) { init__tmp___10 = 1; label_4114:; init__r432 = (_Bool)init__tmp___10; if (!(init__r122 == 0)) { init__tmp___11 = 1; label_4119:; init__r123 = (_Bool)init__tmp___11; if (!(init__r132 == 0)) { init__tmp___12 = 1; label_4124:; init__r133 = (_Bool)init__tmp___12; if (!(init__r142 == 0)) { init__tmp___13 = 1; label_4129:; init__r143 = (_Bool)init__tmp___13; if (!(init__r212 == 0)) { init__tmp___14 = 1; label_4134:; init__r213 = (_Bool)init__tmp___14; if (!(init__r232 == 0)) { init__tmp___15 = 1; label_4139:; init__r233 = (_Bool)init__tmp___15; if (!(init__r242 == 0)) { init__tmp___16 = 1; label_4144:; init__r243 = (_Bool)init__tmp___16; if (!(init__r312 == 0)) { init__tmp___17 = 1; label_4149:; init__r313 = (_Bool)init__tmp___17; if (!(init__r322 == 0)) { init__tmp___18 = 1; label_4154:; init__r323 = (_Bool)init__tmp___18; if (!(init__r342 == 0)) { init__tmp___19 = 1; label_4159:; init__r343 = (_Bool)init__tmp___19; if (!(init__r412 == 0)) { init__tmp___20 = 1; label_4164:; init__r413 = (_Bool)init__tmp___20; if (!(init__r422 == 0)) { init__tmp___21 = 1; label_4169:; init__r423 = (_Bool)init__tmp___21; if (!(init__r432 == 0)) { init__tmp___22 = 1; label_4174:; init__r433 = (_Bool)init__tmp___22; if (((int)id1) != ((int)id2)) { if (((int)id1) != ((int)id3)) { if (((int)id1) != ((int)id4)) { if (((int)id2) != ((int)id3)) { if (((int)id2) != ((int)id4)) { if (((int)id3) != ((int)id4)) { if (((int)id1) >= 0) { if (((int)id2) >= 0) { if (((int)id3) >= 0) { if (((int)id4) >= 0) { if (((int)r1) == 0) { if (((int)r2) == 0) { if (((int)r3) == 0) { if (((int)r4) == 0) { if (!(init__r123 == 0)) { if (!(init__r133 == 0)) { if (!(init__r143 == 0)) { if (!(init__r213 == 0)) { if (!(init__r233 == 0)) { if (!(init__r243 == 0)) { if (!(init__r313 == 0)) { if (!(init__r323 == 0)) { if (!(init__r343 == 0)) { if (!(init__r413 == 0)) { if (!(init__r423 == 0)) { if (!(init__r433 == 0)) { if (((int)max1) == ((int)id1)) { if (((int)max2) == ((int)id2)) { if (((int)max3) == ((int)id3)) { if (((int)max4) == ((int)id4)) { if (((int)st1) == 0) { if (((int)st2) == 0) { if (((int)st3) == 0) { if (((int)st4) == 0) { if (((int)nl1) == 0) { if (((int)nl2) == 0) { if (((int)nl3) == 0) { if (((int)nl4) == 0) { if (((int)mode1) == 0) { if (((int)mode2) == 0) { if (((int)mode3) == 0) { if (((int)mode4) == 0) { init__tmp___23 = 1; __return_4261 = init__tmp___23; main__i2 = __return_4261; if (main__i2 != 0) { p12_old = nomsg; p12_new = nomsg; p13_old = nomsg; p13_new = nomsg; p14_old = nomsg; p14_new = nomsg; p21_old = nomsg; p21_new = nomsg; p23_old = nomsg; p23_new = nomsg; p24_old = nomsg; p24_new = nomsg; p31_old = nomsg; p31_new = nomsg; p32_old = nomsg; p32_new = nomsg; p34_old = nomsg; p34_new = nomsg; p41_old = nomsg; p41_new = nomsg; p42_old = nomsg; p42_new = nomsg; p43_old = nomsg; p43_new = nomsg; main__i2 = 0; if (main__i2 < 8) { { if (!(mode1 == 0)) { return __return_main; } else { if (((int)r1) < 2) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_4301:; p12_new = node1____CPAchecker_TMP_0; label_4296:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4309:; p13_new = node1____CPAchecker_TMP_1; label_4304:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4317:; p14_new = node1____CPAchecker_TMP_2; label_4319:; mode1 = 1; { if (!(mode2 == 0)) { return __return_main; } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_4333:; p21_new = node2____CPAchecker_TMP_0; label_4328:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4341:; p23_new = node2____CPAchecker_TMP_1; label_4336:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4349:; p24_new = node2____CPAchecker_TMP_2; label_4351:; mode2 = 1; { if (!(mode3 == 0)) { return __return_main; } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_4365:; p31_new = node3____CPAchecker_TMP_0; label_4360:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4373:; p32_new = node3____CPAchecker_TMP_1; label_4368:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4381:; p34_new = node3____CPAchecker_TMP_2; label_4383:; mode3 = 1; { if (!(mode4 == 0)) { return __return_main; } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_4397:; p41_new = node4____CPAchecker_TMP_0; label_4392:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4405:; p42_new = node4____CPAchecker_TMP_1; label_4400:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4413:; p43_new = node4____CPAchecker_TMP_2; label_4415:; 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_4471 = check__tmp; main__c1 = __return_4471; { _Bool __tmp_1; __tmp_1 = main__c1; _Bool assert__arg; assert__arg = __tmp_1; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4487:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4494:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4501:; if (((int)r1) == 3) { return __return_main; } else { mode1 = 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; label_4517:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4524:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4531:; if (((int)r2) == 3) { return __return_main; } else { mode2 = 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; label_4547:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4554:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4561:; if (((int)r3) == 3) { return __return_main; } else { mode3 = 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; label_4577:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4584:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4591:; 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_4654 = check__tmp; main__c1 = __return_4654; { _Bool __tmp_2; __tmp_2 = main__c1; _Bool assert__arg; assert__arg = __tmp_2; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { return __return_main; } else { if (((int)r1) < 2) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_4675:; p12_new = node1____CPAchecker_TMP_0; label_4670:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4683:; p13_new = node1____CPAchecker_TMP_1; label_4678:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4691:; p14_new = node1____CPAchecker_TMP_2; label_4693:; mode1 = 1; { if (!(mode2 == 0)) { return __return_main; } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_4707:; p21_new = node2____CPAchecker_TMP_0; label_4702:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4715:; p23_new = node2____CPAchecker_TMP_1; label_4710:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4723:; p24_new = node2____CPAchecker_TMP_2; label_4725:; mode2 = 1; { if (!(mode3 == 0)) { return __return_main; } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_4739:; p31_new = node3____CPAchecker_TMP_0; label_4734:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4747:; p32_new = node3____CPAchecker_TMP_1; label_4742:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4755:; p34_new = node3____CPAchecker_TMP_2; label_4757:; mode3 = 1; { if (!(mode4 == 0)) { return __return_main; } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_4771:; p41_new = node4____CPAchecker_TMP_0; label_4766:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4779:; p42_new = node4____CPAchecker_TMP_1; label_4774:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4787:; p43_new = node4____CPAchecker_TMP_2; label_4789:; 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_4845 = check__tmp; main__c1 = __return_4845; { _Bool __tmp_3; __tmp_3 = main__c1; _Bool assert__arg; assert__arg = __tmp_3; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4861:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4868:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4875:; if (((int)r1) == 3) { return __return_main; } else { mode1 = 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; label_4891:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4898:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4905:; if (((int)r2) == 3) { return __return_main; } else { mode2 = 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; label_4921:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4928:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4935:; if (((int)r3) == 3) { return __return_main; } else { mode3 = 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; label_4951:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4958:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4965:; 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_5028 = check__tmp; main__c1 = __return_5028; { _Bool __tmp_4; __tmp_4 = main__c1; _Bool assert__arg; assert__arg = __tmp_4; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { return __return_main; } else { if (((int)r1) < 2) { return __return_main; } else { mode1 = 1; { if (!(mode2 == 0)) { return __return_main; } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_5057:; p21_new = node2____CPAchecker_TMP_0; label_5052:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5065:; p23_new = node2____CPAchecker_TMP_1; label_5060:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5073:; p24_new = node2____CPAchecker_TMP_2; label_5075:; mode2 = 1; { if (!(mode3 == 0)) { return __return_main; } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_5089:; p31_new = node3____CPAchecker_TMP_0; label_5084:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5097:; p32_new = node3____CPAchecker_TMP_1; label_5092:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5105:; p34_new = node3____CPAchecker_TMP_2; label_5107:; mode3 = 1; { if (!(mode4 == 0)) { return __return_main; } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_5121:; p41_new = node4____CPAchecker_TMP_0; label_5116:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5129:; p42_new = node4____CPAchecker_TMP_1; label_5124:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5137:; p43_new = node4____CPAchecker_TMP_2; label_5139:; 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_5195 = check__tmp; main__c1 = __return_5195; { _Bool __tmp_5; __tmp_5 = main__c1; _Bool assert__arg; assert__arg = __tmp_5; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5211:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5218:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5225:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5236:; mode1 = 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; label_5245:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5252:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5259:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5270:; mode2 = 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; label_5279:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5286:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5293:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5304:; mode3 = 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; label_5313:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5320:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5327:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5338:; 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_5742:; if (((int)r1) < 3) { check__tmp = 1; label_5748:; label_5741:; label_5380:; label_5386:; __return_5387 = check__tmp; main__c1 = __return_5387; __tmp_5388_0 = main____CPAchecker_TMP_0; label_5388:; main____CPAchecker_TMP_0 = __tmp_5388_0; { _Bool __tmp_6; __tmp_6 = main__c1; _Bool assert__arg; assert__arg = __tmp_6; 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) { { if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5407:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5414:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5421:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5429:; mode1 = 0; label_5431:; { if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5439:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5446:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5453:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5461:; mode2 = 0; label_5463:; { if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5471:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5478:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5485:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5493:; mode3 = 0; label_5495:; { if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5503:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5510:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5517:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5525:; mode4 = 0; label_5527:; 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_5584:; if (((int)r1) < 3) { label_5591:; if (((int)r1) >= 3) { label_5598:; if (((int)r1) < 3) { check__tmp = 1; label_5604:; label_5597:; label_5590:; label_5583:; label_5577:; label_5573:; label_5569:; label_5565:; label_5560:; __return_5561 = check__tmp; main__c1 = __return_5561; __tmp_5388_0 = main____CPAchecker_TMP_0; goto label_5388; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5604; } else { check__tmp = 0; goto label_5604; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5598; } else { check__tmp = 0; goto label_5597; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_5591; } else { check__tmp = 0; goto label_5590; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_5584; } else { check__tmp = 0; goto label_5583; } } } else { check__tmp = 0; goto label_5577; } } else { check__tmp = 0; goto label_5573; } } else { check__tmp = 0; goto label_5569; } } else { check__tmp = 0; goto label_5565; } } else { check__tmp = 0; goto label_5560; } } } else { nl4 = 1; goto label_5525; } } else { goto label_5525; } } else { goto label_5517; } } else { goto label_5517; } } else { goto label_5510; } } else { goto label_5510; } } else { goto label_5503; } } else { goto label_5503; } } else { if (((int)r4) < 3) { if (!(ep41 == 0)) { int node4____CPAchecker_TMP_0; if (max4 != nomsg) { if (p41_new == nomsg) { node4____CPAchecker_TMP_0 = max4; label_5619:; p41_new = node4____CPAchecker_TMP_0; label_5614:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5627:; p42_new = node4____CPAchecker_TMP_1; label_5622:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5635:; p43_new = node4____CPAchecker_TMP_2; label_5612:; mode4 = 1; goto label_5527; } else { label_5634:; node4____CPAchecker_TMP_2 = p43_new; goto label_5635; } } else { goto label_5634; } } else { goto label_5612; } } else { label_5626:; node4____CPAchecker_TMP_1 = p42_new; goto label_5627; } } else { goto label_5626; } } else { goto label_5622; } } else { label_5618:; node4____CPAchecker_TMP_0 = p41_new; goto label_5619; } } else { goto label_5618; } } else { goto label_5614; } } else { goto label_5612; } } } } else { nl3 = 1; goto label_5493; } } else { goto label_5493; } } else { goto label_5485; } } else { goto label_5485; } } else { goto label_5478; } } else { goto label_5478; } } else { goto label_5471; } } else { goto label_5471; } } else { if (((int)r3) < 3) { if (!(ep31 == 0)) { int node3____CPAchecker_TMP_0; if (max3 != nomsg) { if (p31_new == nomsg) { node3____CPAchecker_TMP_0 = max3; label_5650:; p31_new = node3____CPAchecker_TMP_0; label_5645:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5658:; p32_new = node3____CPAchecker_TMP_1; label_5653:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5666:; p34_new = node3____CPAchecker_TMP_2; label_5643:; mode3 = 1; goto label_5495; } else { label_5665:; node3____CPAchecker_TMP_2 = p34_new; goto label_5666; } } else { goto label_5665; } } else { goto label_5643; } } else { label_5657:; node3____CPAchecker_TMP_1 = p32_new; goto label_5658; } } else { goto label_5657; } } else { goto label_5653; } } else { label_5649:; node3____CPAchecker_TMP_0 = p31_new; goto label_5650; } } else { goto label_5649; } } else { goto label_5645; } } else { goto label_5643; } } } } else { nl2 = 1; goto label_5461; } } else { goto label_5461; } } else { goto label_5453; } } else { goto label_5453; } } else { goto label_5446; } } else { goto label_5446; } } else { goto label_5439; } } else { goto label_5439; } } else { if (((int)r2) < 3) { if (!(ep21 == 0)) { int node2____CPAchecker_TMP_0; if (max2 != nomsg) { if (p21_new == nomsg) { node2____CPAchecker_TMP_0 = max2; label_5681:; p21_new = node2____CPAchecker_TMP_0; label_5676:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5689:; p23_new = node2____CPAchecker_TMP_1; label_5684:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5697:; p24_new = node2____CPAchecker_TMP_2; label_5674:; mode2 = 1; goto label_5463; } else { label_5696:; node2____CPAchecker_TMP_2 = p24_new; goto label_5697; } } else { goto label_5696; } } else { goto label_5674; } } else { label_5688:; node2____CPAchecker_TMP_1 = p23_new; goto label_5689; } } else { goto label_5688; } } else { goto label_5684; } } else { label_5680:; node2____CPAchecker_TMP_0 = p21_new; goto label_5681; } } else { goto label_5680; } } else { goto label_5676; } } else { goto label_5674; } } } } else { nl1 = 1; goto label_5429; } } else { goto label_5429; } } else { goto label_5421; } } else { goto label_5421; } } else { goto label_5414; } } else { goto label_5414; } } else { goto label_5407; } } else { goto label_5407; } } else { if (((int)r1) < 2) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_5712:; p12_new = node1____CPAchecker_TMP_0; label_5707:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5720:; p13_new = node1____CPAchecker_TMP_1; label_5715:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5728:; p14_new = node1____CPAchecker_TMP_2; label_5705:; mode1 = 1; goto label_5431; } else { label_5727:; node1____CPAchecker_TMP_2 = p14_new; goto label_5728; } } else { goto label_5727; } } else { goto label_5705; } } else { label_5719:; node1____CPAchecker_TMP_1 = p13_new; goto label_5720; } } else { goto label_5719; } } else { goto label_5715; } } else { label_5711:; node1____CPAchecker_TMP_0 = p12_new; goto label_5712; } } else { goto label_5711; } } else { goto label_5707; } } else { goto label_5705; } } } } else { __return_5401 = 0; return __return_5401; } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5748; } else { check__tmp = 0; goto label_5748; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5742; } else { check__tmp = 0; goto label_5741; } } } else { check__tmp = 0; goto label_5380; } } } 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_5386; } } } else { nl4 = 1; goto label_5338; } } else { return __return_main; } } else { goto label_5327; } } else { goto label_5327; } } else { goto label_5320; } } else { goto label_5320; } } else { goto label_5313; } } else { goto label_5313; } } else { return __return_main; } } } else { nl3 = 1; goto label_5304; } } else { return __return_main; } } else { goto label_5293; } } else { goto label_5293; } } else { goto label_5286; } } else { goto label_5286; } } else { goto label_5279; } } else { goto label_5279; } } else { return __return_main; } } } else { nl2 = 1; goto label_5270; } } else { return __return_main; } } else { goto label_5259; } } else { goto label_5259; } } else { goto label_5252; } } else { goto label_5252; } } else { goto label_5245; } } else { goto label_5245; } } else { return __return_main; } } } else { nl1 = 1; goto label_5236; } } else { return __return_main; } } else { goto label_5225; } } else { goto label_5225; } } else { goto label_5218; } } else { goto label_5218; } } else { goto label_5211; } } else { goto label_5211; } } 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_5136:; node4____CPAchecker_TMP_2 = p43_new; goto label_5137; } } else { goto label_5136; } } else { goto label_5139; } } else { label_5128:; node4____CPAchecker_TMP_1 = p42_new; goto label_5129; } } else { goto label_5128; } } else { goto label_5124; } } else { label_5120:; node4____CPAchecker_TMP_0 = p41_new; goto label_5121; } } else { goto label_5120; } } else { goto label_5116; } } else { return __return_main; } } } } else { label_5104:; node3____CPAchecker_TMP_2 = p34_new; goto label_5105; } } else { goto label_5104; } } else { goto label_5107; } } else { label_5096:; node3____CPAchecker_TMP_1 = p32_new; goto label_5097; } } else { goto label_5096; } } else { goto label_5092; } } else { label_5088:; node3____CPAchecker_TMP_0 = p31_new; goto label_5089; } } else { goto label_5088; } } else { goto label_5084; } } else { return __return_main; } } } } else { label_5072:; node2____CPAchecker_TMP_2 = p24_new; goto label_5073; } } else { goto label_5072; } } else { goto label_5075; } } else { label_5064:; node2____CPAchecker_TMP_1 = p23_new; goto label_5065; } } else { goto label_5064; } } else { goto label_5060; } } else { label_5056:; node2____CPAchecker_TMP_0 = p21_new; goto label_5057; } } else { goto label_5056; } } else { goto label_5052; } } 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_4965; } } else { goto label_4965; } } else { goto label_4958; } } else { goto label_4958; } } else { goto label_4951; } } else { goto label_4951; } } else { return __return_main; } } } } else { goto label_4935; } } else { goto label_4935; } } else { goto label_4928; } } else { goto label_4928; } } else { goto label_4921; } } else { goto label_4921; } } else { return __return_main; } } } } else { goto label_4905; } } else { goto label_4905; } } else { goto label_4898; } } else { goto label_4898; } } else { goto label_4891; } } else { goto label_4891; } } else { return __return_main; } } } } else { goto label_4875; } } else { goto label_4875; } } else { goto label_4868; } } else { goto label_4868; } } else { goto label_4861; } } else { goto label_4861; } } 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_4786:; node4____CPAchecker_TMP_2 = p43_new; goto label_4787; } } else { goto label_4786; } } else { goto label_4789; } } else { label_4778:; node4____CPAchecker_TMP_1 = p42_new; goto label_4779; } } else { goto label_4778; } } else { goto label_4774; } } else { label_4770:; node4____CPAchecker_TMP_0 = p41_new; goto label_4771; } } else { goto label_4770; } } else { goto label_4766; } } else { return __return_main; } } } } else { label_4754:; node3____CPAchecker_TMP_2 = p34_new; goto label_4755; } } else { goto label_4754; } } else { goto label_4757; } } else { label_4746:; node3____CPAchecker_TMP_1 = p32_new; goto label_4747; } } else { goto label_4746; } } else { goto label_4742; } } else { label_4738:; node3____CPAchecker_TMP_0 = p31_new; goto label_4739; } } else { goto label_4738; } } else { goto label_4734; } } else { return __return_main; } } } } else { label_4722:; node2____CPAchecker_TMP_2 = p24_new; goto label_4723; } } else { goto label_4722; } } else { goto label_4725; } } else { label_4714:; node2____CPAchecker_TMP_1 = p23_new; goto label_4715; } } else { goto label_4714; } } else { goto label_4710; } } else { label_4706:; node2____CPAchecker_TMP_0 = p21_new; goto label_4707; } } else { goto label_4706; } } else { goto label_4702; } } else { return __return_main; } } } } else { label_4690:; node1____CPAchecker_TMP_2 = p14_new; goto label_4691; } } else { goto label_4690; } } else { goto label_4693; } } else { label_4682:; node1____CPAchecker_TMP_1 = p13_new; goto label_4683; } } else { goto label_4682; } } else { goto label_4678; } } else { label_4674:; node1____CPAchecker_TMP_0 = p12_new; goto label_4675; } } else { goto label_4674; } } else { goto label_4670; } } 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_4591; } } else { goto label_4591; } } else { goto label_4584; } } else { goto label_4584; } } else { goto label_4577; } } else { goto label_4577; } } else { return __return_main; } } } } else { goto label_4561; } } else { goto label_4561; } } else { goto label_4554; } } else { goto label_4554; } } else { goto label_4547; } } else { goto label_4547; } } else { return __return_main; } } } } else { goto label_4531; } } else { goto label_4531; } } else { goto label_4524; } } else { goto label_4524; } } else { goto label_4517; } } else { goto label_4517; } } else { return __return_main; } } } } else { goto label_4501; } } else { goto label_4501; } } else { goto label_4494; } } else { goto label_4494; } } else { goto label_4487; } } else { goto label_4487; } } 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_4412:; node4____CPAchecker_TMP_2 = p43_new; goto label_4413; } } else { goto label_4412; } } else { goto label_4415; } } else { label_4404:; node4____CPAchecker_TMP_1 = p42_new; goto label_4405; } } else { goto label_4404; } } else { goto label_4400; } } else { label_4396:; node4____CPAchecker_TMP_0 = p41_new; goto label_4397; } } else { goto label_4396; } } else { goto label_4392; } } else { return __return_main; } } } } else { label_4380:; node3____CPAchecker_TMP_2 = p34_new; goto label_4381; } } else { goto label_4380; } } else { goto label_4383; } } else { label_4372:; node3____CPAchecker_TMP_1 = p32_new; goto label_4373; } } else { goto label_4372; } } else { goto label_4368; } } else { label_4364:; node3____CPAchecker_TMP_0 = p31_new; goto label_4365; } } else { goto label_4364; } } else { goto label_4360; } } else { return __return_main; } } } } else { label_4348:; node2____CPAchecker_TMP_2 = p24_new; goto label_4349; } } else { goto label_4348; } } else { goto label_4351; } } else { label_4340:; node2____CPAchecker_TMP_1 = p23_new; goto label_4341; } } else { goto label_4340; } } else { goto label_4336; } } else { label_4332:; node2____CPAchecker_TMP_0 = p21_new; goto label_4333; } } else { goto label_4332; } } else { goto label_4328; } } else { return __return_main; } } } } else { label_4316:; node1____CPAchecker_TMP_2 = p14_new; goto label_4317; } } else { goto label_4316; } } else { goto label_4319; } } else { label_4308:; node1____CPAchecker_TMP_1 = p13_new; goto label_4309; } } else { goto label_4308; } } else { goto label_4304; } } else { label_4300:; node1____CPAchecker_TMP_0 = p12_new; goto label_4301; } } else { goto label_4300; } } else { goto label_4296; } } 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_4174; } else { label_5773:; if (!(init__r422 == 0)) { if (!(ep23 == 0)) { init__tmp___22 = 1; label_5779:; goto label_4174; } else { init__tmp___22 = 0; goto label_5779; } } else { init__tmp___22 = 0; goto label_4174; } } } else { goto label_5773; } } } else { if (!(init__r412 == 0)) { if (!(ep12 == 0)) { init__tmp___21 = 1; goto label_4169; } else { label_5788:; if (!(init__r432 == 0)) { if (!(ep32 == 0)) { init__tmp___21 = 1; label_5794:; goto label_4169; } else { init__tmp___21 = 0; goto label_5794; } } else { init__tmp___21 = 0; goto label_4169; } } } else { goto label_5788; } } } else { if (!(init__r422 == 0)) { if (!(ep21 == 0)) { init__tmp___20 = 1; goto label_4164; } else { label_5803:; if (!(init__r432 == 0)) { if (!(ep31 == 0)) { init__tmp___20 = 1; label_5809:; goto label_4164; } else { init__tmp___20 = 0; goto label_5809; } } else { init__tmp___20 = 0; goto label_4164; } } } else { goto label_5803; } } } else { if (!(init__r312 == 0)) { if (!(ep14 == 0)) { init__tmp___19 = 1; goto label_4159; } else { label_5818:; if (!(init__r322 == 0)) { if (!(ep24 == 0)) { init__tmp___19 = 1; label_5824:; goto label_4159; } else { init__tmp___19 = 0; goto label_5824; } } else { init__tmp___19 = 0; goto label_4159; } } } else { goto label_5818; } } } else { if (!(init__r312 == 0)) { if (!(ep12 == 0)) { init__tmp___18 = 1; goto label_4154; } else { label_5833:; if (!(init__r342 == 0)) { if (!(ep42 == 0)) { init__tmp___18 = 1; label_5839:; goto label_4154; } else { init__tmp___18 = 0; goto label_5839; } } else { init__tmp___18 = 0; goto label_4154; } } } else { goto label_5833; } } } else { if (!(init__r322 == 0)) { if (!(ep21 == 0)) { init__tmp___17 = 1; goto label_4149; } else { label_5848:; if (!(init__r342 == 0)) { if (!(ep41 == 0)) { init__tmp___17 = 1; label_5854:; goto label_4149; } else { init__tmp___17 = 0; goto label_5854; } } else { init__tmp___17 = 0; goto label_4149; } } } else { goto label_5848; } } } else { if (!(init__r212 == 0)) { if (!(ep14 == 0)) { init__tmp___16 = 1; goto label_4144; } else { label_5863:; if (!(init__r232 == 0)) { if (!(ep34 == 0)) { init__tmp___16 = 1; label_5869:; goto label_4144; } else { init__tmp___16 = 0; goto label_5869; } } else { init__tmp___16 = 0; goto label_4144; } } } else { goto label_5863; } } } else { if (!(init__r212 == 0)) { if (!(ep13 == 0)) { init__tmp___15 = 1; goto label_4139; } else { label_5878:; if (!(init__r242 == 0)) { if (!(ep43 == 0)) { init__tmp___15 = 1; label_5884:; goto label_4139; } else { init__tmp___15 = 0; goto label_5884; } } else { init__tmp___15 = 0; goto label_4139; } } } else { goto label_5878; } } } else { if (!(init__r232 == 0)) { if (!(ep31 == 0)) { init__tmp___14 = 1; goto label_4134; } else { label_5893:; if (!(init__r242 == 0)) { if (!(ep41 == 0)) { init__tmp___14 = 1; label_5899:; goto label_4134; } else { init__tmp___14 = 0; goto label_5899; } } else { init__tmp___14 = 0; goto label_4134; } } } else { goto label_5893; } } } else { if (!(init__r122 == 0)) { if (!(ep24 == 0)) { init__tmp___13 = 1; goto label_4129; } else { label_5908:; if (!(init__r132 == 0)) { if (!(ep34 == 0)) { init__tmp___13 = 1; label_5914:; goto label_4129; } else { init__tmp___13 = 0; goto label_5914; } } else { init__tmp___13 = 0; goto label_4129; } } } else { goto label_5908; } } } else { if (!(init__r122 == 0)) { if (!(ep23 == 0)) { init__tmp___12 = 1; goto label_4124; } else { label_5923:; if (!(init__r142 == 0)) { if (!(ep43 == 0)) { init__tmp___12 = 1; label_5929:; goto label_4124; } else { init__tmp___12 = 0; goto label_5929; } } else { init__tmp___12 = 0; goto label_4124; } } } else { goto label_5923; } } } else { if (!(init__r132 == 0)) { if (!(ep32 == 0)) { init__tmp___11 = 1; goto label_4119; } else { label_5938:; if (!(init__r142 == 0)) { if (!(ep42 == 0)) { init__tmp___11 = 1; label_5944:; goto label_4119; } else { init__tmp___11 = 0; goto label_5944; } } else { init__tmp___11 = 0; goto label_4119; } } } else { goto label_5938; } } } else { if (!(init__r411 == 0)) { if (!(ep13 == 0)) { init__tmp___10 = 1; goto label_4114; } else { label_5953:; if (!(init__r421 == 0)) { if (!(ep23 == 0)) { init__tmp___10 = 1; label_5959:; goto label_4114; } else { init__tmp___10 = 0; goto label_5959; } } else { init__tmp___10 = 0; goto label_4114; } } } else { goto label_5953; } } } else { if (!(init__r411 == 0)) { if (!(ep12 == 0)) { init__tmp___9 = 1; goto label_4109; } else { label_5968:; if (!(init__r431 == 0)) { if (!(ep32 == 0)) { init__tmp___9 = 1; label_5974:; goto label_4109; } else { init__tmp___9 = 0; goto label_5974; } } else { init__tmp___9 = 0; goto label_4109; } } } else { goto label_5968; } } } else { if (!(init__r421 == 0)) { if (!(ep21 == 0)) { init__tmp___8 = 1; goto label_4104; } else { label_5983:; if (!(init__r431 == 0)) { if (!(ep31 == 0)) { init__tmp___8 = 1; label_5989:; goto label_4104; } else { init__tmp___8 = 0; goto label_5989; } } else { init__tmp___8 = 0; goto label_4104; } } } else { goto label_5983; } } } else { if (!(init__r311 == 0)) { if (!(ep14 == 0)) { init__tmp___7 = 1; goto label_4099; } else { label_5998:; if (!(init__r321 == 0)) { if (!(ep24 == 0)) { init__tmp___7 = 1; label_6004:; goto label_4099; } else { init__tmp___7 = 0; goto label_6004; } } else { init__tmp___7 = 0; goto label_4099; } } } else { goto label_5998; } } } else { if (!(init__r311 == 0)) { if (!(ep12 == 0)) { init__tmp___6 = 1; goto label_4094; } else { label_6013:; if (!(init__r341 == 0)) { if (!(ep42 == 0)) { init__tmp___6 = 1; label_6019:; goto label_4094; } else { init__tmp___6 = 0; goto label_6019; } } else { init__tmp___6 = 0; goto label_4094; } } } else { goto label_6013; } } } else { if (!(init__r321 == 0)) { if (!(ep21 == 0)) { init__tmp___5 = 1; goto label_4089; } else { label_6028:; if (!(init__r341 == 0)) { if (!(ep41 == 0)) { init__tmp___5 = 1; label_6034:; goto label_4089; } else { init__tmp___5 = 0; goto label_6034; } } else { init__tmp___5 = 0; goto label_4089; } } } else { goto label_6028; } } } else { if (!(init__r211 == 0)) { if (!(ep14 == 0)) { init__tmp___4 = 1; goto label_4084; } else { label_6043:; if (!(init__r231 == 0)) { if (!(ep34 == 0)) { init__tmp___4 = 1; label_6049:; goto label_4084; } else { init__tmp___4 = 0; goto label_6049; } } else { init__tmp___4 = 0; goto label_4084; } } } else { goto label_6043; } } } else { if (!(init__r211 == 0)) { if (!(ep13 == 0)) { init__tmp___3 = 1; goto label_4079; } else { label_6058:; if (!(init__r241 == 0)) { if (!(ep43 == 0)) { init__tmp___3 = 1; label_6064:; goto label_4079; } else { init__tmp___3 = 0; goto label_6064; } } else { init__tmp___3 = 0; goto label_4079; } } } else { goto label_6058; } } } else { if (!(init__r231 == 0)) { if (!(ep31 == 0)) { init__tmp___2 = 1; goto label_4074; } else { label_6073:; if (!(init__r241 == 0)) { if (!(ep41 == 0)) { init__tmp___2 = 1; label_6079:; goto label_4074; } else { init__tmp___2 = 0; goto label_6079; } } else { init__tmp___2 = 0; goto label_4074; } } } else { goto label_6073; } } } else { if (!(init__r121 == 0)) { if (!(ep24 == 0)) { init__tmp___1 = 1; goto label_4069; } else { label_6088:; if (!(init__r131 == 0)) { if (!(ep34 == 0)) { init__tmp___1 = 1; label_6094:; goto label_4069; } else { init__tmp___1 = 0; goto label_6094; } } else { init__tmp___1 = 0; goto label_4069; } } } else { goto label_6088; } } } else { if (!(init__r121 == 0)) { if (!(ep23 == 0)) { init__tmp___0 = 1; goto label_4064; } else { label_6103:; if (!(init__r141 == 0)) { if (!(ep43 == 0)) { init__tmp___0 = 1; label_6109:; goto label_4064; } else { init__tmp___0 = 0; goto label_6109; } } else { init__tmp___0 = 0; goto label_4064; } } } else { goto label_6103; } } } else { if (!(init__r131 == 0)) { if (!(ep32 == 0)) { init__tmp = 1; goto label_4059; } else { label_6118:; if (!(init__r141 == 0)) { if (!(ep42 == 0)) { init__tmp = 1; label_6124:; goto label_4059; } else { init__tmp = 0; goto label_6124; } } else { init__tmp = 0; goto label_4059; } } } else { goto label_6118; } } } }