// 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.UNBOUNDED.pals.c.v+lhb-reducer.c", 4, "reach_error"); } char __VERIFIER_nondet_char(); unsigned char __VERIFIER_nondet_uchar(); _Bool __VERIFIER_nondet_bool(); void assert(_Bool arg); void abort(void); void assume_abort_if_not(int cond) { if(!cond) {abort();} } typedef char msg_t; typedef int port_t; void read(port_t p, msg_t m); void write(port_t p, msg_t m); msg_t nomsg = (msg_t )-1; port_t p12 = 0; char p12_old = '\x0'; char p12_new = '\x0'; _Bool ep12 = 0; port_t p13 = 0; char p13_old = '\x0'; char p13_new = '\x0'; _Bool ep13 = 0; port_t p14 = 0; char p14_old = '\x0'; char p14_new = '\x0'; _Bool ep14 = 0; port_t p21 = 0; char p21_old = '\x0'; char p21_new = '\x0'; _Bool ep21 = 0; port_t p23 = 0; char p23_old = '\x0'; char p23_new = '\x0'; _Bool ep23 = 0; port_t p24 = 0; char p24_old = '\x0'; char p24_new = '\x0'; _Bool ep24 = 0; port_t p31 = 0; char p31_old = '\x0'; char p31_new = '\x0'; _Bool ep31 = 0; port_t p32 = 0; char p32_old = '\x0'; char p32_new = '\x0'; _Bool ep32 = 0; port_t p34 = 0; char p34_old = '\x0'; char p34_new = '\x0'; _Bool ep34 = 0; port_t p41 = 0; char p41_old = '\x0'; char p41_new = '\x0'; _Bool ep41 = 0; port_t p42 = 0; char p42_old = '\x0'; char p42_new = '\x0'; _Bool ep42 = 0; port_t p43 = 0; char p43_old = '\x0'; char p43_new = '\x0'; _Bool ep43 = 0; char id1 = '\x0'; unsigned char r1 = '\x0'; char st1 = '\x0'; char nl1 = '\x0'; char m1 = '\x0'; char max1 = '\x0'; _Bool mode1 = 0; char id2 = '\x0'; unsigned char r2 = '\x0'; char st2 = '\x0'; char nl2 = '\x0'; char m2 = '\x0'; char max2 = '\x0'; _Bool mode2 = 0; char id3 = '\x0'; unsigned char r3 = '\x0'; char st3 = '\x0'; char nl3 = '\x0'; char m3 = '\x0'; char max3 = '\x0'; _Bool mode3 = 0; char id4 = '\x0'; unsigned 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_4282; int __return_4492; int __return_4676; int __return_4864; int __return_5048; int __return_5212; int __return_6873; int __return_6830; int __return_6752; int __return_6709; int __return_6596; int __return_6553; int __return_6475; int __return_6429; int __return_5582; int __return_6261; int __return_6218; int __return_6140; int __return_6094; int __return_5961; int __return_5915; int __return_5814; int __return_5405; int main() { int main__c1; int main__i2; main__c1 = 0; ep12 = __VERIFIER_nondet_bool(); ep13 = __VERIFIER_nondet_bool(); ep14 = __VERIFIER_nondet_bool(); ep21 = __VERIFIER_nondet_bool(); ep23 = __VERIFIER_nondet_bool(); ep24 = __VERIFIER_nondet_bool(); ep31 = __VERIFIER_nondet_bool(); ep32 = __VERIFIER_nondet_bool(); ep34 = __VERIFIER_nondet_bool(); ep41 = __VERIFIER_nondet_bool(); ep42 = __VERIFIER_nondet_bool(); ep43 = __VERIFIER_nondet_bool(); id1 = __VERIFIER_nondet_char(); r1 = __VERIFIER_nondet_uchar(); st1 = __VERIFIER_nondet_char(); nl1 = __VERIFIER_nondet_char(); m1 = __VERIFIER_nondet_char(); max1 = __VERIFIER_nondet_char(); mode1 = __VERIFIER_nondet_bool(); id2 = __VERIFIER_nondet_char(); r2 = __VERIFIER_nondet_uchar(); st2 = __VERIFIER_nondet_char(); nl2 = __VERIFIER_nondet_char(); m2 = __VERIFIER_nondet_char(); max2 = __VERIFIER_nondet_char(); mode2 = __VERIFIER_nondet_bool(); id3 = __VERIFIER_nondet_char(); r3 = __VERIFIER_nondet_uchar(); st3 = __VERIFIER_nondet_char(); nl3 = __VERIFIER_nondet_char(); m3 = __VERIFIER_nondet_char(); max3 = __VERIFIER_nondet_char(); mode3 = __VERIFIER_nondet_bool(); id4 = __VERIFIER_nondet_char(); r4 = __VERIFIER_nondet_uchar(); st4 = __VERIFIER_nondet_char(); nl4 = __VERIFIER_nondet_char(); m4 = __VERIFIER_nondet_char(); max4 = __VERIFIER_nondet_char(); mode4 = __VERIFIER_nondet_bool(); { _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_4080:; init__r122 = (_Bool)init__tmp; if (!(init__r131 == 0)) { init__tmp___0 = 1; label_4085:; init__r132 = (_Bool)init__tmp___0; if (!(init__r141 == 0)) { init__tmp___1 = 1; label_4090:; init__r142 = (_Bool)init__tmp___1; if (!(init__r211 == 0)) { init__tmp___2 = 1; label_4095:; init__r212 = (_Bool)init__tmp___2; if (!(init__r231 == 0)) { init__tmp___3 = 1; label_4100:; init__r232 = (_Bool)init__tmp___3; if (!(init__r241 == 0)) { init__tmp___4 = 1; label_4105:; init__r242 = (_Bool)init__tmp___4; if (!(init__r311 == 0)) { init__tmp___5 = 1; label_4110:; init__r312 = (_Bool)init__tmp___5; if (!(init__r321 == 0)) { init__tmp___6 = 1; label_4115:; init__r322 = (_Bool)init__tmp___6; if (!(init__r341 == 0)) { init__tmp___7 = 1; label_4120:; init__r342 = (_Bool)init__tmp___7; if (!(init__r411 == 0)) { init__tmp___8 = 1; label_4125:; init__r412 = (_Bool)init__tmp___8; if (!(init__r421 == 0)) { init__tmp___9 = 1; label_4130:; init__r422 = (_Bool)init__tmp___9; if (!(init__r431 == 0)) { init__tmp___10 = 1; label_4135:; init__r432 = (_Bool)init__tmp___10; if (!(init__r122 == 0)) { init__tmp___11 = 1; label_4140:; init__r123 = (_Bool)init__tmp___11; if (!(init__r132 == 0)) { init__tmp___12 = 1; label_4145:; init__r133 = (_Bool)init__tmp___12; if (!(init__r142 == 0)) { init__tmp___13 = 1; label_4150:; init__r143 = (_Bool)init__tmp___13; if (!(init__r212 == 0)) { init__tmp___14 = 1; label_4155:; init__r213 = (_Bool)init__tmp___14; if (!(init__r232 == 0)) { init__tmp___15 = 1; label_4160:; init__r233 = (_Bool)init__tmp___15; if (!(init__r242 == 0)) { init__tmp___16 = 1; label_4165:; init__r243 = (_Bool)init__tmp___16; if (!(init__r312 == 0)) { init__tmp___17 = 1; label_4170:; init__r313 = (_Bool)init__tmp___17; if (!(init__r322 == 0)) { init__tmp___18 = 1; label_4175:; init__r323 = (_Bool)init__tmp___18; if (!(init__r342 == 0)) { init__tmp___19 = 1; label_4180:; init__r343 = (_Bool)init__tmp___19; if (!(init__r412 == 0)) { init__tmp___20 = 1; label_4185:; init__r413 = (_Bool)init__tmp___20; if (!(init__r422 == 0)) { init__tmp___21 = 1; label_4190:; init__r423 = (_Bool)init__tmp___21; if (!(init__r432 == 0)) { init__tmp___22 = 1; label_4195:; 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_4282 = init__tmp___23; main__i2 = __return_4282; 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 (!(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_4322:; p12_new = node1____CPAchecker_TMP_0; label_4317:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4330:; p13_new = node1____CPAchecker_TMP_1; label_4325:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4338:; p14_new = node1____CPAchecker_TMP_2; label_4340:; 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_4354:; p21_new = node2____CPAchecker_TMP_0; label_4349:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4362:; p23_new = node2____CPAchecker_TMP_1; label_4357:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4370:; p24_new = node2____CPAchecker_TMP_2; label_4372:; 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_4386:; p31_new = node3____CPAchecker_TMP_0; label_4381:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4394:; p32_new = node3____CPAchecker_TMP_1; label_4389:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4402:; p34_new = node3____CPAchecker_TMP_2; label_4404:; 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_4418:; p41_new = node4____CPAchecker_TMP_0; label_4413:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4426:; p42_new = node4____CPAchecker_TMP_1; label_4421:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4434:; p43_new = node4____CPAchecker_TMP_2; label_4436:; 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_4492 = check__tmp; main__c1 = __return_4492; { _Bool __tmp_1; __tmp_1 = main__c1; _Bool assert__arg; assert__arg = __tmp_1; if (assert__arg == 0) { return __return_main; } else { { if (!(mode1 == 0)) { if (r1 == 255) { return __return_main; } else { r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4506:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4513:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4520:; if (((int)r1) == 3) { return __return_main; } else { mode1 = 0; { if (!(mode2 == 0)) { if (r2 == 255) { return __return_main; } else { r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4537:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4544:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4551:; if (((int)r2) == 3) { return __return_main; } else { mode2 = 0; { if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4568:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4575:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4582:; if (((int)r3) == 3) { return __return_main; } else { mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4599:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4606:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4613:; 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_4676 = check__tmp; main__c1 = __return_4676; { _Bool __tmp_2; __tmp_2 = main__c1; _Bool assert__arg; assert__arg = __tmp_2; if (assert__arg == 0) { return __return_main; } else { { 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_4694:; p12_new = node1____CPAchecker_TMP_0; label_4689:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4702:; p13_new = node1____CPAchecker_TMP_1; label_4697:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4710:; p14_new = node1____CPAchecker_TMP_2; label_4712:; 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_4726:; p21_new = node2____CPAchecker_TMP_0; label_4721:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4734:; p23_new = node2____CPAchecker_TMP_1; label_4729:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4742:; p24_new = node2____CPAchecker_TMP_2; label_4744:; 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_4758:; p31_new = node3____CPAchecker_TMP_0; label_4753:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4766:; p32_new = node3____CPAchecker_TMP_1; label_4761:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4774:; p34_new = node3____CPAchecker_TMP_2; label_4776:; mode3 = 1; { 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_4790:; p41_new = node4____CPAchecker_TMP_0; label_4785:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4798:; p42_new = node4____CPAchecker_TMP_1; label_4793:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4806:; p43_new = node4____CPAchecker_TMP_2; label_4808:; 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_4864 = check__tmp; main__c1 = __return_4864; { _Bool __tmp_3; __tmp_3 = main__c1; _Bool assert__arg; assert__arg = __tmp_3; if (assert__arg == 0) { return __return_main; } else { { if (!(mode1 == 0)) { if (r1 == 255) { return __return_main; } else { r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4878:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4885:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4892:; if (((int)r1) == 3) { return __return_main; } else { mode1 = 0; { if (!(mode2 == 0)) { if (r2 == 255) { return __return_main; } else { r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4909:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4916:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4923:; if (((int)r2) == 3) { return __return_main; } else { mode2 = 0; { if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4940:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4947:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4954:; if (((int)r3) == 3) { return __return_main; } else { mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4971:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4978:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4985:; 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_5048 = check__tmp; main__c1 = __return_5048; { _Bool __tmp_4; __tmp_4 = main__c1; _Bool assert__arg; assert__arg = __tmp_4; if (assert__arg == 0) { return __return_main; } else { { 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_5074:; p21_new = node2____CPAchecker_TMP_0; label_5069:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5082:; p23_new = node2____CPAchecker_TMP_1; label_5077:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5090:; p24_new = node2____CPAchecker_TMP_2; label_5092:; 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_5106:; p31_new = node3____CPAchecker_TMP_0; label_5101:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5114:; p32_new = node3____CPAchecker_TMP_1; label_5109:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5122:; p34_new = node3____CPAchecker_TMP_2; label_5124:; 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_5138:; p41_new = node4____CPAchecker_TMP_0; label_5133:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5146:; p42_new = node4____CPAchecker_TMP_1; label_5141:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5154:; p43_new = node4____CPAchecker_TMP_2; label_5156:; 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_5212 = check__tmp; main__c1 = __return_5212; { _Bool __tmp_5; __tmp_5 = main__c1; _Bool assert__arg; assert__arg = __tmp_5; if (assert__arg == 0) { return __return_main; } else { { if (!(mode1 == 0)) { if (r1 == 255) { return __return_main; } else { r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5226:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5233:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5240:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; mode1 = 0; { if (!(mode2 == 0)) { if (r2 == 255) { return __return_main; } else { r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_6279:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_6286:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_6293:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; mode2 = 0; { if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6614:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6621:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6628:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6770:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6777:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6784:; 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_6873 = check__tmp; main__c1 = __return_6873; { _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_6830 = check__tmp; main__c1 = __return_6830; { _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_6784; } } else { goto label_6784; } } else { goto label_6777; } } else { goto label_6777; } } else { goto label_6770; } } else { goto label_6770; } } } else { return __return_main; } } } else { nl3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6649:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6656:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6663:; 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_6752 = check__tmp; main__c1 = __return_6752; { _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_6709 = check__tmp; main__c1 = __return_6709; { _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_6663; } } else { goto label_6663; } } else { goto label_6656; } } else { goto label_6656; } } else { goto label_6649; } } else { goto label_6649; } } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6628; } } else { goto label_6628; } } else { goto label_6621; } } else { goto label_6621; } } else { goto label_6614; } } else { goto label_6614; } } } else { return __return_main; } } } else { nl2 = 1; mode2 = 0; { if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6314:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6321:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6328:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6493:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6500:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6507:; 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_6596 = check__tmp; main__c1 = __return_6596; { _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_6553 = check__tmp; main__c1 = __return_6553; { _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_6507; } } else { goto label_6507; } } else { goto label_6500; } } else { goto label_6500; } } else { goto label_6493; } } else { goto label_6493; } } } else { return __return_main; } } } else { nl3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6349:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6356:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6363:; 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_6475 = check__tmp; main__c1 = __return_6475; { _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_6430:; if (((int)r1) < 3) { check__tmp = 1; label_6436:; label_6421:; __return_6429 = check__tmp; main__c1 = __return_6429; label_5406:; { _Bool __tmp_13; __tmp_13 = main__c1; _Bool assert__arg; assert__arg = __tmp_13; if (assert__arg == 0) { {reach_error();} return __return_main; } else { { if (!(mode1 == 0)) { if (r1 == 255) { r1 = 3; label_5420:; r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5422:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5429:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5436:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5444:; mode1 = 0; label_5446:; { if (!(mode2 == 0)) { if (r2 == 255) { r2 = 3; label_5454:; r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5456:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5463:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5470:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5478:; mode2 = 0; label_5480:; { if (!(mode3 == 0)) { if (r3 == 255) { r3 = 3; label_5488:; r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5490:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5497:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5504:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5512:; mode3 = 0; label_5514:; { if (!(mode4 == 0)) { if (r4 == 255) { r4 = 3; label_5522:; r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5524:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5531:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5538:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5546:; mode4 = 0; label_5548:; 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_5605:; if (((int)r1) < 3) { label_5612:; if (((int)r1) >= 3) { label_5619:; if (((int)r1) < 3) { check__tmp = 1; label_5625:; label_5618:; label_5611:; label_5604:; label_5598:; label_5594:; label_5590:; label_5586:; label_5581:; __return_5582 = check__tmp; main__c1 = __return_5582; goto label_5406; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5625; } else { check__tmp = 0; goto label_5625; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5619; } else { check__tmp = 0; goto label_5618; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_5612; } else { check__tmp = 0; goto label_5611; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_5605; } else { check__tmp = 0; goto label_5604; } } } else { check__tmp = 0; goto label_5598; } } else { check__tmp = 0; goto label_5594; } } else { check__tmp = 0; goto label_5590; } } else { check__tmp = 0; goto label_5586; } } else { check__tmp = 0; goto label_5581; } } } else { nl4 = 1; goto label_5546; } } else { goto label_5546; } } else { goto label_5538; } } else { goto label_5538; } } else { goto label_5531; } } else { goto label_5531; } } else { goto label_5524; } } else { goto label_5524; } } else { goto label_5522; } } 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_5641:; p41_new = node4____CPAchecker_TMP_0; label_5636:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5649:; p42_new = node4____CPAchecker_TMP_1; label_5644:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5657:; p43_new = node4____CPAchecker_TMP_2; label_5634:; mode4 = 1; goto label_5548; } else { label_5656:; node4____CPAchecker_TMP_2 = p43_new; goto label_5657; } } else { goto label_5656; } } else { goto label_5634; } } else { label_5648:; node4____CPAchecker_TMP_1 = p42_new; goto label_5649; } } else { goto label_5648; } } else { goto label_5644; } } else { label_5640:; node4____CPAchecker_TMP_0 = p41_new; goto label_5641; } } else { goto label_5640; } } else { goto label_5636; } } else { goto label_5634; } } } } else { nl3 = 1; goto label_5512; } } else { goto label_5512; } } else { goto label_5504; } } else { goto label_5504; } } else { goto label_5497; } } else { goto label_5497; } } else { goto label_5490; } } else { goto label_5490; } } else { goto label_5488; } } 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_5673:; p31_new = node3____CPAchecker_TMP_0; label_5668:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5681:; p32_new = node3____CPAchecker_TMP_1; label_5676:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5689:; p34_new = node3____CPAchecker_TMP_2; label_5666:; mode3 = 1; goto label_5514; } else { label_5688:; node3____CPAchecker_TMP_2 = p34_new; goto label_5689; } } else { goto label_5688; } } else { goto label_5666; } } else { label_5680:; node3____CPAchecker_TMP_1 = p32_new; goto label_5681; } } else { goto label_5680; } } else { goto label_5676; } } else { label_5672:; node3____CPAchecker_TMP_0 = p31_new; goto label_5673; } } else { goto label_5672; } } else { goto label_5668; } } else { goto label_5666; } } } } else { nl2 = 1; goto label_5478; } } else { goto label_5478; } } else { goto label_5470; } } else { goto label_5470; } } else { goto label_5463; } } else { goto label_5463; } } else { goto label_5456; } } else { goto label_5456; } } else { goto label_5454; } } 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_5705:; p21_new = node2____CPAchecker_TMP_0; label_5700:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5713:; p23_new = node2____CPAchecker_TMP_1; label_5708:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5721:; p24_new = node2____CPAchecker_TMP_2; label_5698:; mode2 = 1; goto label_5480; } else { label_5720:; node2____CPAchecker_TMP_2 = p24_new; goto label_5721; } } else { goto label_5720; } } else { goto label_5698; } } else { label_5712:; node2____CPAchecker_TMP_1 = p23_new; goto label_5713; } } else { goto label_5712; } } else { goto label_5708; } } else { label_5704:; node2____CPAchecker_TMP_0 = p21_new; goto label_5705; } } else { goto label_5704; } } else { goto label_5700; } } else { goto label_5698; } } } } else { nl1 = 1; goto label_5444; } } else { goto label_5444; } } else { goto label_5436; } } else { goto label_5436; } } else { goto label_5429; } } else { goto label_5429; } } else { goto label_5422; } } else { goto label_5422; } } else { goto label_5420; } } 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_5737:; p12_new = node1____CPAchecker_TMP_0; label_5732:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5745:; p13_new = node1____CPAchecker_TMP_1; label_5740:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5753:; p14_new = node1____CPAchecker_TMP_2; label_5730:; mode1 = 1; goto label_5446; } else { label_5752:; node1____CPAchecker_TMP_2 = p14_new; goto label_5753; } } else { goto label_5752; } } else { goto label_5730; } } else { label_5744:; node1____CPAchecker_TMP_1 = p13_new; goto label_5745; } } else { goto label_5744; } } else { goto label_5740; } } else { label_5736:; node1____CPAchecker_TMP_0 = p12_new; goto label_5737; } } else { goto label_5736; } } else { goto label_5732; } } else { goto label_5730; } } } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6436; } else { check__tmp = 0; goto label_6436; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6430; } else { check__tmp = 0; goto label_6421; } } } else { 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_6363; } } else { goto label_6363; } } else { goto label_6356; } } else { goto label_6356; } } else { goto label_6349; } } else { goto label_6349; } } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6328; } } else { goto label_6328; } } else { goto label_6321; } } else { goto label_6321; } } else { goto label_6314; } } else { goto label_6314; } } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6293; } } else { goto label_6293; } } else { goto label_6286; } } else { goto label_6286; } } else { goto label_6279; } } else { goto label_6279; } } } else { return __return_main; } } } else { nl1 = 1; mode1 = 0; { if (!(mode2 == 0)) { if (r2 == 255) { return __return_main; } else { r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5261:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5268:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5275:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; mode2 = 0; { if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5979:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5986:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5993:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6158:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6165:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6172:; 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_6261 = check__tmp; main__c1 = __return_6261; { _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_6218 = check__tmp; main__c1 = __return_6218; { _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_6172; } } else { goto label_6172; } } else { goto label_6165; } } else { goto label_6165; } } else { goto label_6158; } } else { goto label_6158; } } } else { return __return_main; } } } else { nl3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6014:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6021:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6028:; 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_6140 = check__tmp; main__c1 = __return_6140; { _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_6095:; if (((int)r1) < 3) { check__tmp = 1; label_6101:; label_6086:; __return_6094 = check__tmp; main__c1 = __return_6094; goto label_5406; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6101; } else { check__tmp = 0; goto label_6101; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6095; } else { check__tmp = 0; goto label_6086; } } } else { 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_6028; } } else { goto label_6028; } } else { goto label_6021; } } else { goto label_6021; } } else { goto label_6014; } } else { goto label_6014; } } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5993; } } else { goto label_5993; } } else { goto label_5986; } } else { goto label_5986; } } else { goto label_5979; } } else { goto label_5979; } } } else { return __return_main; } } } else { nl2 = 1; mode2 = 0; { if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5296:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5303:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5310:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5835:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5842:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5849:; 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_5961 = check__tmp; main__c1 = __return_5961; { _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_5916:; if (((int)r1) < 3) { check__tmp = 1; label_5922:; label_5907:; __return_5915 = check__tmp; main__c1 = __return_5915; goto label_5406; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5922; } else { check__tmp = 0; goto label_5922; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5916; } else { check__tmp = 0; goto label_5907; } } } else { 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_5849; } } else { goto label_5849; } } else { goto label_5842; } } else { goto label_5842; } } else { goto label_5835; } } else { goto label_5835; } } } else { return __return_main; } } } else { nl3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5331:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5338:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5345:; 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_5815:; if (((int)r1) < 3) { check__tmp = 1; label_5821:; label_5806:; __return_5814 = check__tmp; main__c1 = __return_5814; goto label_5406; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5821; } else { check__tmp = 0; goto label_5821; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5815; } else { check__tmp = 0; goto label_5806; } } } else { 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_5405 = check__tmp; main__c1 = __return_5405; goto label_5406; } } } else { 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_5345; } } else { goto label_5345; } } else { goto label_5338; } } else { goto label_5338; } } else { goto label_5331; } } else { goto label_5331; } } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5310; } } else { goto label_5310; } } else { goto label_5303; } } else { goto label_5303; } } else { goto label_5296; } } else { goto label_5296; } } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5275; } } else { goto label_5275; } } else { goto label_5268; } } else { goto label_5268; } } else { goto label_5261; } } else { goto label_5261; } } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5240; } } else { goto label_5240; } } else { goto label_5233; } } else { goto label_5233; } } else { goto label_5226; } } else { goto label_5226; } } } else { 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_5153:; node4____CPAchecker_TMP_2 = p43_new; goto label_5154; } } else { goto label_5153; } } else { goto label_5156; } } else { label_5145:; node4____CPAchecker_TMP_1 = p42_new; goto label_5146; } } else { goto label_5145; } } else { goto label_5141; } } else { label_5137:; node4____CPAchecker_TMP_0 = p41_new; goto label_5138; } } else { goto label_5137; } } else { goto label_5133; } } else { return __return_main; } } } } else { label_5121:; node3____CPAchecker_TMP_2 = p34_new; goto label_5122; } } else { goto label_5121; } } else { goto label_5124; } } else { label_5113:; node3____CPAchecker_TMP_1 = p32_new; goto label_5114; } } else { goto label_5113; } } else { goto label_5109; } } else { label_5105:; node3____CPAchecker_TMP_0 = p31_new; goto label_5106; } } else { goto label_5105; } } else { goto label_5101; } } else { return __return_main; } } } } else { label_5089:; node2____CPAchecker_TMP_2 = p24_new; goto label_5090; } } else { goto label_5089; } } else { goto label_5092; } } else { label_5081:; node2____CPAchecker_TMP_1 = p23_new; goto label_5082; } } else { goto label_5081; } } else { goto label_5077; } } else { label_5073:; node2____CPAchecker_TMP_0 = p21_new; goto label_5074; } } else { goto label_5073; } } else { goto label_5069; } } else { 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_4985; } } else { goto label_4985; } } else { goto label_4978; } } else { goto label_4978; } } else { goto label_4971; } } else { goto label_4971; } } } else { return __return_main; } } } } else { goto label_4954; } } else { goto label_4954; } } else { goto label_4947; } } else { goto label_4947; } } else { goto label_4940; } } else { goto label_4940; } } } else { return __return_main; } } } } else { goto label_4923; } } else { goto label_4923; } } else { goto label_4916; } } else { goto label_4916; } } else { goto label_4909; } } else { goto label_4909; } } } else { return __return_main; } } } } else { goto label_4892; } } else { goto label_4892; } } else { goto label_4885; } } else { goto label_4885; } } else { goto label_4878; } } else { goto label_4878; } } } else { 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_4805:; node4____CPAchecker_TMP_2 = p43_new; goto label_4806; } } else { goto label_4805; } } else { goto label_4808; } } else { label_4797:; node4____CPAchecker_TMP_1 = p42_new; goto label_4798; } } else { goto label_4797; } } else { goto label_4793; } } else { label_4789:; node4____CPAchecker_TMP_0 = p41_new; goto label_4790; } } else { goto label_4789; } } else { goto label_4785; } } else { return __return_main; } } } } else { label_4773:; node3____CPAchecker_TMP_2 = p34_new; goto label_4774; } } else { goto label_4773; } } else { goto label_4776; } } else { label_4765:; node3____CPAchecker_TMP_1 = p32_new; goto label_4766; } } else { goto label_4765; } } else { goto label_4761; } } else { label_4757:; node3____CPAchecker_TMP_0 = p31_new; goto label_4758; } } else { goto label_4757; } } else { goto label_4753; } } else { return __return_main; } } } } else { label_4741:; node2____CPAchecker_TMP_2 = p24_new; goto label_4742; } } else { goto label_4741; } } else { goto label_4744; } } else { label_4733:; node2____CPAchecker_TMP_1 = p23_new; goto label_4734; } } else { goto label_4733; } } else { goto label_4729; } } else { label_4725:; node2____CPAchecker_TMP_0 = p21_new; goto label_4726; } } else { goto label_4725; } } else { goto label_4721; } } else { return __return_main; } } } } else { label_4709:; node1____CPAchecker_TMP_2 = p14_new; goto label_4710; } } else { goto label_4709; } } else { goto label_4712; } } else { label_4701:; node1____CPAchecker_TMP_1 = p13_new; goto label_4702; } } else { goto label_4701; } } else { goto label_4697; } } else { label_4693:; node1____CPAchecker_TMP_0 = p12_new; goto label_4694; } } else { goto label_4693; } } else { goto label_4689; } } else { 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_4613; } } else { goto label_4613; } } else { goto label_4606; } } else { goto label_4606; } } else { goto label_4599; } } else { goto label_4599; } } } else { return __return_main; } } } } else { goto label_4582; } } else { goto label_4582; } } else { goto label_4575; } } else { goto label_4575; } } else { goto label_4568; } } else { goto label_4568; } } } else { return __return_main; } } } } else { goto label_4551; } } else { goto label_4551; } } else { goto label_4544; } } else { goto label_4544; } } else { goto label_4537; } } else { goto label_4537; } } } else { return __return_main; } } } } else { goto label_4520; } } else { goto label_4520; } } else { goto label_4513; } } else { goto label_4513; } } else { goto label_4506; } } else { goto label_4506; } } } else { 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_4433:; node4____CPAchecker_TMP_2 = p43_new; goto label_4434; } } else { goto label_4433; } } else { goto label_4436; } } else { label_4425:; node4____CPAchecker_TMP_1 = p42_new; goto label_4426; } } else { goto label_4425; } } else { goto label_4421; } } else { label_4417:; node4____CPAchecker_TMP_0 = p41_new; goto label_4418; } } else { goto label_4417; } } else { goto label_4413; } } else { return __return_main; } } } } else { label_4401:; node3____CPAchecker_TMP_2 = p34_new; goto label_4402; } } else { goto label_4401; } } else { goto label_4404; } } else { label_4393:; node3____CPAchecker_TMP_1 = p32_new; goto label_4394; } } else { goto label_4393; } } else { goto label_4389; } } else { label_4385:; node3____CPAchecker_TMP_0 = p31_new; goto label_4386; } } else { goto label_4385; } } else { goto label_4381; } } else { return __return_main; } } } } else { label_4369:; node2____CPAchecker_TMP_2 = p24_new; goto label_4370; } } else { goto label_4369; } } else { goto label_4372; } } else { label_4361:; node2____CPAchecker_TMP_1 = p23_new; goto label_4362; } } else { goto label_4361; } } else { goto label_4357; } } else { label_4353:; node2____CPAchecker_TMP_0 = p21_new; goto label_4354; } } else { goto label_4353; } } else { goto label_4349; } } else { return __return_main; } } } } else { label_4337:; node1____CPAchecker_TMP_2 = p14_new; goto label_4338; } } else { goto label_4337; } } else { goto label_4340; } } else { label_4329:; node1____CPAchecker_TMP_1 = p13_new; goto label_4330; } } else { goto label_4329; } } else { goto label_4325; } } else { label_4321:; node1____CPAchecker_TMP_0 = p12_new; goto label_4322; } } else { goto label_4321; } } else { goto label_4317; } } else { 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_4195; } else { label_6897:; if (!(init__r422 == 0)) { if (!(ep23 == 0)) { init__tmp___22 = 1; label_6903:; goto label_4195; } else { init__tmp___22 = 0; goto label_6903; } } else { init__tmp___22 = 0; goto label_4195; } } } else { goto label_6897; } } } else { if (!(init__r412 == 0)) { if (!(ep12 == 0)) { init__tmp___21 = 1; goto label_4190; } else { label_6912:; if (!(init__r432 == 0)) { if (!(ep32 == 0)) { init__tmp___21 = 1; label_6918:; goto label_4190; } else { init__tmp___21 = 0; goto label_6918; } } else { init__tmp___21 = 0; goto label_4190; } } } else { goto label_6912; } } } else { if (!(init__r422 == 0)) { if (!(ep21 == 0)) { init__tmp___20 = 1; goto label_4185; } else { label_6927:; if (!(init__r432 == 0)) { if (!(ep31 == 0)) { init__tmp___20 = 1; label_6933:; goto label_4185; } else { init__tmp___20 = 0; goto label_6933; } } else { init__tmp___20 = 0; goto label_4185; } } } else { goto label_6927; } } } else { if (!(init__r312 == 0)) { if (!(ep14 == 0)) { init__tmp___19 = 1; goto label_4180; } else { label_6942:; if (!(init__r322 == 0)) { if (!(ep24 == 0)) { init__tmp___19 = 1; label_6948:; goto label_4180; } else { init__tmp___19 = 0; goto label_6948; } } else { init__tmp___19 = 0; goto label_4180; } } } else { goto label_6942; } } } else { if (!(init__r312 == 0)) { if (!(ep12 == 0)) { init__tmp___18 = 1; goto label_4175; } else { label_6957:; if (!(init__r342 == 0)) { if (!(ep42 == 0)) { init__tmp___18 = 1; label_6963:; goto label_4175; } else { init__tmp___18 = 0; goto label_6963; } } else { init__tmp___18 = 0; goto label_4175; } } } else { goto label_6957; } } } else { if (!(init__r322 == 0)) { if (!(ep21 == 0)) { init__tmp___17 = 1; goto label_4170; } else { label_6972:; if (!(init__r342 == 0)) { if (!(ep41 == 0)) { init__tmp___17 = 1; label_6978:; goto label_4170; } else { init__tmp___17 = 0; goto label_6978; } } else { init__tmp___17 = 0; goto label_4170; } } } else { goto label_6972; } } } else { if (!(init__r212 == 0)) { if (!(ep14 == 0)) { init__tmp___16 = 1; goto label_4165; } else { label_6987:; if (!(init__r232 == 0)) { if (!(ep34 == 0)) { init__tmp___16 = 1; label_6993:; goto label_4165; } else { init__tmp___16 = 0; goto label_6993; } } else { init__tmp___16 = 0; goto label_4165; } } } else { goto label_6987; } } } else { if (!(init__r212 == 0)) { if (!(ep13 == 0)) { init__tmp___15 = 1; goto label_4160; } else { label_7002:; if (!(init__r242 == 0)) { if (!(ep43 == 0)) { init__tmp___15 = 1; label_7008:; goto label_4160; } else { init__tmp___15 = 0; goto label_7008; } } else { init__tmp___15 = 0; goto label_4160; } } } else { goto label_7002; } } } else { if (!(init__r232 == 0)) { if (!(ep31 == 0)) { init__tmp___14 = 1; goto label_4155; } else { label_7017:; if (!(init__r242 == 0)) { if (!(ep41 == 0)) { init__tmp___14 = 1; label_7023:; goto label_4155; } else { init__tmp___14 = 0; goto label_7023; } } else { init__tmp___14 = 0; goto label_4155; } } } else { goto label_7017; } } } else { if (!(init__r122 == 0)) { if (!(ep24 == 0)) { init__tmp___13 = 1; goto label_4150; } else { label_7032:; if (!(init__r132 == 0)) { if (!(ep34 == 0)) { init__tmp___13 = 1; label_7038:; goto label_4150; } else { init__tmp___13 = 0; goto label_7038; } } else { init__tmp___13 = 0; goto label_4150; } } } else { goto label_7032; } } } else { if (!(init__r122 == 0)) { if (!(ep23 == 0)) { init__tmp___12 = 1; goto label_4145; } else { label_7047:; if (!(init__r142 == 0)) { if (!(ep43 == 0)) { init__tmp___12 = 1; label_7053:; goto label_4145; } else { init__tmp___12 = 0; goto label_7053; } } else { init__tmp___12 = 0; goto label_4145; } } } else { goto label_7047; } } } else { if (!(init__r132 == 0)) { if (!(ep32 == 0)) { init__tmp___11 = 1; goto label_4140; } else { label_7062:; if (!(init__r142 == 0)) { if (!(ep42 == 0)) { init__tmp___11 = 1; label_7068:; goto label_4140; } else { init__tmp___11 = 0; goto label_7068; } } else { init__tmp___11 = 0; goto label_4140; } } } else { goto label_7062; } } } else { if (!(init__r411 == 0)) { if (!(ep13 == 0)) { init__tmp___10 = 1; goto label_4135; } else { label_7077:; if (!(init__r421 == 0)) { if (!(ep23 == 0)) { init__tmp___10 = 1; label_7083:; goto label_4135; } else { init__tmp___10 = 0; goto label_7083; } } else { init__tmp___10 = 0; goto label_4135; } } } else { goto label_7077; } } } else { if (!(init__r411 == 0)) { if (!(ep12 == 0)) { init__tmp___9 = 1; goto label_4130; } else { label_7092:; if (!(init__r431 == 0)) { if (!(ep32 == 0)) { init__tmp___9 = 1; label_7098:; goto label_4130; } else { init__tmp___9 = 0; goto label_7098; } } else { init__tmp___9 = 0; goto label_4130; } } } else { goto label_7092; } } } else { if (!(init__r421 == 0)) { if (!(ep21 == 0)) { init__tmp___8 = 1; goto label_4125; } else { label_7107:; if (!(init__r431 == 0)) { if (!(ep31 == 0)) { init__tmp___8 = 1; label_7113:; goto label_4125; } else { init__tmp___8 = 0; goto label_7113; } } else { init__tmp___8 = 0; goto label_4125; } } } else { goto label_7107; } } } else { if (!(init__r311 == 0)) { if (!(ep14 == 0)) { init__tmp___7 = 1; goto label_4120; } else { label_7122:; if (!(init__r321 == 0)) { if (!(ep24 == 0)) { init__tmp___7 = 1; label_7128:; goto label_4120; } else { init__tmp___7 = 0; goto label_7128; } } else { init__tmp___7 = 0; goto label_4120; } } } else { goto label_7122; } } } else { if (!(init__r311 == 0)) { if (!(ep12 == 0)) { init__tmp___6 = 1; goto label_4115; } else { label_7137:; if (!(init__r341 == 0)) { if (!(ep42 == 0)) { init__tmp___6 = 1; label_7143:; goto label_4115; } else { init__tmp___6 = 0; goto label_7143; } } else { init__tmp___6 = 0; goto label_4115; } } } else { goto label_7137; } } } else { if (!(init__r321 == 0)) { if (!(ep21 == 0)) { init__tmp___5 = 1; goto label_4110; } else { label_7152:; if (!(init__r341 == 0)) { if (!(ep41 == 0)) { init__tmp___5 = 1; label_7158:; goto label_4110; } else { init__tmp___5 = 0; goto label_7158; } } else { init__tmp___5 = 0; goto label_4110; } } } else { goto label_7152; } } } else { if (!(init__r211 == 0)) { if (!(ep14 == 0)) { init__tmp___4 = 1; goto label_4105; } else { label_7167:; if (!(init__r231 == 0)) { if (!(ep34 == 0)) { init__tmp___4 = 1; label_7173:; goto label_4105; } else { init__tmp___4 = 0; goto label_7173; } } else { init__tmp___4 = 0; goto label_4105; } } } else { goto label_7167; } } } else { if (!(init__r211 == 0)) { if (!(ep13 == 0)) { init__tmp___3 = 1; goto label_4100; } else { label_7182:; if (!(init__r241 == 0)) { if (!(ep43 == 0)) { init__tmp___3 = 1; label_7188:; goto label_4100; } else { init__tmp___3 = 0; goto label_7188; } } else { init__tmp___3 = 0; goto label_4100; } } } else { goto label_7182; } } } else { if (!(init__r231 == 0)) { if (!(ep31 == 0)) { init__tmp___2 = 1; goto label_4095; } else { label_7197:; if (!(init__r241 == 0)) { if (!(ep41 == 0)) { init__tmp___2 = 1; label_7203:; goto label_4095; } else { init__tmp___2 = 0; goto label_7203; } } else { init__tmp___2 = 0; goto label_4095; } } } else { goto label_7197; } } } else { if (!(init__r121 == 0)) { if (!(ep24 == 0)) { init__tmp___1 = 1; goto label_4090; } else { label_7212:; if (!(init__r131 == 0)) { if (!(ep34 == 0)) { init__tmp___1 = 1; label_7218:; goto label_4090; } else { init__tmp___1 = 0; goto label_7218; } } else { init__tmp___1 = 0; goto label_4090; } } } else { goto label_7212; } } } else { if (!(init__r121 == 0)) { if (!(ep23 == 0)) { init__tmp___0 = 1; goto label_4085; } else { label_7227:; if (!(init__r141 == 0)) { if (!(ep43 == 0)) { init__tmp___0 = 1; label_7233:; goto label_4085; } else { init__tmp___0 = 0; goto label_7233; } } else { init__tmp___0 = 0; goto label_4085; } } } else { goto label_7227; } } } else { if (!(init__r131 == 0)) { if (!(ep32 == 0)) { init__tmp = 1; goto label_4080; } else { label_7242:; if (!(init__r141 == 0)) { if (!(ep42 == 0)) { init__tmp = 1; label_7248:; goto label_4080; } else { init__tmp = 0; goto label_7248; } } else { init__tmp = 0; goto label_4080; } } } else { goto label_7242; } } } }