// 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.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_4295; int __return_4505; int __return_4688; int __return_4879; int __return_5062; int __return_5253; int __return_6895; int __return_6852; int __return_6775; int __return_6732; int __return_6621; int __return_6578; int __return_6501; int __return_6455; int __tmp_5446_0; int __return_5619; int __return_5459; int __return_6290; int __return_6247; int __return_6170; int __return_6124; int __return_5993; int __return_5947; int __return_5847; int __return_5445; 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_4093:; init__r122 = (_Bool)init__tmp; if (!(init__r131 == 0)) { init__tmp___0 = 1; label_4098:; init__r132 = (_Bool)init__tmp___0; if (!(init__r141 == 0)) { init__tmp___1 = 1; label_4103:; init__r142 = (_Bool)init__tmp___1; if (!(init__r211 == 0)) { init__tmp___2 = 1; label_4108:; init__r212 = (_Bool)init__tmp___2; if (!(init__r231 == 0)) { init__tmp___3 = 1; label_4113:; init__r232 = (_Bool)init__tmp___3; if (!(init__r241 == 0)) { init__tmp___4 = 1; label_4118:; init__r242 = (_Bool)init__tmp___4; if (!(init__r311 == 0)) { init__tmp___5 = 1; label_4123:; init__r312 = (_Bool)init__tmp___5; if (!(init__r321 == 0)) { init__tmp___6 = 1; label_4128:; init__r322 = (_Bool)init__tmp___6; if (!(init__r341 == 0)) { init__tmp___7 = 1; label_4133:; init__r342 = (_Bool)init__tmp___7; if (!(init__r411 == 0)) { init__tmp___8 = 1; label_4138:; init__r412 = (_Bool)init__tmp___8; if (!(init__r421 == 0)) { init__tmp___9 = 1; label_4143:; init__r422 = (_Bool)init__tmp___9; if (!(init__r431 == 0)) { init__tmp___10 = 1; label_4148:; init__r432 = (_Bool)init__tmp___10; if (!(init__r122 == 0)) { init__tmp___11 = 1; label_4153:; init__r123 = (_Bool)init__tmp___11; if (!(init__r132 == 0)) { init__tmp___12 = 1; label_4158:; init__r133 = (_Bool)init__tmp___12; if (!(init__r142 == 0)) { init__tmp___13 = 1; label_4163:; init__r143 = (_Bool)init__tmp___13; if (!(init__r212 == 0)) { init__tmp___14 = 1; label_4168:; init__r213 = (_Bool)init__tmp___14; if (!(init__r232 == 0)) { init__tmp___15 = 1; label_4173:; init__r233 = (_Bool)init__tmp___15; if (!(init__r242 == 0)) { init__tmp___16 = 1; label_4178:; init__r243 = (_Bool)init__tmp___16; if (!(init__r312 == 0)) { init__tmp___17 = 1; label_4183:; init__r313 = (_Bool)init__tmp___17; if (!(init__r322 == 0)) { init__tmp___18 = 1; label_4188:; init__r323 = (_Bool)init__tmp___18; if (!(init__r342 == 0)) { init__tmp___19 = 1; label_4193:; init__r343 = (_Bool)init__tmp___19; if (!(init__r412 == 0)) { init__tmp___20 = 1; label_4198:; init__r413 = (_Bool)init__tmp___20; if (!(init__r422 == 0)) { init__tmp___21 = 1; label_4203:; init__r423 = (_Bool)init__tmp___21; if (!(init__r432 == 0)) { init__tmp___22 = 1; label_4208:; 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_4295 = init__tmp___23; main__i2 = __return_4295; 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_4335:; p12_new = node1____CPAchecker_TMP_0; label_4330:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4343:; p13_new = node1____CPAchecker_TMP_1; label_4338:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4351:; p14_new = node1____CPAchecker_TMP_2; label_4353:; 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_4367:; p21_new = node2____CPAchecker_TMP_0; label_4362:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4375:; p23_new = node2____CPAchecker_TMP_1; label_4370:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4383:; p24_new = node2____CPAchecker_TMP_2; label_4385:; 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_4399:; p31_new = node3____CPAchecker_TMP_0; label_4394:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4407:; p32_new = node3____CPAchecker_TMP_1; label_4402:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4415:; p34_new = node3____CPAchecker_TMP_2; label_4417:; 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_4431:; p41_new = node4____CPAchecker_TMP_0; label_4426:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4439:; p42_new = node4____CPAchecker_TMP_1; label_4434:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4447:; p43_new = node4____CPAchecker_TMP_2; label_4449:; 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_4505 = check__tmp; main__c1 = __return_4505; { _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_4521:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4528:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4535:; 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_4551:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4558:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4565:; 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_4581:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4588:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4595:; 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_4611:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4618:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4625:; 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_4688 = check__tmp; main__c1 = __return_4688; { _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_4709:; p12_new = node1____CPAchecker_TMP_0; label_4704:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4717:; p13_new = node1____CPAchecker_TMP_1; label_4712:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4725:; p14_new = node1____CPAchecker_TMP_2; label_4727:; 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_4741:; p21_new = node2____CPAchecker_TMP_0; label_4736:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4749:; p23_new = node2____CPAchecker_TMP_1; label_4744:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4757:; p24_new = node2____CPAchecker_TMP_2; label_4759:; 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_4773:; p31_new = node3____CPAchecker_TMP_0; label_4768:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4781:; p32_new = node3____CPAchecker_TMP_1; label_4776:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4789:; p34_new = node3____CPAchecker_TMP_2; label_4791:; 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_4805:; p41_new = node4____CPAchecker_TMP_0; label_4800:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4813:; p42_new = node4____CPAchecker_TMP_1; label_4808:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4821:; p43_new = node4____CPAchecker_TMP_2; label_4823:; 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_4879 = check__tmp; main__c1 = __return_4879; { _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_4895:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4902:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4909:; 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_4925:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4932:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4939:; 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_4955:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4962:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4969:; 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_4985:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4992:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4999:; 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_5062 = check__tmp; main__c1 = __return_5062; { _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_5083:; p12_new = node1____CPAchecker_TMP_0; label_5078:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5091:; p13_new = node1____CPAchecker_TMP_1; label_5086:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5099:; p14_new = node1____CPAchecker_TMP_2; label_5101:; 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_5115:; p21_new = node2____CPAchecker_TMP_0; label_5110:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5123:; p23_new = node2____CPAchecker_TMP_1; label_5118:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5131:; p24_new = node2____CPAchecker_TMP_2; label_5133:; 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_5147:; p31_new = node3____CPAchecker_TMP_0; label_5142:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5155:; p32_new = node3____CPAchecker_TMP_1; label_5150:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5163:; p34_new = node3____CPAchecker_TMP_2; label_5165:; 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_5179:; p41_new = node4____CPAchecker_TMP_0; label_5174:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5187:; p42_new = node4____CPAchecker_TMP_1; label_5182:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5195:; p43_new = node4____CPAchecker_TMP_2; label_5197:; 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_5253 = check__tmp; main__c1 = __return_5253; { _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_5269:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5276:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5283:; 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_6307:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_6314:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_6321:; 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_6638:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6645:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6652:; 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_6792:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6799:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6806:; 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_6895 = check__tmp; main__c1 = __return_6895; { _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_6852 = check__tmp; main__c1 = __return_6852; { _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_6806; } } else { goto label_6806; } } else { goto label_6799; } } else { goto label_6799; } } else { goto label_6792; } } else { goto label_6792; } } 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_6672:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6679:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6686:; 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_6775 = check__tmp; main__c1 = __return_6775; { _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_6732 = check__tmp; main__c1 = __return_6732; { _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_6686; } } else { goto label_6686; } } else { goto label_6679; } } else { goto label_6679; } } else { goto label_6672; } } else { goto label_6672; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6652; } } else { goto label_6652; } } else { goto label_6645; } } else { goto label_6645; } } else { goto label_6638; } } else { goto label_6638; } } 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_6341:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6348:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6355:; 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_6518:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6525:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6532:; 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_6621 = check__tmp; main__c1 = __return_6621; { _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_6578 = check__tmp; main__c1 = __return_6578; { _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_6532; } } else { goto label_6532; } } else { goto label_6525; } } else { goto label_6525; } } else { goto label_6518; } } else { goto label_6518; } } 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_6375:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6382:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6389:; 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_6501 = check__tmp; main__c1 = __return_6501; { _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_6456:; if (((int)r1) < 3) { check__tmp = 1; label_6462:; label_6447:; __return_6455 = check__tmp; main__c1 = __return_6455; __tmp_5446_0 = main____CPAchecker_TMP_0; label_5446:; main____CPAchecker_TMP_0 = __tmp_5446_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_5465:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5472:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5479:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5487:; mode1 = 0; label_5489:; { 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_5497:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5504:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5511:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5519:; mode2 = 0; label_5521:; { 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_5529:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5536:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5543:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5551:; mode3 = 0; label_5553:; { 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_5561:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5568:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5575:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5583:; mode4 = 0; label_5585:; 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_5642:; if (((int)r1) < 3) { label_5649:; if (((int)r1) >= 3) { label_5656:; if (((int)r1) < 3) { check__tmp = 1; label_5662:; label_5655:; label_5648:; label_5641:; label_5635:; label_5631:; label_5627:; label_5623:; label_5618:; __return_5619 = check__tmp; main__c1 = __return_5619; __tmp_5446_0 = main____CPAchecker_TMP_0; goto label_5446; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5662; } else { check__tmp = 0; goto label_5662; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5656; } else { check__tmp = 0; goto label_5655; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_5649; } else { check__tmp = 0; goto label_5648; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_5642; } else { check__tmp = 0; goto label_5641; } } } else { check__tmp = 0; goto label_5635; } } else { check__tmp = 0; goto label_5631; } } else { check__tmp = 0; goto label_5627; } } else { check__tmp = 0; goto label_5623; } } else { check__tmp = 0; goto label_5618; } } } else { nl4 = 1; goto label_5583; } } else { goto label_5583; } } else { goto label_5575; } } else { goto label_5575; } } else { goto label_5568; } } else { goto label_5568; } } else { goto label_5561; } } else { goto label_5561; } } 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_5677:; p41_new = node4____CPAchecker_TMP_0; label_5672:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5685:; p42_new = node4____CPAchecker_TMP_1; label_5680:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5693:; p43_new = node4____CPAchecker_TMP_2; label_5670:; mode4 = 1; goto label_5585; } else { label_5692:; node4____CPAchecker_TMP_2 = p43_new; goto label_5693; } } else { goto label_5692; } } else { goto label_5670; } } else { label_5684:; node4____CPAchecker_TMP_1 = p42_new; goto label_5685; } } else { goto label_5684; } } else { goto label_5680; } } else { label_5676:; node4____CPAchecker_TMP_0 = p41_new; goto label_5677; } } else { goto label_5676; } } else { goto label_5672; } } else { goto label_5670; } } } } else { nl3 = 1; goto label_5551; } } else { goto label_5551; } } else { goto label_5543; } } else { goto label_5543; } } else { goto label_5536; } } else { goto label_5536; } } else { goto label_5529; } } else { goto label_5529; } } 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_5708:; p31_new = node3____CPAchecker_TMP_0; label_5703:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5716:; p32_new = node3____CPAchecker_TMP_1; label_5711:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5724:; p34_new = node3____CPAchecker_TMP_2; label_5701:; mode3 = 1; goto label_5553; } else { label_5723:; node3____CPAchecker_TMP_2 = p34_new; goto label_5724; } } else { goto label_5723; } } else { goto label_5701; } } else { label_5715:; node3____CPAchecker_TMP_1 = p32_new; goto label_5716; } } else { goto label_5715; } } else { goto label_5711; } } else { label_5707:; node3____CPAchecker_TMP_0 = p31_new; goto label_5708; } } else { goto label_5707; } } else { goto label_5703; } } else { goto label_5701; } } } } else { nl2 = 1; goto label_5519; } } else { goto label_5519; } } else { goto label_5511; } } else { goto label_5511; } } else { goto label_5504; } } else { goto label_5504; } } else { goto label_5497; } } else { goto label_5497; } } 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_5739:; p21_new = node2____CPAchecker_TMP_0; label_5734:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5747:; p23_new = node2____CPAchecker_TMP_1; label_5742:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5755:; p24_new = node2____CPAchecker_TMP_2; label_5732:; mode2 = 1; goto label_5521; } else { label_5754:; node2____CPAchecker_TMP_2 = p24_new; goto label_5755; } } else { goto label_5754; } } else { goto label_5732; } } else { label_5746:; node2____CPAchecker_TMP_1 = p23_new; goto label_5747; } } else { goto label_5746; } } else { goto label_5742; } } else { label_5738:; node2____CPAchecker_TMP_0 = p21_new; goto label_5739; } } else { goto label_5738; } } else { goto label_5734; } } else { goto label_5732; } } } } else { nl1 = 1; goto label_5487; } } else { goto label_5487; } } else { goto label_5479; } } else { goto label_5479; } } else { goto label_5472; } } else { goto label_5472; } } else { goto label_5465; } } else { goto label_5465; } } 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_5770:; p12_new = node1____CPAchecker_TMP_0; label_5765:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5778:; p13_new = node1____CPAchecker_TMP_1; label_5773:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5786:; p14_new = node1____CPAchecker_TMP_2; label_5763:; mode1 = 1; goto label_5489; } else { label_5785:; node1____CPAchecker_TMP_2 = p14_new; goto label_5786; } } else { goto label_5785; } } else { goto label_5763; } } else { label_5777:; node1____CPAchecker_TMP_1 = p13_new; goto label_5778; } } else { goto label_5777; } } else { goto label_5773; } } else { label_5769:; node1____CPAchecker_TMP_0 = p12_new; goto label_5770; } } else { goto label_5769; } } else { goto label_5765; } } else { goto label_5763; } } } } else { __return_5459 = 0; return __return_5459; } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6462; } else { check__tmp = 0; goto label_6462; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6456; } else { check__tmp = 0; goto label_6447; } } } else { return __return_main; } } } else { return __return_main; } } else { 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_6389; } } else { goto label_6389; } } else { goto label_6382; } } else { goto label_6382; } } else { goto label_6375; } } else { goto label_6375; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6355; } } else { goto label_6355; } } else { goto label_6348; } } else { goto label_6348; } } else { goto label_6341; } } else { goto label_6341; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6321; } } else { goto label_6321; } } else { goto label_6314; } } else { goto label_6314; } } else { goto label_6307; } } else { goto label_6307; } } 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_5303:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5310:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5317:; 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_6010:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6017:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6024:; 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_6187:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6194:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6201:; 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_6290 = check__tmp; main__c1 = __return_6290; { _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_6247 = check__tmp; main__c1 = __return_6247; { _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_6201; } } else { goto label_6201; } } else { goto label_6194; } } else { goto label_6194; } } else { goto label_6187; } } else { goto label_6187; } } 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_6044:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6051:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6058:; 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_6170 = check__tmp; main__c1 = __return_6170; { _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_6125:; if (((int)r1) < 3) { check__tmp = 1; label_6131:; label_6116:; __return_6124 = check__tmp; main__c1 = __return_6124; __tmp_5446_0 = main____CPAchecker_TMP_0; goto label_5446; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6131; } else { check__tmp = 0; goto label_6131; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6125; } else { check__tmp = 0; goto label_6116; } } } else { return __return_main; } } } else { return __return_main; } } else { 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_6058; } } else { goto label_6058; } } else { goto label_6051; } } else { goto label_6051; } } else { goto label_6044; } } else { goto label_6044; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6024; } } else { goto label_6024; } } else { goto label_6017; } } else { goto label_6017; } } else { goto label_6010; } } else { goto label_6010; } } 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_5337:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5344:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5351:; 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_5867:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5874:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5881:; 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_5993 = check__tmp; main__c1 = __return_5993; { _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_5948:; if (((int)r1) < 3) { check__tmp = 1; label_5954:; label_5939:; __return_5947 = check__tmp; main__c1 = __return_5947; __tmp_5446_0 = main____CPAchecker_TMP_0; goto label_5446; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5954; } else { check__tmp = 0; goto label_5954; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5948; } else { check__tmp = 0; goto label_5939; } } } else { return __return_main; } } } else { return __return_main; } } else { 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_5881; } } else { goto label_5881; } } else { goto label_5874; } } else { goto label_5874; } } else { goto label_5867; } } else { goto label_5867; } } 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_5371:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5378:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5385:; 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_5848:; if (((int)r1) < 3) { check__tmp = 1; label_5854:; label_5839:; __return_5847 = check__tmp; main__c1 = __return_5847; __tmp_5446_0 = main____CPAchecker_TMP_0; goto label_5446; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5854; } else { check__tmp = 0; goto label_5854; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5848; } else { check__tmp = 0; goto label_5839; } } } else { return __return_main; } } } else { 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_5445 = check__tmp; main__c1 = __return_5445; __tmp_5446_0 = main____CPAchecker_TMP_0; goto label_5446; } } } else { return __return_main; } } else { 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_5385; } } else { goto label_5385; } } else { goto label_5378; } } else { goto label_5378; } } else { goto label_5371; } } else { goto label_5371; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5351; } } else { goto label_5351; } } else { goto label_5344; } } else { goto label_5344; } } else { goto label_5337; } } else { goto label_5337; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5317; } } else { goto label_5317; } } else { goto label_5310; } } else { goto label_5310; } } else { goto label_5303; } } else { goto label_5303; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5283; } } else { goto label_5283; } } else { goto label_5276; } } else { goto label_5276; } } else { goto label_5269; } } else { goto label_5269; } } else { return __return_main; } } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_5194:; node4____CPAchecker_TMP_2 = p43_new; goto label_5195; } } else { goto label_5194; } } else { goto label_5197; } } else { label_5186:; node4____CPAchecker_TMP_1 = p42_new; goto label_5187; } } else { goto label_5186; } } else { goto label_5182; } } else { label_5178:; node4____CPAchecker_TMP_0 = p41_new; goto label_5179; } } else { goto label_5178; } } else { goto label_5174; } } else { return __return_main; } } } } else { label_5162:; node3____CPAchecker_TMP_2 = p34_new; goto label_5163; } } else { goto label_5162; } } else { goto label_5165; } } else { label_5154:; node3____CPAchecker_TMP_1 = p32_new; goto label_5155; } } else { goto label_5154; } } else { goto label_5150; } } else { label_5146:; node3____CPAchecker_TMP_0 = p31_new; goto label_5147; } } else { goto label_5146; } } else { goto label_5142; } } else { return __return_main; } } } } else { label_5130:; node2____CPAchecker_TMP_2 = p24_new; goto label_5131; } } else { goto label_5130; } } else { goto label_5133; } } else { label_5122:; node2____CPAchecker_TMP_1 = p23_new; goto label_5123; } } else { goto label_5122; } } else { goto label_5118; } } else { label_5114:; node2____CPAchecker_TMP_0 = p21_new; goto label_5115; } } else { goto label_5114; } } else { goto label_5110; } } else { return __return_main; } } } } else { label_5098:; node1____CPAchecker_TMP_2 = p14_new; goto label_5099; } } else { goto label_5098; } } else { goto label_5101; } } else { label_5090:; node1____CPAchecker_TMP_1 = p13_new; goto label_5091; } } else { goto label_5090; } } else { goto label_5086; } } else { label_5082:; node1____CPAchecker_TMP_0 = p12_new; goto label_5083; } } else { goto label_5082; } } else { goto label_5078; } } else { return __return_main; } } } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4999; } } else { goto label_4999; } } else { goto label_4992; } } else { goto label_4992; } } else { goto label_4985; } } else { goto label_4985; } } else { return __return_main; } } } } else { goto label_4969; } } else { goto label_4969; } } else { goto label_4962; } } else { goto label_4962; } } else { goto label_4955; } } else { goto label_4955; } } else { return __return_main; } } } } else { goto label_4939; } } else { goto label_4939; } } else { goto label_4932; } } else { goto label_4932; } } else { goto label_4925; } } else { goto label_4925; } } else { return __return_main; } } } } else { goto label_4909; } } else { goto label_4909; } } else { goto label_4902; } } else { goto label_4902; } } else { goto label_4895; } } else { goto label_4895; } } else { return __return_main; } } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4820:; node4____CPAchecker_TMP_2 = p43_new; goto label_4821; } } else { goto label_4820; } } else { goto label_4823; } } else { label_4812:; node4____CPAchecker_TMP_1 = p42_new; goto label_4813; } } else { goto label_4812; } } else { goto label_4808; } } else { label_4804:; node4____CPAchecker_TMP_0 = p41_new; goto label_4805; } } else { goto label_4804; } } else { goto label_4800; } } else { return __return_main; } } } } else { label_4788:; node3____CPAchecker_TMP_2 = p34_new; goto label_4789; } } else { goto label_4788; } } else { goto label_4791; } } else { label_4780:; node3____CPAchecker_TMP_1 = p32_new; goto label_4781; } } else { goto label_4780; } } else { goto label_4776; } } else { label_4772:; node3____CPAchecker_TMP_0 = p31_new; goto label_4773; } } else { goto label_4772; } } else { goto label_4768; } } else { return __return_main; } } } } else { label_4756:; node2____CPAchecker_TMP_2 = p24_new; goto label_4757; } } else { goto label_4756; } } else { goto label_4759; } } else { label_4748:; node2____CPAchecker_TMP_1 = p23_new; goto label_4749; } } else { goto label_4748; } } else { goto label_4744; } } else { label_4740:; node2____CPAchecker_TMP_0 = p21_new; goto label_4741; } } else { goto label_4740; } } else { goto label_4736; } } else { return __return_main; } } } } else { label_4724:; node1____CPAchecker_TMP_2 = p14_new; goto label_4725; } } else { goto label_4724; } } else { goto label_4727; } } else { label_4716:; node1____CPAchecker_TMP_1 = p13_new; goto label_4717; } } else { goto label_4716; } } else { goto label_4712; } } else { label_4708:; node1____CPAchecker_TMP_0 = p12_new; goto label_4709; } } else { goto label_4708; } } else { goto label_4704; } } else { return __return_main; } } } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4625; } } else { goto label_4625; } } else { goto label_4618; } } else { goto label_4618; } } else { goto label_4611; } } else { goto label_4611; } } else { return __return_main; } } } } else { goto label_4595; } } else { goto label_4595; } } else { goto label_4588; } } else { goto label_4588; } } else { goto label_4581; } } else { goto label_4581; } } else { return __return_main; } } } } else { goto label_4565; } } else { goto label_4565; } } else { goto label_4558; } } else { goto label_4558; } } else { goto label_4551; } } else { goto label_4551; } } else { return __return_main; } } } } else { goto label_4535; } } else { goto label_4535; } } else { goto label_4528; } } else { goto label_4528; } } else { goto label_4521; } } else { goto label_4521; } } else { return __return_main; } } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4446:; node4____CPAchecker_TMP_2 = p43_new; goto label_4447; } } else { goto label_4446; } } else { goto label_4449; } } else { label_4438:; node4____CPAchecker_TMP_1 = p42_new; goto label_4439; } } else { goto label_4438; } } else { goto label_4434; } } else { label_4430:; node4____CPAchecker_TMP_0 = p41_new; goto label_4431; } } else { goto label_4430; } } else { goto label_4426; } } else { return __return_main; } } } } else { label_4414:; node3____CPAchecker_TMP_2 = p34_new; goto label_4415; } } else { goto label_4414; } } else { goto label_4417; } } else { label_4406:; node3____CPAchecker_TMP_1 = p32_new; goto label_4407; } } else { goto label_4406; } } else { goto label_4402; } } else { label_4398:; node3____CPAchecker_TMP_0 = p31_new; goto label_4399; } } else { goto label_4398; } } else { goto label_4394; } } else { return __return_main; } } } } else { label_4382:; node2____CPAchecker_TMP_2 = p24_new; goto label_4383; } } else { goto label_4382; } } else { goto label_4385; } } else { label_4374:; node2____CPAchecker_TMP_1 = p23_new; goto label_4375; } } else { goto label_4374; } } else { goto label_4370; } } else { label_4366:; node2____CPAchecker_TMP_0 = p21_new; goto label_4367; } } else { goto label_4366; } } else { goto label_4362; } } else { return __return_main; } } } } else { label_4350:; node1____CPAchecker_TMP_2 = p14_new; goto label_4351; } } else { goto label_4350; } } else { goto label_4353; } } else { label_4342:; node1____CPAchecker_TMP_1 = p13_new; goto label_4343; } } else { goto label_4342; } } else { goto label_4338; } } else { label_4334:; node1____CPAchecker_TMP_0 = p12_new; goto label_4335; } } else { goto label_4334; } } else { goto label_4330; } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { 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_4208; } else { label_6920:; if (!(init__r422 == 0)) { if (!(ep23 == 0)) { init__tmp___22 = 1; label_6926:; goto label_4208; } else { init__tmp___22 = 0; goto label_6926; } } else { init__tmp___22 = 0; goto label_4208; } } } else { goto label_6920; } } } else { if (!(init__r412 == 0)) { if (!(ep12 == 0)) { init__tmp___21 = 1; goto label_4203; } else { label_6935:; if (!(init__r432 == 0)) { if (!(ep32 == 0)) { init__tmp___21 = 1; label_6941:; goto label_4203; } else { init__tmp___21 = 0; goto label_6941; } } else { init__tmp___21 = 0; goto label_4203; } } } else { goto label_6935; } } } else { if (!(init__r422 == 0)) { if (!(ep21 == 0)) { init__tmp___20 = 1; goto label_4198; } else { label_6950:; if (!(init__r432 == 0)) { if (!(ep31 == 0)) { init__tmp___20 = 1; label_6956:; goto label_4198; } else { init__tmp___20 = 0; goto label_6956; } } else { init__tmp___20 = 0; goto label_4198; } } } else { goto label_6950; } } } else { if (!(init__r312 == 0)) { if (!(ep14 == 0)) { init__tmp___19 = 1; goto label_4193; } else { label_6965:; if (!(init__r322 == 0)) { if (!(ep24 == 0)) { init__tmp___19 = 1; label_6971:; goto label_4193; } else { init__tmp___19 = 0; goto label_6971; } } else { init__tmp___19 = 0; goto label_4193; } } } else { goto label_6965; } } } else { if (!(init__r312 == 0)) { if (!(ep12 == 0)) { init__tmp___18 = 1; goto label_4188; } else { label_6980:; if (!(init__r342 == 0)) { if (!(ep42 == 0)) { init__tmp___18 = 1; label_6986:; goto label_4188; } else { init__tmp___18 = 0; goto label_6986; } } else { init__tmp___18 = 0; goto label_4188; } } } else { goto label_6980; } } } else { if (!(init__r322 == 0)) { if (!(ep21 == 0)) { init__tmp___17 = 1; goto label_4183; } else { label_6995:; if (!(init__r342 == 0)) { if (!(ep41 == 0)) { init__tmp___17 = 1; label_7001:; goto label_4183; } else { init__tmp___17 = 0; goto label_7001; } } else { init__tmp___17 = 0; goto label_4183; } } } else { goto label_6995; } } } else { if (!(init__r212 == 0)) { if (!(ep14 == 0)) { init__tmp___16 = 1; goto label_4178; } else { label_7010:; if (!(init__r232 == 0)) { if (!(ep34 == 0)) { init__tmp___16 = 1; label_7016:; goto label_4178; } else { init__tmp___16 = 0; goto label_7016; } } else { init__tmp___16 = 0; goto label_4178; } } } else { goto label_7010; } } } else { if (!(init__r212 == 0)) { if (!(ep13 == 0)) { init__tmp___15 = 1; goto label_4173; } else { label_7025:; if (!(init__r242 == 0)) { if (!(ep43 == 0)) { init__tmp___15 = 1; label_7031:; goto label_4173; } else { init__tmp___15 = 0; goto label_7031; } } else { init__tmp___15 = 0; goto label_4173; } } } else { goto label_7025; } } } else { if (!(init__r232 == 0)) { if (!(ep31 == 0)) { init__tmp___14 = 1; goto label_4168; } else { label_7040:; if (!(init__r242 == 0)) { if (!(ep41 == 0)) { init__tmp___14 = 1; label_7046:; goto label_4168; } else { init__tmp___14 = 0; goto label_7046; } } else { init__tmp___14 = 0; goto label_4168; } } } else { goto label_7040; } } } else { if (!(init__r122 == 0)) { if (!(ep24 == 0)) { init__tmp___13 = 1; goto label_4163; } else { label_7055:; if (!(init__r132 == 0)) { if (!(ep34 == 0)) { init__tmp___13 = 1; label_7061:; goto label_4163; } else { init__tmp___13 = 0; goto label_7061; } } else { init__tmp___13 = 0; goto label_4163; } } } else { goto label_7055; } } } else { if (!(init__r122 == 0)) { if (!(ep23 == 0)) { init__tmp___12 = 1; goto label_4158; } else { label_7070:; if (!(init__r142 == 0)) { if (!(ep43 == 0)) { init__tmp___12 = 1; label_7076:; goto label_4158; } else { init__tmp___12 = 0; goto label_7076; } } else { init__tmp___12 = 0; goto label_4158; } } } else { goto label_7070; } } } else { if (!(init__r132 == 0)) { if (!(ep32 == 0)) { init__tmp___11 = 1; goto label_4153; } else { label_7085:; if (!(init__r142 == 0)) { if (!(ep42 == 0)) { init__tmp___11 = 1; label_7091:; goto label_4153; } else { init__tmp___11 = 0; goto label_7091; } } else { init__tmp___11 = 0; goto label_4153; } } } else { goto label_7085; } } } else { if (!(init__r411 == 0)) { if (!(ep13 == 0)) { init__tmp___10 = 1; goto label_4148; } else { label_7100:; if (!(init__r421 == 0)) { if (!(ep23 == 0)) { init__tmp___10 = 1; label_7106:; goto label_4148; } else { init__tmp___10 = 0; goto label_7106; } } else { init__tmp___10 = 0; goto label_4148; } } } else { goto label_7100; } } } else { if (!(init__r411 == 0)) { if (!(ep12 == 0)) { init__tmp___9 = 1; goto label_4143; } else { label_7115:; if (!(init__r431 == 0)) { if (!(ep32 == 0)) { init__tmp___9 = 1; label_7121:; goto label_4143; } else { init__tmp___9 = 0; goto label_7121; } } else { init__tmp___9 = 0; goto label_4143; } } } else { goto label_7115; } } } else { if (!(init__r421 == 0)) { if (!(ep21 == 0)) { init__tmp___8 = 1; goto label_4138; } else { label_7130:; if (!(init__r431 == 0)) { if (!(ep31 == 0)) { init__tmp___8 = 1; label_7136:; goto label_4138; } else { init__tmp___8 = 0; goto label_7136; } } else { init__tmp___8 = 0; goto label_4138; } } } else { goto label_7130; } } } else { if (!(init__r311 == 0)) { if (!(ep14 == 0)) { init__tmp___7 = 1; goto label_4133; } else { label_7145:; if (!(init__r321 == 0)) { if (!(ep24 == 0)) { init__tmp___7 = 1; label_7151:; goto label_4133; } else { init__tmp___7 = 0; goto label_7151; } } else { init__tmp___7 = 0; goto label_4133; } } } else { goto label_7145; } } } else { if (!(init__r311 == 0)) { if (!(ep12 == 0)) { init__tmp___6 = 1; goto label_4128; } else { label_7160:; if (!(init__r341 == 0)) { if (!(ep42 == 0)) { init__tmp___6 = 1; label_7166:; goto label_4128; } else { init__tmp___6 = 0; goto label_7166; } } else { init__tmp___6 = 0; goto label_4128; } } } else { goto label_7160; } } } else { if (!(init__r321 == 0)) { if (!(ep21 == 0)) { init__tmp___5 = 1; goto label_4123; } else { label_7175:; if (!(init__r341 == 0)) { if (!(ep41 == 0)) { init__tmp___5 = 1; label_7181:; goto label_4123; } else { init__tmp___5 = 0; goto label_7181; } } else { init__tmp___5 = 0; goto label_4123; } } } else { goto label_7175; } } } else { if (!(init__r211 == 0)) { if (!(ep14 == 0)) { init__tmp___4 = 1; goto label_4118; } else { label_7190:; if (!(init__r231 == 0)) { if (!(ep34 == 0)) { init__tmp___4 = 1; label_7196:; goto label_4118; } else { init__tmp___4 = 0; goto label_7196; } } else { init__tmp___4 = 0; goto label_4118; } } } else { goto label_7190; } } } else { if (!(init__r211 == 0)) { if (!(ep13 == 0)) { init__tmp___3 = 1; goto label_4113; } else { label_7205:; if (!(init__r241 == 0)) { if (!(ep43 == 0)) { init__tmp___3 = 1; label_7211:; goto label_4113; } else { init__tmp___3 = 0; goto label_7211; } } else { init__tmp___3 = 0; goto label_4113; } } } else { goto label_7205; } } } else { if (!(init__r231 == 0)) { if (!(ep31 == 0)) { init__tmp___2 = 1; goto label_4108; } else { label_7220:; if (!(init__r241 == 0)) { if (!(ep41 == 0)) { init__tmp___2 = 1; label_7226:; goto label_4108; } else { init__tmp___2 = 0; goto label_7226; } } else { init__tmp___2 = 0; goto label_4108; } } } else { goto label_7220; } } } else { if (!(init__r121 == 0)) { if (!(ep24 == 0)) { init__tmp___1 = 1; goto label_4103; } else { label_7235:; if (!(init__r131 == 0)) { if (!(ep34 == 0)) { init__tmp___1 = 1; label_7241:; goto label_4103; } else { init__tmp___1 = 0; goto label_7241; } } else { init__tmp___1 = 0; goto label_4103; } } } else { goto label_7235; } } } else { if (!(init__r121 == 0)) { if (!(ep23 == 0)) { init__tmp___0 = 1; goto label_4098; } else { label_7250:; if (!(init__r141 == 0)) { if (!(ep43 == 0)) { init__tmp___0 = 1; label_7256:; goto label_4098; } else { init__tmp___0 = 0; goto label_7256; } } else { init__tmp___0 = 0; goto label_4098; } } } else { goto label_7250; } } } else { if (!(init__r131 == 0)) { if (!(ep32 == 0)) { init__tmp = 1; goto label_4093; } else { label_7265:; if (!(init__r141 == 0)) { if (!(ep42 == 0)) { init__tmp = 1; label_7271:; goto label_4093; } else { init__tmp = 0; goto label_7271; } } else { init__tmp = 0; goto label_4093; } } } else { goto label_7265; } } } }