// 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.1.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c", 4, "reach_error"); } char __VERIFIER_nondet_char(); _Bool __VERIFIER_nondet_bool(); void assert(_Bool arg); void abort(void); void assume_abort_if_not(int cond) { if(!cond) {abort();} } typedef char msg_t; typedef int port_t; void read(port_t p, msg_t m); void write(port_t p, msg_t m); msg_t nomsg = (msg_t )-1; port_t p12 = 0; char p12_old = '\x0'; char p12_new = '\x0'; _Bool ep12 = 0; port_t p13 = 0; char p13_old = '\x0'; char p13_new = '\x0'; _Bool ep13 = 0; port_t p14 = 0; char p14_old = '\x0'; char p14_new = '\x0'; _Bool ep14 = 0; port_t p21 = 0; char p21_old = '\x0'; char p21_new = '\x0'; _Bool ep21 = 0; port_t p23 = 0; char p23_old = '\x0'; char p23_new = '\x0'; _Bool ep23 = 0; port_t p24 = 0; char p24_old = '\x0'; char p24_new = '\x0'; _Bool ep24 = 0; port_t p31 = 0; char p31_old = '\x0'; char p31_new = '\x0'; _Bool ep31 = 0; port_t p32 = 0; char p32_old = '\x0'; char p32_new = '\x0'; _Bool ep32 = 0; port_t p34 = 0; char p34_old = '\x0'; char p34_new = '\x0'; _Bool ep34 = 0; port_t p41 = 0; char p41_old = '\x0'; char p41_new = '\x0'; _Bool ep41 = 0; port_t p42 = 0; char p42_old = '\x0'; char p42_new = '\x0'; _Bool ep42 = 0; port_t p43 = 0; char p43_old = '\x0'; char p43_new = '\x0'; _Bool ep43 = 0; char id1 = '\x0'; char r1 = '\x0'; char st1 = '\x0'; char nl1 = '\x0'; char m1 = '\x0'; char max1 = '\x0'; _Bool mode1 = 0; 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_4247; int __return_4457; int __return_4640; int __return_4831; int __return_5014; int __return_5205; int __return_6847; int __return_6804; int __return_6727; int __return_6684; int __return_6573; int __return_6530; int __return_6453; int __return_6407; int __tmp_5398_0; int __return_5571; int __return_5411; int __return_6242; int __return_6199; int __return_6122; int __return_6076; int __return_5945; int __return_5899; int __return_5799; int __return_5397; 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_4069:; init__r122 = (_Bool)init__tmp; if (!(init__r131 == 0)) { init__tmp___0 = 1; label_4074:; init__r132 = (_Bool)init__tmp___0; if (!(init__r141 == 0)) { init__tmp___1 = 1; label_4079:; init__r142 = (_Bool)init__tmp___1; if (!(init__r211 == 0)) { init__tmp___2 = 1; label_4084:; init__r212 = (_Bool)init__tmp___2; if (!(init__r231 == 0)) { init__tmp___3 = 1; label_4089:; init__r232 = (_Bool)init__tmp___3; if (!(init__r241 == 0)) { init__tmp___4 = 1; label_4094:; init__r242 = (_Bool)init__tmp___4; if (!(init__r311 == 0)) { init__tmp___5 = 1; label_4099:; init__r312 = (_Bool)init__tmp___5; if (!(init__r321 == 0)) { init__tmp___6 = 1; label_4104:; init__r322 = (_Bool)init__tmp___6; if (!(init__r341 == 0)) { init__tmp___7 = 1; label_4109:; init__r342 = (_Bool)init__tmp___7; if (!(init__r411 == 0)) { init__tmp___8 = 1; label_4114:; init__r412 = (_Bool)init__tmp___8; if (!(init__r421 == 0)) { init__tmp___9 = 1; label_4119:; init__r422 = (_Bool)init__tmp___9; if (!(init__r431 == 0)) { init__tmp___10 = 1; label_4124:; init__r432 = (_Bool)init__tmp___10; if (!(init__r122 == 0)) { init__tmp___11 = 1; label_4129:; init__r123 = (_Bool)init__tmp___11; if (!(init__r132 == 0)) { init__tmp___12 = 1; label_4134:; init__r133 = (_Bool)init__tmp___12; if (!(init__r142 == 0)) { init__tmp___13 = 1; label_4139:; init__r143 = (_Bool)init__tmp___13; if (!(init__r212 == 0)) { init__tmp___14 = 1; label_4144:; init__r213 = (_Bool)init__tmp___14; if (!(init__r232 == 0)) { init__tmp___15 = 1; label_4149:; init__r233 = (_Bool)init__tmp___15; if (!(init__r242 == 0)) { init__tmp___16 = 1; label_4154:; init__r243 = (_Bool)init__tmp___16; if (!(init__r312 == 0)) { init__tmp___17 = 1; label_4159:; init__r313 = (_Bool)init__tmp___17; if (!(init__r322 == 0)) { init__tmp___18 = 1; label_4164:; init__r323 = (_Bool)init__tmp___18; if (!(init__r342 == 0)) { init__tmp___19 = 1; label_4169:; init__r343 = (_Bool)init__tmp___19; if (!(init__r412 == 0)) { init__tmp___20 = 1; label_4174:; init__r413 = (_Bool)init__tmp___20; if (!(init__r422 == 0)) { init__tmp___21 = 1; label_4179:; init__r423 = (_Bool)init__tmp___21; if (!(init__r432 == 0)) { init__tmp___22 = 1; label_4184:; init__r433 = (_Bool)init__tmp___22; if (((int)id1) != ((int)id2)) { if (((int)id1) != ((int)id3)) { if (((int)id1) != ((int)id4)) { if (((int)id2) != ((int)id3)) { if (((int)id2) != ((int)id4)) { if (((int)id3) != ((int)id4)) { if (((int)id1) >= 0) { if (((int)id2) >= 0) { if (((int)id3) >= 0) { if (((int)id4) >= 0) { if (((int)r1) == 0) { if (((int)r2) == 0) { if (((int)r3) == 0) { if (((int)r4) == 0) { if (((int)max1) == ((int)id1)) { if (((int)max2) == ((int)id2)) { if (((int)max3) == ((int)id3)) { if (((int)max4) == ((int)id4)) { if (((int)st1) == 0) { if (((int)st2) == 0) { if (((int)st3) == 0) { if (((int)st4) == 0) { if (((int)nl1) == 0) { if (((int)nl2) == 0) { if (((int)nl3) == 0) { if (((int)nl4) == 0) { if (((int)mode1) == 0) { if (((int)mode2) == 0) { if (((int)mode3) == 0) { if (((int)mode4) == 0) { init__tmp___23 = 1; __return_4247 = init__tmp___23; main__i2 = __return_4247; 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) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_4287:; p12_new = node1____CPAchecker_TMP_0; label_4282:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4295:; p13_new = node1____CPAchecker_TMP_1; label_4290:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4303:; p14_new = node1____CPAchecker_TMP_2; label_4305:; 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_4319:; p21_new = node2____CPAchecker_TMP_0; label_4314:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4327:; p23_new = node2____CPAchecker_TMP_1; label_4322:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4335:; p24_new = node2____CPAchecker_TMP_2; label_4337:; 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_4351:; p31_new = node3____CPAchecker_TMP_0; label_4346:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4359:; p32_new = node3____CPAchecker_TMP_1; label_4354:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4367:; p34_new = node3____CPAchecker_TMP_2; label_4369:; 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_4383:; p41_new = node4____CPAchecker_TMP_0; label_4378:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4391:; p42_new = node4____CPAchecker_TMP_1; label_4386:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4399:; p43_new = node4____CPAchecker_TMP_2; label_4401:; 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_4457 = check__tmp; main__c1 = __return_4457; { _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_4473:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4480:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4487:; 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_4503:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4510:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4517:; 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_4533:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4540:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4547:; 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_4563:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4570:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4577:; 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_4640 = check__tmp; main__c1 = __return_4640; { _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) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_4661:; p12_new = node1____CPAchecker_TMP_0; label_4656:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4669:; p13_new = node1____CPAchecker_TMP_1; label_4664:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4677:; p14_new = node1____CPAchecker_TMP_2; label_4679:; 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_4693:; p21_new = node2____CPAchecker_TMP_0; label_4688:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4701:; p23_new = node2____CPAchecker_TMP_1; label_4696:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4709:; p24_new = node2____CPAchecker_TMP_2; label_4711:; 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_4725:; p31_new = node3____CPAchecker_TMP_0; label_4720:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4733:; p32_new = node3____CPAchecker_TMP_1; label_4728:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4741:; p34_new = node3____CPAchecker_TMP_2; label_4743:; 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_4757:; p41_new = node4____CPAchecker_TMP_0; label_4752:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4765:; p42_new = node4____CPAchecker_TMP_1; label_4760:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4773:; p43_new = node4____CPAchecker_TMP_2; label_4775:; 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_4831 = check__tmp; main__c1 = __return_4831; { _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_4847:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4854:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4861:; 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_4877:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4884:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4891:; 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_4907:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4914:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4921:; 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_4937:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4944:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4951:; 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_5014 = check__tmp; main__c1 = __return_5014; { _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) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_5035:; p12_new = node1____CPAchecker_TMP_0; label_5030:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5043:; p13_new = node1____CPAchecker_TMP_1; label_5038:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5051:; p14_new = node1____CPAchecker_TMP_2; label_5053:; 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_5067:; p21_new = node2____CPAchecker_TMP_0; label_5062:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5075:; p23_new = node2____CPAchecker_TMP_1; label_5070:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5083:; p24_new = node2____CPAchecker_TMP_2; label_5085:; 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_5099:; p31_new = node3____CPAchecker_TMP_0; label_5094:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5107:; p32_new = node3____CPAchecker_TMP_1; label_5102:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5115:; p34_new = node3____CPAchecker_TMP_2; label_5117:; 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_5131:; p41_new = node4____CPAchecker_TMP_0; label_5126:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5139:; p42_new = node4____CPAchecker_TMP_1; label_5134:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5147:; p43_new = node4____CPAchecker_TMP_2; label_5149:; 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_5205 = check__tmp; main__c1 = __return_5205; { _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_5221:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5228:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5235:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; 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_6259:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_6266:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_6273:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; 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_6590:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6597:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6604:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; 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_6744:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6751:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6758:; 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_6847 = check__tmp; main__c1 = __return_6847; { _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_6804 = check__tmp; main__c1 = __return_6804; { _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_6758; } } else { goto label_6758; } } else { goto label_6751; } } else { goto label_6751; } } else { goto label_6744; } } else { goto label_6744; } } else { return __return_main; } } } else { nl3 = 1; 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_6624:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6631:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6638:; 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_6727 = check__tmp; main__c1 = __return_6727; { _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_6684 = check__tmp; main__c1 = __return_6684; { _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_6638; } } else { goto label_6638; } } else { goto label_6631; } } else { goto label_6631; } } else { goto label_6624; } } else { goto label_6624; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6604; } } else { goto label_6604; } } else { goto label_6597; } } else { goto label_6597; } } else { goto label_6590; } } else { goto label_6590; } } else { return __return_main; } } } else { nl2 = 1; 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_6293:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6300:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6307:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; 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_6470:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6477:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6484:; 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_6573 = check__tmp; main__c1 = __return_6573; { _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_6530 = check__tmp; main__c1 = __return_6530; { _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_6484; } } else { goto label_6484; } } else { goto label_6477; } } else { goto label_6477; } } else { goto label_6470; } } else { goto label_6470; } } else { return __return_main; } } } else { nl3 = 1; 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_6327:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6334:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6341:; 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_6453 = check__tmp; main__c1 = __return_6453; { _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_6408:; if (((int)r1) < 3) { check__tmp = 1; label_6414:; label_6399:; __return_6407 = check__tmp; main__c1 = __return_6407; __tmp_5398_0 = main____CPAchecker_TMP_0; label_5398:; main____CPAchecker_TMP_0 = __tmp_5398_0; { _Bool __tmp_13; __tmp_13 = main__c1; _Bool assert__arg; assert__arg = __tmp_13; if (assert__arg == 0) { {reach_error();} return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { 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_5417:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5424:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5431:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5439:; mode1 = 0; label_5441:; { 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_5449:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5456:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5463:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5471:; mode2 = 0; label_5473:; { 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_5481:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5488:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5495:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5503:; mode3 = 0; label_5505:; { 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_5513:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5520:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5527:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5535:; mode4 = 0; label_5537:; 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_5594:; if (((int)r1) < 3) { label_5601:; if (((int)r1) >= 3) { label_5608:; if (((int)r1) < 3) { check__tmp = 1; label_5614:; label_5607:; label_5600:; label_5593:; label_5587:; label_5583:; label_5579:; label_5575:; label_5570:; __return_5571 = check__tmp; main__c1 = __return_5571; __tmp_5398_0 = main____CPAchecker_TMP_0; goto label_5398; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5614; } else { check__tmp = 0; goto label_5614; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5608; } else { check__tmp = 0; goto label_5607; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_5601; } else { check__tmp = 0; goto label_5600; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_5594; } else { check__tmp = 0; goto label_5593; } } } else { check__tmp = 0; goto label_5587; } } else { check__tmp = 0; goto label_5583; } } else { check__tmp = 0; goto label_5579; } } else { check__tmp = 0; goto label_5575; } } else { check__tmp = 0; goto label_5570; } } } else { nl4 = 1; goto label_5535; } } else { goto label_5535; } } else { goto label_5527; } } else { goto label_5527; } } else { goto label_5520; } } else { goto label_5520; } } else { goto label_5513; } } else { goto label_5513; } } 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_5629:; p41_new = node4____CPAchecker_TMP_0; label_5624:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5637:; p42_new = node4____CPAchecker_TMP_1; label_5632:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5645:; p43_new = node4____CPAchecker_TMP_2; label_5622:; mode4 = 1; goto label_5537; } else { label_5644:; node4____CPAchecker_TMP_2 = p43_new; goto label_5645; } } else { goto label_5644; } } else { goto label_5622; } } else { label_5636:; node4____CPAchecker_TMP_1 = p42_new; goto label_5637; } } else { goto label_5636; } } else { goto label_5632; } } else { label_5628:; node4____CPAchecker_TMP_0 = p41_new; goto label_5629; } } else { goto label_5628; } } else { goto label_5624; } } else { goto label_5622; } } } } else { nl3 = 1; goto label_5503; } } else { goto label_5503; } } else { goto label_5495; } } else { goto label_5495; } } else { goto label_5488; } } else { goto label_5488; } } else { goto label_5481; } } else { goto label_5481; } } 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_5660:; p31_new = node3____CPAchecker_TMP_0; label_5655:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5668:; p32_new = node3____CPAchecker_TMP_1; label_5663:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5676:; p34_new = node3____CPAchecker_TMP_2; label_5653:; mode3 = 1; goto label_5505; } else { label_5675:; node3____CPAchecker_TMP_2 = p34_new; goto label_5676; } } else { goto label_5675; } } else { goto label_5653; } } else { label_5667:; node3____CPAchecker_TMP_1 = p32_new; goto label_5668; } } else { goto label_5667; } } else { goto label_5663; } } else { label_5659:; node3____CPAchecker_TMP_0 = p31_new; goto label_5660; } } else { goto label_5659; } } else { goto label_5655; } } else { goto label_5653; } } } } else { nl2 = 1; goto label_5471; } } else { goto label_5471; } } else { goto label_5463; } } else { goto label_5463; } } else { goto label_5456; } } else { goto label_5456; } } else { goto label_5449; } } else { goto label_5449; } } 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_5691:; p21_new = node2____CPAchecker_TMP_0; label_5686:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5699:; p23_new = node2____CPAchecker_TMP_1; label_5694:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5707:; p24_new = node2____CPAchecker_TMP_2; label_5684:; mode2 = 1; goto label_5473; } else { label_5706:; node2____CPAchecker_TMP_2 = p24_new; goto label_5707; } } else { goto label_5706; } } else { goto label_5684; } } else { label_5698:; node2____CPAchecker_TMP_1 = p23_new; goto label_5699; } } else { goto label_5698; } } else { goto label_5694; } } else { label_5690:; node2____CPAchecker_TMP_0 = p21_new; goto label_5691; } } else { goto label_5690; } } else { goto label_5686; } } else { goto label_5684; } } } } else { nl1 = 1; goto label_5439; } } else { goto label_5439; } } else { goto label_5431; } } else { goto label_5431; } } else { goto label_5424; } } else { goto label_5424; } } else { goto label_5417; } } else { goto label_5417; } } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_5722:; p12_new = node1____CPAchecker_TMP_0; label_5717:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5730:; p13_new = node1____CPAchecker_TMP_1; label_5725:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5738:; p14_new = node1____CPAchecker_TMP_2; label_5715:; mode1 = 1; goto label_5441; } else { label_5737:; node1____CPAchecker_TMP_2 = p14_new; goto label_5738; } } else { goto label_5737; } } else { goto label_5715; } } else { label_5729:; node1____CPAchecker_TMP_1 = p13_new; goto label_5730; } } else { goto label_5729; } } else { goto label_5725; } } else { label_5721:; node1____CPAchecker_TMP_0 = p12_new; goto label_5722; } } else { goto label_5721; } } else { goto label_5717; } } else { goto label_5715; } } } } else { __return_5411 = 0; return __return_5411; } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6414; } else { check__tmp = 0; goto label_6414; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6408; } else { check__tmp = 0; goto label_6399; } } } else { return __return_main; } } } else { return __return_main; } } else { 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_6341; } } else { goto label_6341; } } else { goto label_6334; } } else { goto label_6334; } } else { goto label_6327; } } else { goto label_6327; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6307; } } else { goto label_6307; } } else { goto label_6300; } } else { goto label_6300; } } else { goto label_6293; } } else { goto label_6293; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6273; } } else { goto label_6273; } } else { goto label_6266; } } else { goto label_6266; } } else { goto label_6259; } } else { goto label_6259; } } else { return __return_main; } } } else { nl1 = 1; 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_5255:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5262:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5269:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; 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_5962:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5969:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5976:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; 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_6139:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6146:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6153:; 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_6242 = check__tmp; main__c1 = __return_6242; { _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_6199 = check__tmp; main__c1 = __return_6199; { _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_6153; } } else { goto label_6153; } } else { goto label_6146; } } else { goto label_6146; } } else { goto label_6139; } } else { goto label_6139; } } else { return __return_main; } } } else { nl3 = 1; 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_5996:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6003:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6010:; 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_6122 = check__tmp; main__c1 = __return_6122; { _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_6077:; if (((int)r1) < 3) { check__tmp = 1; label_6083:; label_6068:; __return_6076 = check__tmp; main__c1 = __return_6076; __tmp_5398_0 = main____CPAchecker_TMP_0; goto label_5398; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6083; } else { check__tmp = 0; goto label_6083; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6077; } else { check__tmp = 0; goto label_6068; } } } else { return __return_main; } } } else { return __return_main; } } else { 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_6010; } } else { goto label_6010; } } else { goto label_6003; } } else { goto label_6003; } } else { goto label_5996; } } else { goto label_5996; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5976; } } else { goto label_5976; } } else { goto label_5969; } } else { goto label_5969; } } else { goto label_5962; } } else { goto label_5962; } } else { return __return_main; } } } else { nl2 = 1; 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_5289:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5296:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5303:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; 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_5819:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5826:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5833:; 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_5945 = check__tmp; main__c1 = __return_5945; { _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_5900:; if (((int)r1) < 3) { check__tmp = 1; label_5906:; label_5891:; __return_5899 = check__tmp; main__c1 = __return_5899; __tmp_5398_0 = main____CPAchecker_TMP_0; goto label_5398; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5906; } else { check__tmp = 0; goto label_5906; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5900; } else { check__tmp = 0; goto label_5891; } } } else { return __return_main; } } } else { return __return_main; } } else { 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_5833; } } else { goto label_5833; } } else { goto label_5826; } } else { goto label_5826; } } else { goto label_5819; } } else { goto label_5819; } } else { return __return_main; } } } else { nl3 = 1; 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_5323:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5330:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5337:; 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_5800:; if (((int)r1) < 3) { check__tmp = 1; label_5806:; label_5791:; __return_5799 = check__tmp; main__c1 = __return_5799; __tmp_5398_0 = main____CPAchecker_TMP_0; goto label_5398; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5806; } else { check__tmp = 0; goto label_5806; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5800; } else { check__tmp = 0; goto label_5791; } } } else { return __return_main; } } } else { 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_5397 = check__tmp; main__c1 = __return_5397; __tmp_5398_0 = main____CPAchecker_TMP_0; goto label_5398; } } } else { return __return_main; } } else { 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_5337; } } else { goto label_5337; } } else { goto label_5330; } } else { goto label_5330; } } else { goto label_5323; } } else { goto label_5323; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5303; } } else { goto label_5303; } } else { goto label_5296; } } else { goto label_5296; } } else { goto label_5289; } } else { goto label_5289; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5269; } } else { goto label_5269; } } else { goto label_5262; } } else { goto label_5262; } } else { goto label_5255; } } else { goto label_5255; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5235; } } else { goto label_5235; } } else { goto label_5228; } } else { goto label_5228; } } else { goto label_5221; } } else { goto label_5221; } } else { return __return_main; } } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_5146:; node4____CPAchecker_TMP_2 = p43_new; goto label_5147; } } else { goto label_5146; } } else { goto label_5149; } } else { label_5138:; node4____CPAchecker_TMP_1 = p42_new; goto label_5139; } } else { goto label_5138; } } else { goto label_5134; } } else { label_5130:; node4____CPAchecker_TMP_0 = p41_new; goto label_5131; } } else { goto label_5130; } } else { goto label_5126; } } else { return __return_main; } } } } else { label_5114:; node3____CPAchecker_TMP_2 = p34_new; goto label_5115; } } else { goto label_5114; } } else { goto label_5117; } } else { label_5106:; node3____CPAchecker_TMP_1 = p32_new; goto label_5107; } } else { goto label_5106; } } else { goto label_5102; } } else { label_5098:; node3____CPAchecker_TMP_0 = p31_new; goto label_5099; } } else { goto label_5098; } } else { goto label_5094; } } else { return __return_main; } } } } else { label_5082:; node2____CPAchecker_TMP_2 = p24_new; goto label_5083; } } else { goto label_5082; } } else { goto label_5085; } } else { label_5074:; node2____CPAchecker_TMP_1 = p23_new; goto label_5075; } } else { goto label_5074; } } else { goto label_5070; } } else { label_5066:; node2____CPAchecker_TMP_0 = p21_new; goto label_5067; } } else { goto label_5066; } } else { goto label_5062; } } else { return __return_main; } } } } else { label_5050:; node1____CPAchecker_TMP_2 = p14_new; goto label_5051; } } else { goto label_5050; } } else { goto label_5053; } } else { label_5042:; node1____CPAchecker_TMP_1 = p13_new; goto label_5043; } } else { goto label_5042; } } else { goto label_5038; } } else { label_5034:; node1____CPAchecker_TMP_0 = p12_new; goto label_5035; } } else { goto label_5034; } } else { goto label_5030; } } else { return __return_main; } } } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4951; } } else { goto label_4951; } } else { goto label_4944; } } else { goto label_4944; } } else { goto label_4937; } } else { goto label_4937; } } else { return __return_main; } } } } else { goto label_4921; } } else { goto label_4921; } } else { goto label_4914; } } else { goto label_4914; } } else { goto label_4907; } } else { goto label_4907; } } else { return __return_main; } } } } else { goto label_4891; } } else { goto label_4891; } } else { goto label_4884; } } else { goto label_4884; } } else { goto label_4877; } } else { goto label_4877; } } else { return __return_main; } } } } else { goto label_4861; } } else { goto label_4861; } } else { goto label_4854; } } else { goto label_4854; } } else { goto label_4847; } } else { goto label_4847; } } else { return __return_main; } } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4772:; node4____CPAchecker_TMP_2 = p43_new; goto label_4773; } } else { goto label_4772; } } else { goto label_4775; } } else { label_4764:; node4____CPAchecker_TMP_1 = p42_new; goto label_4765; } } else { goto label_4764; } } else { goto label_4760; } } else { label_4756:; node4____CPAchecker_TMP_0 = p41_new; goto label_4757; } } else { goto label_4756; } } else { goto label_4752; } } else { return __return_main; } } } } else { label_4740:; node3____CPAchecker_TMP_2 = p34_new; goto label_4741; } } else { goto label_4740; } } else { goto label_4743; } } else { label_4732:; node3____CPAchecker_TMP_1 = p32_new; goto label_4733; } } else { goto label_4732; } } else { goto label_4728; } } else { label_4724:; node3____CPAchecker_TMP_0 = p31_new; goto label_4725; } } else { goto label_4724; } } else { goto label_4720; } } else { return __return_main; } } } } else { label_4708:; node2____CPAchecker_TMP_2 = p24_new; goto label_4709; } } else { goto label_4708; } } else { goto label_4711; } } else { label_4700:; node2____CPAchecker_TMP_1 = p23_new; goto label_4701; } } else { goto label_4700; } } else { goto label_4696; } } else { label_4692:; node2____CPAchecker_TMP_0 = p21_new; goto label_4693; } } else { goto label_4692; } } else { goto label_4688; } } else { return __return_main; } } } } else { label_4676:; node1____CPAchecker_TMP_2 = p14_new; goto label_4677; } } else { goto label_4676; } } else { goto label_4679; } } else { label_4668:; node1____CPAchecker_TMP_1 = p13_new; goto label_4669; } } else { goto label_4668; } } else { goto label_4664; } } else { label_4660:; node1____CPAchecker_TMP_0 = p12_new; goto label_4661; } } else { goto label_4660; } } else { goto label_4656; } } else { return __return_main; } } } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4577; } } else { goto label_4577; } } else { goto label_4570; } } else { goto label_4570; } } else { goto label_4563; } } else { goto label_4563; } } else { return __return_main; } } } } else { goto label_4547; } } else { goto label_4547; } } else { goto label_4540; } } else { goto label_4540; } } else { goto label_4533; } } else { goto label_4533; } } else { return __return_main; } } } } else { goto label_4517; } } else { goto label_4517; } } else { goto label_4510; } } else { goto label_4510; } } else { goto label_4503; } } else { goto label_4503; } } else { return __return_main; } } } } else { goto label_4487; } } else { goto label_4487; } } else { goto label_4480; } } else { goto label_4480; } } else { goto label_4473; } } else { goto label_4473; } } else { return __return_main; } } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4398:; node4____CPAchecker_TMP_2 = p43_new; goto label_4399; } } else { goto label_4398; } } else { goto label_4401; } } else { label_4390:; node4____CPAchecker_TMP_1 = p42_new; goto label_4391; } } else { goto label_4390; } } else { goto label_4386; } } else { label_4382:; node4____CPAchecker_TMP_0 = p41_new; goto label_4383; } } else { goto label_4382; } } else { goto label_4378; } } else { return __return_main; } } } } else { label_4366:; node3____CPAchecker_TMP_2 = p34_new; goto label_4367; } } else { goto label_4366; } } else { goto label_4369; } } else { label_4358:; node3____CPAchecker_TMP_1 = p32_new; goto label_4359; } } else { goto label_4358; } } else { goto label_4354; } } else { label_4350:; node3____CPAchecker_TMP_0 = p31_new; goto label_4351; } } else { goto label_4350; } } else { goto label_4346; } } else { return __return_main; } } } } else { label_4334:; node2____CPAchecker_TMP_2 = p24_new; goto label_4335; } } else { goto label_4334; } } else { goto label_4337; } } else { label_4326:; node2____CPAchecker_TMP_1 = p23_new; goto label_4327; } } else { goto label_4326; } } else { goto label_4322; } } else { label_4318:; node2____CPAchecker_TMP_0 = p21_new; goto label_4319; } } else { goto label_4318; } } else { goto label_4314; } } else { return __return_main; } } } } else { label_4302:; node1____CPAchecker_TMP_2 = p14_new; goto label_4303; } } else { goto label_4302; } } else { goto label_4305; } } else { label_4294:; node1____CPAchecker_TMP_1 = p13_new; goto label_4295; } } else { goto label_4294; } } else { goto label_4290; } } else { label_4286:; node1____CPAchecker_TMP_0 = p12_new; goto label_4287; } } else { goto label_4286; } } else { goto label_4282; } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { 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_4184; } else { label_6872:; if (!(init__r422 == 0)) { if (!(ep23 == 0)) { init__tmp___22 = 1; label_6878:; goto label_4184; } else { init__tmp___22 = 0; goto label_6878; } } else { init__tmp___22 = 0; goto label_4184; } } } else { goto label_6872; } } } else { if (!(init__r412 == 0)) { if (!(ep12 == 0)) { init__tmp___21 = 1; goto label_4179; } else { label_6887:; if (!(init__r432 == 0)) { if (!(ep32 == 0)) { init__tmp___21 = 1; label_6893:; goto label_4179; } else { init__tmp___21 = 0; goto label_6893; } } else { init__tmp___21 = 0; goto label_4179; } } } else { goto label_6887; } } } else { if (!(init__r422 == 0)) { if (!(ep21 == 0)) { init__tmp___20 = 1; goto label_4174; } else { label_6902:; if (!(init__r432 == 0)) { if (!(ep31 == 0)) { init__tmp___20 = 1; label_6908:; goto label_4174; } else { init__tmp___20 = 0; goto label_6908; } } else { init__tmp___20 = 0; goto label_4174; } } } else { goto label_6902; } } } else { if (!(init__r312 == 0)) { if (!(ep14 == 0)) { init__tmp___19 = 1; goto label_4169; } else { label_6917:; if (!(init__r322 == 0)) { if (!(ep24 == 0)) { init__tmp___19 = 1; label_6923:; goto label_4169; } else { init__tmp___19 = 0; goto label_6923; } } else { init__tmp___19 = 0; goto label_4169; } } } else { goto label_6917; } } } else { if (!(init__r312 == 0)) { if (!(ep12 == 0)) { init__tmp___18 = 1; goto label_4164; } else { label_6932:; if (!(init__r342 == 0)) { if (!(ep42 == 0)) { init__tmp___18 = 1; label_6938:; goto label_4164; } else { init__tmp___18 = 0; goto label_6938; } } else { init__tmp___18 = 0; goto label_4164; } } } else { goto label_6932; } } } else { if (!(init__r322 == 0)) { if (!(ep21 == 0)) { init__tmp___17 = 1; goto label_4159; } else { label_6947:; if (!(init__r342 == 0)) { if (!(ep41 == 0)) { init__tmp___17 = 1; label_6953:; goto label_4159; } else { init__tmp___17 = 0; goto label_6953; } } else { init__tmp___17 = 0; goto label_4159; } } } else { goto label_6947; } } } else { if (!(init__r212 == 0)) { if (!(ep14 == 0)) { init__tmp___16 = 1; goto label_4154; } else { label_6962:; if (!(init__r232 == 0)) { if (!(ep34 == 0)) { init__tmp___16 = 1; label_6968:; goto label_4154; } else { init__tmp___16 = 0; goto label_6968; } } else { init__tmp___16 = 0; goto label_4154; } } } else { goto label_6962; } } } else { if (!(init__r212 == 0)) { if (!(ep13 == 0)) { init__tmp___15 = 1; goto label_4149; } else { label_6977:; if (!(init__r242 == 0)) { if (!(ep43 == 0)) { init__tmp___15 = 1; label_6983:; goto label_4149; } else { init__tmp___15 = 0; goto label_6983; } } else { init__tmp___15 = 0; goto label_4149; } } } else { goto label_6977; } } } else { if (!(init__r232 == 0)) { if (!(ep31 == 0)) { init__tmp___14 = 1; goto label_4144; } else { label_6992:; if (!(init__r242 == 0)) { if (!(ep41 == 0)) { init__tmp___14 = 1; label_6998:; goto label_4144; } else { init__tmp___14 = 0; goto label_6998; } } else { init__tmp___14 = 0; goto label_4144; } } } else { goto label_6992; } } } else { if (!(init__r122 == 0)) { if (!(ep24 == 0)) { init__tmp___13 = 1; goto label_4139; } else { label_7007:; if (!(init__r132 == 0)) { if (!(ep34 == 0)) { init__tmp___13 = 1; label_7013:; goto label_4139; } else { init__tmp___13 = 0; goto label_7013; } } else { init__tmp___13 = 0; goto label_4139; } } } else { goto label_7007; } } } else { if (!(init__r122 == 0)) { if (!(ep23 == 0)) { init__tmp___12 = 1; goto label_4134; } else { label_7022:; if (!(init__r142 == 0)) { if (!(ep43 == 0)) { init__tmp___12 = 1; label_7028:; goto label_4134; } else { init__tmp___12 = 0; goto label_7028; } } else { init__tmp___12 = 0; goto label_4134; } } } else { goto label_7022; } } } else { if (!(init__r132 == 0)) { if (!(ep32 == 0)) { init__tmp___11 = 1; goto label_4129; } else { label_7037:; if (!(init__r142 == 0)) { if (!(ep42 == 0)) { init__tmp___11 = 1; label_7043:; goto label_4129; } else { init__tmp___11 = 0; goto label_7043; } } else { init__tmp___11 = 0; goto label_4129; } } } else { goto label_7037; } } } else { if (!(init__r411 == 0)) { if (!(ep13 == 0)) { init__tmp___10 = 1; goto label_4124; } else { label_7052:; if (!(init__r421 == 0)) { if (!(ep23 == 0)) { init__tmp___10 = 1; label_7058:; goto label_4124; } else { init__tmp___10 = 0; goto label_7058; } } else { init__tmp___10 = 0; goto label_4124; } } } else { goto label_7052; } } } else { if (!(init__r411 == 0)) { if (!(ep12 == 0)) { init__tmp___9 = 1; goto label_4119; } else { label_7067:; if (!(init__r431 == 0)) { if (!(ep32 == 0)) { init__tmp___9 = 1; label_7073:; goto label_4119; } else { init__tmp___9 = 0; goto label_7073; } } else { init__tmp___9 = 0; goto label_4119; } } } else { goto label_7067; } } } else { if (!(init__r421 == 0)) { if (!(ep21 == 0)) { init__tmp___8 = 1; goto label_4114; } else { label_7082:; if (!(init__r431 == 0)) { if (!(ep31 == 0)) { init__tmp___8 = 1; label_7088:; goto label_4114; } else { init__tmp___8 = 0; goto label_7088; } } else { init__tmp___8 = 0; goto label_4114; } } } else { goto label_7082; } } } else { if (!(init__r311 == 0)) { if (!(ep14 == 0)) { init__tmp___7 = 1; goto label_4109; } else { label_7097:; if (!(init__r321 == 0)) { if (!(ep24 == 0)) { init__tmp___7 = 1; label_7103:; goto label_4109; } else { init__tmp___7 = 0; goto label_7103; } } else { init__tmp___7 = 0; goto label_4109; } } } else { goto label_7097; } } } else { if (!(init__r311 == 0)) { if (!(ep12 == 0)) { init__tmp___6 = 1; goto label_4104; } else { label_7112:; if (!(init__r341 == 0)) { if (!(ep42 == 0)) { init__tmp___6 = 1; label_7118:; goto label_4104; } else { init__tmp___6 = 0; goto label_7118; } } else { init__tmp___6 = 0; goto label_4104; } } } else { goto label_7112; } } } else { if (!(init__r321 == 0)) { if (!(ep21 == 0)) { init__tmp___5 = 1; goto label_4099; } else { label_7127:; if (!(init__r341 == 0)) { if (!(ep41 == 0)) { init__tmp___5 = 1; label_7133:; goto label_4099; } else { init__tmp___5 = 0; goto label_7133; } } else { init__tmp___5 = 0; goto label_4099; } } } else { goto label_7127; } } } else { if (!(init__r211 == 0)) { if (!(ep14 == 0)) { init__tmp___4 = 1; goto label_4094; } else { label_7142:; if (!(init__r231 == 0)) { if (!(ep34 == 0)) { init__tmp___4 = 1; label_7148:; goto label_4094; } else { init__tmp___4 = 0; goto label_7148; } } else { init__tmp___4 = 0; goto label_4094; } } } else { goto label_7142; } } } else { if (!(init__r211 == 0)) { if (!(ep13 == 0)) { init__tmp___3 = 1; goto label_4089; } else { label_7157:; if (!(init__r241 == 0)) { if (!(ep43 == 0)) { init__tmp___3 = 1; label_7163:; goto label_4089; } else { init__tmp___3 = 0; goto label_7163; } } else { init__tmp___3 = 0; goto label_4089; } } } else { goto label_7157; } } } else { if (!(init__r231 == 0)) { if (!(ep31 == 0)) { init__tmp___2 = 1; goto label_4084; } else { label_7172:; if (!(init__r241 == 0)) { if (!(ep41 == 0)) { init__tmp___2 = 1; label_7178:; goto label_4084; } else { init__tmp___2 = 0; goto label_7178; } } else { init__tmp___2 = 0; goto label_4084; } } } else { goto label_7172; } } } else { if (!(init__r121 == 0)) { if (!(ep24 == 0)) { init__tmp___1 = 1; goto label_4079; } else { label_7187:; if (!(init__r131 == 0)) { if (!(ep34 == 0)) { init__tmp___1 = 1; label_7193:; goto label_4079; } else { init__tmp___1 = 0; goto label_7193; } } else { init__tmp___1 = 0; goto label_4079; } } } else { goto label_7187; } } } else { if (!(init__r121 == 0)) { if (!(ep23 == 0)) { init__tmp___0 = 1; goto label_4074; } else { label_7202:; if (!(init__r141 == 0)) { if (!(ep43 == 0)) { init__tmp___0 = 1; label_7208:; goto label_4074; } else { init__tmp___0 = 0; goto label_7208; } } else { init__tmp___0 = 0; goto label_4074; } } } else { goto label_7202; } } } else { if (!(init__r131 == 0)) { if (!(ep32 == 0)) { init__tmp = 1; goto label_4069; } else { label_7217:; if (!(init__r141 == 0)) { if (!(ep42 == 0)) { init__tmp = 1; label_7223:; goto label_4069; } else { init__tmp = 0; goto label_7223; } } else { init__tmp = 0; goto label_4069; } } } else { goto label_7217; } } } }