// 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.UNBOUNDED.pals.c.v+lhb-reducer.c", 4, "reach_error"); } char __VERIFIER_nondet_char(); unsigned char __VERIFIER_nondet_uchar(); _Bool __VERIFIER_nondet_bool(); void assert(_Bool arg); void abort(void); void assume_abort_if_not(int cond) { if(!cond) {abort();} } typedef char msg_t; typedef int port_t; void read(port_t p, msg_t m); void write(port_t p, msg_t m); msg_t nomsg = (msg_t )-1; port_t p12 = 0; char p12_old = '\x0'; char p12_new = '\x0'; _Bool ep12 = 0; port_t p13 = 0; char p13_old = '\x0'; char p13_new = '\x0'; _Bool ep13 = 0; port_t p14 = 0; char p14_old = '\x0'; char p14_new = '\x0'; _Bool ep14 = 0; port_t p21 = 0; char p21_old = '\x0'; char p21_new = '\x0'; _Bool ep21 = 0; port_t p23 = 0; char p23_old = '\x0'; char p23_new = '\x0'; _Bool ep23 = 0; port_t p24 = 0; char p24_old = '\x0'; char p24_new = '\x0'; _Bool ep24 = 0; port_t p31 = 0; char p31_old = '\x0'; char p31_new = '\x0'; _Bool ep31 = 0; port_t p32 = 0; char p32_old = '\x0'; char p32_new = '\x0'; _Bool ep32 = 0; port_t p34 = 0; char p34_old = '\x0'; char p34_new = '\x0'; _Bool ep34 = 0; port_t p41 = 0; char p41_old = '\x0'; char p41_new = '\x0'; _Bool ep41 = 0; port_t p42 = 0; char p42_old = '\x0'; char p42_new = '\x0'; _Bool ep42 = 0; port_t p43 = 0; char p43_old = '\x0'; char p43_new = '\x0'; _Bool ep43 = 0; char id1 = '\x0'; unsigned char r1 = '\x0'; char st1 = '\x0'; char nl1 = '\x0'; char m1 = '\x0'; char max1 = '\x0'; _Bool mode1 = 0; char id2 = '\x0'; unsigned char r2 = '\x0'; char st2 = '\x0'; char nl2 = '\x0'; char m2 = '\x0'; char max2 = '\x0'; _Bool mode2 = 0; char id3 = '\x0'; unsigned char r3 = '\x0'; char st3 = '\x0'; char nl3 = '\x0'; char m3 = '\x0'; char max3 = '\x0'; _Bool mode3 = 0; char id4 = '\x0'; unsigned char r4 = '\x0'; char st4 = '\x0'; char nl4 = '\x0'; char m4 = '\x0'; char max4 = '\x0'; _Bool mode4 = 0; void node1(); void node2(); void node3(); void node4(); void (*nodes[4])() = { &node1, &node2, &node3, &node4 }; int init(); int check(); int main(); int __return_4316; int __return_4526; int __return_4710; int __return_4898; int __return_5082; int __return_5270; int __return_6931; int __return_6888; int __return_6810; int __return_6767; int __return_6654; int __return_6611; int __return_6533; int __return_6487; int __return_5640; int __return_6319; int __return_6276; int __return_6198; int __return_6152; int __return_6019; int __return_5973; int __return_5872; int __return_5463; int main() { int main__c1; int main__i2; main__c1 = 0; ep12 = __VERIFIER_nondet_bool(); ep13 = __VERIFIER_nondet_bool(); ep14 = __VERIFIER_nondet_bool(); ep21 = __VERIFIER_nondet_bool(); ep23 = __VERIFIER_nondet_bool(); ep24 = __VERIFIER_nondet_bool(); ep31 = __VERIFIER_nondet_bool(); ep32 = __VERIFIER_nondet_bool(); ep34 = __VERIFIER_nondet_bool(); ep41 = __VERIFIER_nondet_bool(); ep42 = __VERIFIER_nondet_bool(); ep43 = __VERIFIER_nondet_bool(); id1 = __VERIFIER_nondet_char(); r1 = __VERIFIER_nondet_uchar(); st1 = __VERIFIER_nondet_char(); nl1 = __VERIFIER_nondet_char(); m1 = __VERIFIER_nondet_char(); max1 = __VERIFIER_nondet_char(); mode1 = __VERIFIER_nondet_bool(); id2 = __VERIFIER_nondet_char(); r2 = __VERIFIER_nondet_uchar(); st2 = __VERIFIER_nondet_char(); nl2 = __VERIFIER_nondet_char(); m2 = __VERIFIER_nondet_char(); max2 = __VERIFIER_nondet_char(); mode2 = __VERIFIER_nondet_bool(); id3 = __VERIFIER_nondet_char(); r3 = __VERIFIER_nondet_uchar(); st3 = __VERIFIER_nondet_char(); nl3 = __VERIFIER_nondet_char(); m3 = __VERIFIER_nondet_char(); max3 = __VERIFIER_nondet_char(); mode3 = __VERIFIER_nondet_bool(); id4 = __VERIFIER_nondet_char(); r4 = __VERIFIER_nondet_uchar(); st4 = __VERIFIER_nondet_char(); nl4 = __VERIFIER_nondet_char(); m4 = __VERIFIER_nondet_char(); max4 = __VERIFIER_nondet_char(); mode4 = __VERIFIER_nondet_bool(); { _Bool init__r121; _Bool init__r131; _Bool init__r141; _Bool init__r211; _Bool init__r231; _Bool init__r241; _Bool init__r311; _Bool init__r321; _Bool init__r341; _Bool init__r411; _Bool init__r421; _Bool init__r431; _Bool init__r122; int init__tmp; _Bool init__r132; int init__tmp___0; _Bool init__r142; int init__tmp___1; _Bool init__r212; int init__tmp___2; _Bool init__r232; int init__tmp___3; _Bool init__r242; int init__tmp___4; _Bool init__r312; int init__tmp___5; _Bool init__r322; int init__tmp___6; _Bool init__r342; int init__tmp___7; _Bool init__r412; int init__tmp___8; _Bool init__r422; int init__tmp___9; _Bool init__r432; int init__tmp___10; _Bool init__r123; int init__tmp___11; _Bool init__r133; int init__tmp___12; _Bool init__r143; int init__tmp___13; _Bool init__r213; int init__tmp___14; _Bool init__r233; int init__tmp___15; _Bool init__r243; int init__tmp___16; _Bool init__r313; int init__tmp___17; _Bool init__r323; int init__tmp___18; _Bool init__r343; int init__tmp___19; _Bool init__r413; int init__tmp___20; _Bool init__r423; int init__tmp___21; _Bool init__r433; int init__tmp___22; int init__tmp___23; init__r121 = ep12; init__r131 = ep13; init__r141 = ep14; init__r211 = ep21; init__r231 = ep23; init__r241 = ep24; init__r311 = ep31; init__r321 = ep32; init__r341 = ep34; init__r411 = ep41; init__r421 = ep42; init__r431 = ep43; if (!(init__r121 == 0)) { init__tmp = 1; label_4114:; init__r122 = (_Bool)init__tmp; if (!(init__r131 == 0)) { init__tmp___0 = 1; label_4119:; init__r132 = (_Bool)init__tmp___0; if (!(init__r141 == 0)) { init__tmp___1 = 1; label_4124:; init__r142 = (_Bool)init__tmp___1; if (!(init__r211 == 0)) { init__tmp___2 = 1; label_4129:; init__r212 = (_Bool)init__tmp___2; if (!(init__r231 == 0)) { init__tmp___3 = 1; label_4134:; init__r232 = (_Bool)init__tmp___3; if (!(init__r241 == 0)) { init__tmp___4 = 1; label_4139:; init__r242 = (_Bool)init__tmp___4; if (!(init__r311 == 0)) { init__tmp___5 = 1; label_4144:; init__r312 = (_Bool)init__tmp___5; if (!(init__r321 == 0)) { init__tmp___6 = 1; label_4149:; init__r322 = (_Bool)init__tmp___6; if (!(init__r341 == 0)) { init__tmp___7 = 1; label_4154:; init__r342 = (_Bool)init__tmp___7; if (!(init__r411 == 0)) { init__tmp___8 = 1; label_4159:; init__r412 = (_Bool)init__tmp___8; if (!(init__r421 == 0)) { init__tmp___9 = 1; label_4164:; init__r422 = (_Bool)init__tmp___9; if (!(init__r431 == 0)) { init__tmp___10 = 1; label_4169:; init__r432 = (_Bool)init__tmp___10; if (!(init__r122 == 0)) { init__tmp___11 = 1; label_4174:; init__r123 = (_Bool)init__tmp___11; if (!(init__r132 == 0)) { init__tmp___12 = 1; label_4179:; init__r133 = (_Bool)init__tmp___12; if (!(init__r142 == 0)) { init__tmp___13 = 1; label_4184:; init__r143 = (_Bool)init__tmp___13; if (!(init__r212 == 0)) { init__tmp___14 = 1; label_4189:; init__r213 = (_Bool)init__tmp___14; if (!(init__r232 == 0)) { init__tmp___15 = 1; label_4194:; init__r233 = (_Bool)init__tmp___15; if (!(init__r242 == 0)) { init__tmp___16 = 1; label_4199:; init__r243 = (_Bool)init__tmp___16; if (!(init__r312 == 0)) { init__tmp___17 = 1; label_4204:; init__r313 = (_Bool)init__tmp___17; if (!(init__r322 == 0)) { init__tmp___18 = 1; label_4209:; init__r323 = (_Bool)init__tmp___18; if (!(init__r342 == 0)) { init__tmp___19 = 1; label_4214:; init__r343 = (_Bool)init__tmp___19; if (!(init__r412 == 0)) { init__tmp___20 = 1; label_4219:; init__r413 = (_Bool)init__tmp___20; if (!(init__r422 == 0)) { init__tmp___21 = 1; label_4224:; init__r423 = (_Bool)init__tmp___21; if (!(init__r432 == 0)) { init__tmp___22 = 1; label_4229:; 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_4316 = init__tmp___23; main__i2 = __return_4316; if (main__i2 != 0) { p12_old = nomsg; p12_new = nomsg; p13_old = nomsg; p13_new = nomsg; p14_old = nomsg; p14_new = nomsg; p21_old = nomsg; p21_new = nomsg; p23_old = nomsg; p23_new = nomsg; p24_old = nomsg; p24_new = nomsg; p31_old = nomsg; p31_new = nomsg; p32_old = nomsg; p32_new = nomsg; p34_old = nomsg; p34_new = nomsg; p41_old = nomsg; p41_new = nomsg; p42_old = nomsg; p42_new = nomsg; p43_old = nomsg; p43_new = nomsg; main__i2 = 0; { if (!(mode1 == 0)) { return __return_main; } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_4356:; p12_new = node1____CPAchecker_TMP_0; label_4351:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4364:; p13_new = node1____CPAchecker_TMP_1; label_4359:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4372:; p14_new = node1____CPAchecker_TMP_2; label_4374:; 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_4388:; p21_new = node2____CPAchecker_TMP_0; label_4383:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4396:; p23_new = node2____CPAchecker_TMP_1; label_4391:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4404:; p24_new = node2____CPAchecker_TMP_2; label_4406:; 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_4420:; p31_new = node3____CPAchecker_TMP_0; label_4415:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4428:; p32_new = node3____CPAchecker_TMP_1; label_4423:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4436:; p34_new = node3____CPAchecker_TMP_2; label_4438:; 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_4452:; p41_new = node4____CPAchecker_TMP_0; label_4447:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4460:; p42_new = node4____CPAchecker_TMP_1; label_4455:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4468:; p43_new = node4____CPAchecker_TMP_2; label_4470:; 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_4526 = check__tmp; main__c1 = __return_4526; { _Bool __tmp_1; __tmp_1 = main__c1; _Bool assert__arg; assert__arg = __tmp_1; if (assert__arg == 0) { return __return_main; } else { { if (!(mode1 == 0)) { if (r1 == 255) { return __return_main; } else { r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4540:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4547:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4554:; if (((int)r1) == 3) { return __return_main; } else { mode1 = 0; { if (!(mode2 == 0)) { if (r2 == 255) { return __return_main; } else { r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4571:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4578:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4585:; if (((int)r2) == 3) { return __return_main; } else { mode2 = 0; { if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4602:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4609:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4616:; if (((int)r3) == 3) { return __return_main; } else { mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4633:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4640:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4647:; 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_4710 = check__tmp; main__c1 = __return_4710; { _Bool __tmp_2; __tmp_2 = main__c1; _Bool assert__arg; assert__arg = __tmp_2; if (assert__arg == 0) { return __return_main; } else { { if (!(mode1 == 0)) { return __return_main; } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_4728:; p12_new = node1____CPAchecker_TMP_0; label_4723:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4736:; p13_new = node1____CPAchecker_TMP_1; label_4731:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4744:; p14_new = node1____CPAchecker_TMP_2; label_4746:; 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_4760:; p21_new = node2____CPAchecker_TMP_0; label_4755:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4768:; p23_new = node2____CPAchecker_TMP_1; label_4763:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4776:; p24_new = node2____CPAchecker_TMP_2; label_4778:; 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_4792:; p31_new = node3____CPAchecker_TMP_0; label_4787:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4800:; p32_new = node3____CPAchecker_TMP_1; label_4795:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4808:; p34_new = node3____CPAchecker_TMP_2; label_4810:; 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_4824:; p41_new = node4____CPAchecker_TMP_0; label_4819:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4832:; p42_new = node4____CPAchecker_TMP_1; label_4827:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4840:; p43_new = node4____CPAchecker_TMP_2; label_4842:; 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_4898 = check__tmp; main__c1 = __return_4898; { _Bool __tmp_3; __tmp_3 = main__c1; _Bool assert__arg; assert__arg = __tmp_3; if (assert__arg == 0) { return __return_main; } else { { if (!(mode1 == 0)) { if (r1 == 255) { return __return_main; } else { r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4912:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4919:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4926:; if (((int)r1) == 3) { return __return_main; } else { mode1 = 0; { if (!(mode2 == 0)) { if (r2 == 255) { return __return_main; } else { r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4943:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4950:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4957:; if (((int)r2) == 3) { return __return_main; } else { mode2 = 0; { if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4974:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4981:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4988:; if (((int)r3) == 3) { return __return_main; } else { mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5005:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5012:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5019:; 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_5082 = check__tmp; main__c1 = __return_5082; { _Bool __tmp_4; __tmp_4 = main__c1; _Bool assert__arg; assert__arg = __tmp_4; if (assert__arg == 0) { return __return_main; } else { { if (!(mode1 == 0)) { return __return_main; } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_5100:; p12_new = node1____CPAchecker_TMP_0; label_5095:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5108:; p13_new = node1____CPAchecker_TMP_1; label_5103:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5116:; p14_new = node1____CPAchecker_TMP_2; label_5118:; 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_5132:; p21_new = node2____CPAchecker_TMP_0; label_5127:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5140:; p23_new = node2____CPAchecker_TMP_1; label_5135:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5148:; p24_new = node2____CPAchecker_TMP_2; label_5150:; mode2 = 1; { 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_5164:; p31_new = node3____CPAchecker_TMP_0; label_5159:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5172:; p32_new = node3____CPAchecker_TMP_1; label_5167:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5180:; p34_new = node3____CPAchecker_TMP_2; label_5182:; 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_5196:; p41_new = node4____CPAchecker_TMP_0; label_5191:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5204:; p42_new = node4____CPAchecker_TMP_1; label_5199:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5212:; p43_new = node4____CPAchecker_TMP_2; label_5214:; 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_5270 = check__tmp; main__c1 = __return_5270; { _Bool __tmp_5; __tmp_5 = main__c1; _Bool assert__arg; assert__arg = __tmp_5; if (assert__arg == 0) { return __return_main; } else { { if (!(mode1 == 0)) { if (r1 == 255) { return __return_main; } else { r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5284:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5291:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5298:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; mode1 = 0; { if (!(mode2 == 0)) { if (r2 == 255) { return __return_main; } else { r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_6337:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_6344:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_6351:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; mode2 = 0; { if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6672:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6679:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6686:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6828:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6835:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6842:; 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_6931 = check__tmp; main__c1 = __return_6931; { _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_6888 = check__tmp; main__c1 = __return_6888; { _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_6842; } } else { goto label_6842; } } else { goto label_6835; } } else { goto label_6835; } } else { goto label_6828; } } else { goto label_6828; } } } else { return __return_main; } } } else { nl3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6707:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6714:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6721:; 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_6810 = check__tmp; main__c1 = __return_6810; { _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_6767 = check__tmp; main__c1 = __return_6767; { _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_6721; } } else { goto label_6721; } } else { goto label_6714; } } else { goto label_6714; } } else { goto label_6707; } } else { goto label_6707; } } } 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 { nl2 = 1; mode2 = 0; { if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6372:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6379:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6386:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6551:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6558:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6565:; 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_6654 = check__tmp; main__c1 = __return_6654; { _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_6611 = check__tmp; main__c1 = __return_6611; { _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_6565; } } else { goto label_6565; } } else { goto label_6558; } } else { goto label_6558; } } else { goto label_6551; } } else { goto label_6551; } } } else { return __return_main; } } } else { nl3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6407:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6414:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6421:; 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_6533 = check__tmp; main__c1 = __return_6533; { _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_6488:; if (((int)r1) < 3) { check__tmp = 1; label_6494:; label_6479:; __return_6487 = check__tmp; main__c1 = __return_6487; label_5464:; { _Bool __tmp_13; __tmp_13 = main__c1; _Bool assert__arg; assert__arg = __tmp_13; if (assert__arg == 0) { {reach_error();} return __return_main; } else { { if (!(mode1 == 0)) { if (r1 == 255) { r1 = 3; label_5478:; r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5480:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5487:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5494:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5502:; mode1 = 0; label_5504:; { if (!(mode2 == 0)) { if (r2 == 255) { r2 = 3; label_5512:; r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5514:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5521:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5528:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5536:; mode2 = 0; label_5538:; { if (!(mode3 == 0)) { if (r3 == 255) { r3 = 3; label_5546:; r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5548:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5555:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5562:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5570:; mode3 = 0; label_5572:; { if (!(mode4 == 0)) { if (r4 == 255) { r4 = 3; label_5580:; r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5582:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5589:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5596:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5604:; mode4 = 0; label_5606:; 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_5663:; if (((int)r1) < 3) { label_5670:; if (((int)r1) >= 3) { label_5677:; if (((int)r1) < 3) { check__tmp = 1; label_5683:; label_5676:; label_5669:; label_5662:; label_5656:; label_5652:; label_5648:; label_5644:; label_5639:; __return_5640 = check__tmp; main__c1 = __return_5640; goto label_5464; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5683; } else { check__tmp = 0; goto label_5683; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5677; } else { check__tmp = 0; goto label_5676; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_5670; } else { check__tmp = 0; goto label_5669; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_5663; } else { check__tmp = 0; goto label_5662; } } } else { check__tmp = 0; goto label_5656; } } else { check__tmp = 0; goto label_5652; } } else { check__tmp = 0; goto label_5648; } } else { check__tmp = 0; goto label_5644; } } else { check__tmp = 0; goto label_5639; } } } else { nl4 = 1; goto label_5604; } } else { goto label_5604; } } else { goto label_5596; } } else { goto label_5596; } } else { goto label_5589; } } else { goto label_5589; } } else { goto label_5582; } } else { goto label_5582; } } else { goto label_5580; } } 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_5699:; p41_new = node4____CPAchecker_TMP_0; label_5694:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5707:; p42_new = node4____CPAchecker_TMP_1; label_5702:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5715:; p43_new = node4____CPAchecker_TMP_2; label_5692:; mode4 = 1; goto label_5606; } else { label_5714:; node4____CPAchecker_TMP_2 = p43_new; goto label_5715; } } else { goto label_5714; } } else { goto label_5692; } } else { label_5706:; node4____CPAchecker_TMP_1 = p42_new; goto label_5707; } } else { goto label_5706; } } else { goto label_5702; } } else { label_5698:; node4____CPAchecker_TMP_0 = p41_new; goto label_5699; } } else { goto label_5698; } } else { goto label_5694; } } else { goto label_5692; } } } } else { nl3 = 1; goto label_5570; } } else { goto label_5570; } } else { goto label_5562; } } else { goto label_5562; } } else { goto label_5555; } } else { goto label_5555; } } else { goto label_5548; } } else { goto label_5548; } } else { goto label_5546; } } 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_5731:; p31_new = node3____CPAchecker_TMP_0; label_5726:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5739:; p32_new = node3____CPAchecker_TMP_1; label_5734:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5747:; p34_new = node3____CPAchecker_TMP_2; label_5724:; mode3 = 1; goto label_5572; } else { label_5746:; node3____CPAchecker_TMP_2 = p34_new; goto label_5747; } } else { goto label_5746; } } else { goto label_5724; } } else { label_5738:; node3____CPAchecker_TMP_1 = p32_new; goto label_5739; } } else { goto label_5738; } } else { goto label_5734; } } else { label_5730:; node3____CPAchecker_TMP_0 = p31_new; goto label_5731; } } else { goto label_5730; } } else { goto label_5726; } } else { goto label_5724; } } } } else { nl2 = 1; goto label_5536; } } else { goto label_5536; } } else { goto label_5528; } } else { goto label_5528; } } else { goto label_5521; } } else { goto label_5521; } } else { goto label_5514; } } else { goto label_5514; } } else { goto label_5512; } } 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_5763:; p21_new = node2____CPAchecker_TMP_0; label_5758:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5771:; p23_new = node2____CPAchecker_TMP_1; label_5766:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5779:; p24_new = node2____CPAchecker_TMP_2; label_5756:; mode2 = 1; goto label_5538; } else { label_5778:; node2____CPAchecker_TMP_2 = p24_new; goto label_5779; } } else { goto label_5778; } } else { goto label_5756; } } else { label_5770:; node2____CPAchecker_TMP_1 = p23_new; goto label_5771; } } else { goto label_5770; } } else { goto label_5766; } } else { label_5762:; node2____CPAchecker_TMP_0 = p21_new; goto label_5763; } } else { goto label_5762; } } else { goto label_5758; } } else { goto label_5756; } } } } else { nl1 = 1; goto label_5502; } } else { goto label_5502; } } else { goto label_5494; } } else { goto label_5494; } } else { goto label_5487; } } else { goto label_5487; } } else { goto label_5480; } } else { goto label_5480; } } else { goto label_5478; } } 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_5795:; p12_new = node1____CPAchecker_TMP_0; label_5790:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5803:; p13_new = node1____CPAchecker_TMP_1; label_5798:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5811:; p14_new = node1____CPAchecker_TMP_2; label_5788:; mode1 = 1; goto label_5504; } else { label_5810:; node1____CPAchecker_TMP_2 = p14_new; goto label_5811; } } else { goto label_5810; } } else { goto label_5788; } } else { label_5802:; node1____CPAchecker_TMP_1 = p13_new; goto label_5803; } } else { goto label_5802; } } else { goto label_5798; } } else { label_5794:; node1____CPAchecker_TMP_0 = p12_new; goto label_5795; } } else { goto label_5794; } } else { goto label_5790; } } else { goto label_5788; } } } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6494; } else { check__tmp = 0; goto label_6494; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6488; } else { check__tmp = 0; goto label_6479; } } } else { return __return_main; } } } else { return __return_main; } } else { 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_6421; } } else { goto label_6421; } } else { goto label_6414; } } else { goto label_6414; } } else { goto label_6407; } } else { goto label_6407; } } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6386; } } else { goto label_6386; } } else { goto label_6379; } } else { goto label_6379; } } else { goto label_6372; } } else { goto label_6372; } } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6351; } } else { goto label_6351; } } else { goto label_6344; } } else { goto label_6344; } } else { goto label_6337; } } else { goto label_6337; } } } else { return __return_main; } } } else { nl1 = 1; mode1 = 0; { if (!(mode2 == 0)) { if (r2 == 255) { return __return_main; } else { r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5319:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5326:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5333:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; mode2 = 0; { if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6037:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6044:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_6051:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6216:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6223:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6230:; 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_6319 = check__tmp; main__c1 = __return_6319; { _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_6276 = check__tmp; main__c1 = __return_6276; { _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_6230; } } else { goto label_6230; } } else { goto label_6223; } } else { goto label_6223; } } else { goto label_6216; } } else { goto label_6216; } } } else { return __return_main; } } } else { nl3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6072:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6079:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_6086:; 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_6198 = check__tmp; main__c1 = __return_6198; { _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_6153:; if (((int)r1) < 3) { check__tmp = 1; label_6159:; label_6144:; __return_6152 = check__tmp; main__c1 = __return_6152; goto label_5464; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6159; } else { check__tmp = 0; goto label_6159; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6153; } else { check__tmp = 0; goto label_6144; } } } else { return __return_main; } } } else { return __return_main; } } else { 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_6086; } } else { goto label_6086; } } else { goto label_6079; } } else { goto label_6079; } } else { goto label_6072; } } else { goto label_6072; } } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_6051; } } else { goto label_6051; } } else { goto label_6044; } } else { goto label_6044; } } else { goto label_6037; } } else { goto label_6037; } } } else { return __return_main; } } } else { nl2 = 1; mode2 = 0; { if (!(mode3 == 0)) { if (r3 == 255) { return __return_main; } else { r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5354:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5361:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5368:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5893:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5900:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5907:; 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_6019 = check__tmp; main__c1 = __return_6019; { _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_5974:; if (((int)r1) < 3) { check__tmp = 1; label_5980:; label_5965:; __return_5973 = check__tmp; main__c1 = __return_5973; goto label_5464; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5980; } else { check__tmp = 0; goto label_5980; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5974; } else { check__tmp = 0; goto label_5965; } } } else { return __return_main; } } } else { return __return_main; } } else { 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_5907; } } else { goto label_5907; } } else { goto label_5900; } } else { goto label_5900; } } else { goto label_5893; } } else { goto label_5893; } } } else { return __return_main; } } } else { nl3 = 1; mode3 = 0; { if (!(mode4 == 0)) { if (r4 == 255) { return __return_main; } else { r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5389:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5396:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5403:; 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_5873:; if (((int)r1) < 3) { check__tmp = 1; label_5879:; label_5864:; __return_5872 = check__tmp; main__c1 = __return_5872; goto label_5464; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5879; } else { check__tmp = 0; goto label_5879; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5873; } else { check__tmp = 0; goto label_5864; } } } else { return __return_main; } } } else { 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_5463 = check__tmp; main__c1 = __return_5463; goto label_5464; } } } else { return __return_main; } } else { 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_5403; } } else { goto label_5403; } } else { goto label_5396; } } else { goto label_5396; } } else { goto label_5389; } } else { goto label_5389; } } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5368; } } else { goto label_5368; } } else { goto label_5361; } } else { goto label_5361; } } else { goto label_5354; } } else { goto label_5354; } } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5333; } } else { goto label_5333; } } else { goto label_5326; } } else { goto label_5326; } } else { goto label_5319; } } else { goto label_5319; } } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_5298; } } else { goto label_5298; } } else { goto label_5291; } } else { goto label_5291; } } else { goto label_5284; } } else { goto label_5284; } } } else { return __return_main; } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_5211:; node4____CPAchecker_TMP_2 = p43_new; goto label_5212; } } else { goto label_5211; } } else { goto label_5214; } } else { label_5203:; node4____CPAchecker_TMP_1 = p42_new; goto label_5204; } } else { goto label_5203; } } else { goto label_5199; } } else { label_5195:; node4____CPAchecker_TMP_0 = p41_new; goto label_5196; } } else { goto label_5195; } } else { goto label_5191; } } else { return __return_main; } } } } else { label_5179:; node3____CPAchecker_TMP_2 = p34_new; goto label_5180; } } else { goto label_5179; } } else { goto label_5182; } } else { label_5171:; node3____CPAchecker_TMP_1 = p32_new; goto label_5172; } } else { goto label_5171; } } else { goto label_5167; } } else { label_5163:; node3____CPAchecker_TMP_0 = p31_new; goto label_5164; } } else { goto label_5163; } } else { goto label_5159; } } else { return __return_main; } } } } else { label_5147:; node2____CPAchecker_TMP_2 = p24_new; goto label_5148; } } else { goto label_5147; } } else { goto label_5150; } } else { label_5139:; node2____CPAchecker_TMP_1 = p23_new; goto label_5140; } } else { goto label_5139; } } else { goto label_5135; } } else { label_5131:; node2____CPAchecker_TMP_0 = p21_new; goto label_5132; } } else { goto label_5131; } } else { goto label_5127; } } else { return __return_main; } } } } else { label_5115:; node1____CPAchecker_TMP_2 = p14_new; goto label_5116; } } else { goto label_5115; } } else { goto label_5118; } } else { label_5107:; node1____CPAchecker_TMP_1 = p13_new; goto label_5108; } } else { goto label_5107; } } else { goto label_5103; } } else { label_5099:; node1____CPAchecker_TMP_0 = p12_new; goto label_5100; } } else { goto label_5099; } } else { goto label_5095; } } else { return __return_main; } } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_5019; } } else { goto label_5019; } } else { goto label_5012; } } else { goto label_5012; } } else { goto label_5005; } } else { goto label_5005; } } } else { return __return_main; } } } } else { goto label_4988; } } else { goto label_4988; } } else { goto label_4981; } } else { goto label_4981; } } else { goto label_4974; } } else { goto label_4974; } } } else { return __return_main; } } } } else { goto label_4957; } } else { goto label_4957; } } else { goto label_4950; } } else { goto label_4950; } } else { goto label_4943; } } else { goto label_4943; } } } else { return __return_main; } } } } else { goto label_4926; } } else { goto label_4926; } } else { goto label_4919; } } else { goto label_4919; } } else { goto label_4912; } } else { goto label_4912; } } } else { return __return_main; } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4839:; node4____CPAchecker_TMP_2 = p43_new; goto label_4840; } } else { goto label_4839; } } else { goto label_4842; } } else { label_4831:; node4____CPAchecker_TMP_1 = p42_new; goto label_4832; } } else { goto label_4831; } } else { goto label_4827; } } else { label_4823:; node4____CPAchecker_TMP_0 = p41_new; goto label_4824; } } else { goto label_4823; } } else { goto label_4819; } } else { return __return_main; } } } } else { label_4807:; node3____CPAchecker_TMP_2 = p34_new; goto label_4808; } } else { goto label_4807; } } else { goto label_4810; } } else { label_4799:; node3____CPAchecker_TMP_1 = p32_new; goto label_4800; } } else { goto label_4799; } } else { goto label_4795; } } else { label_4791:; node3____CPAchecker_TMP_0 = p31_new; goto label_4792; } } else { goto label_4791; } } else { goto label_4787; } } else { return __return_main; } } } } else { label_4775:; node2____CPAchecker_TMP_2 = p24_new; goto label_4776; } } else { goto label_4775; } } else { goto label_4778; } } else { label_4767:; node2____CPAchecker_TMP_1 = p23_new; goto label_4768; } } else { goto label_4767; } } else { goto label_4763; } } else { label_4759:; node2____CPAchecker_TMP_0 = p21_new; goto label_4760; } } else { goto label_4759; } } else { goto label_4755; } } else { return __return_main; } } } } else { label_4743:; node1____CPAchecker_TMP_2 = p14_new; goto label_4744; } } else { goto label_4743; } } else { goto label_4746; } } else { label_4735:; node1____CPAchecker_TMP_1 = p13_new; goto label_4736; } } else { goto label_4735; } } else { goto label_4731; } } else { label_4727:; node1____CPAchecker_TMP_0 = p12_new; goto label_4728; } } else { goto label_4727; } } else { goto label_4723; } } else { return __return_main; } } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4647; } } else { goto label_4647; } } else { goto label_4640; } } else { goto label_4640; } } else { goto label_4633; } } else { goto label_4633; } } } else { return __return_main; } } } } else { goto label_4616; } } else { goto label_4616; } } else { goto label_4609; } } else { goto label_4609; } } else { goto label_4602; } } else { goto label_4602; } } } else { return __return_main; } } } } else { goto label_4585; } } else { goto label_4585; } } else { goto label_4578; } } else { goto label_4578; } } else { goto label_4571; } } else { goto label_4571; } } } else { return __return_main; } } } } else { goto label_4554; } } else { goto label_4554; } } else { goto label_4547; } } else { goto label_4547; } } else { goto label_4540; } } else { goto label_4540; } } } else { return __return_main; } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4467:; node4____CPAchecker_TMP_2 = p43_new; goto label_4468; } } else { goto label_4467; } } else { goto label_4470; } } else { label_4459:; node4____CPAchecker_TMP_1 = p42_new; goto label_4460; } } else { goto label_4459; } } else { goto label_4455; } } else { label_4451:; node4____CPAchecker_TMP_0 = p41_new; goto label_4452; } } else { goto label_4451; } } else { goto label_4447; } } else { return __return_main; } } } } else { label_4435:; node3____CPAchecker_TMP_2 = p34_new; goto label_4436; } } else { goto label_4435; } } else { goto label_4438; } } else { label_4427:; node3____CPAchecker_TMP_1 = p32_new; goto label_4428; } } else { goto label_4427; } } else { goto label_4423; } } else { label_4419:; node3____CPAchecker_TMP_0 = p31_new; goto label_4420; } } else { goto label_4419; } } else { goto label_4415; } } else { return __return_main; } } } } else { label_4403:; node2____CPAchecker_TMP_2 = p24_new; goto label_4404; } } else { goto label_4403; } } else { goto label_4406; } } else { label_4395:; node2____CPAchecker_TMP_1 = p23_new; goto label_4396; } } else { goto label_4395; } } else { goto label_4391; } } else { label_4387:; node2____CPAchecker_TMP_0 = p21_new; goto label_4388; } } else { goto label_4387; } } else { goto label_4383; } } else { return __return_main; } } } } else { label_4371:; node1____CPAchecker_TMP_2 = p14_new; goto label_4372; } } else { goto label_4371; } } else { goto label_4374; } } else { label_4363:; node1____CPAchecker_TMP_1 = p13_new; goto label_4364; } } else { goto label_4363; } } else { goto label_4359; } } else { label_4355:; node1____CPAchecker_TMP_0 = p12_new; goto label_4356; } } else { goto label_4355; } } else { goto label_4351; } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { 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_4229; } else { label_6956:; if (!(init__r422 == 0)) { if (!(ep23 == 0)) { init__tmp___22 = 1; label_6962:; goto label_4229; } else { init__tmp___22 = 0; goto label_6962; } } else { init__tmp___22 = 0; goto label_4229; } } } else { goto label_6956; } } } else { if (!(init__r412 == 0)) { if (!(ep12 == 0)) { init__tmp___21 = 1; goto label_4224; } else { label_6971:; if (!(init__r432 == 0)) { if (!(ep32 == 0)) { init__tmp___21 = 1; label_6977:; goto label_4224; } else { init__tmp___21 = 0; goto label_6977; } } else { init__tmp___21 = 0; goto label_4224; } } } else { goto label_6971; } } } else { if (!(init__r422 == 0)) { if (!(ep21 == 0)) { init__tmp___20 = 1; goto label_4219; } else { label_6986:; if (!(init__r432 == 0)) { if (!(ep31 == 0)) { init__tmp___20 = 1; label_6992:; goto label_4219; } else { init__tmp___20 = 0; goto label_6992; } } else { init__tmp___20 = 0; goto label_4219; } } } else { goto label_6986; } } } else { if (!(init__r312 == 0)) { if (!(ep14 == 0)) { init__tmp___19 = 1; goto label_4214; } else { label_7001:; if (!(init__r322 == 0)) { if (!(ep24 == 0)) { init__tmp___19 = 1; label_7007:; goto label_4214; } else { init__tmp___19 = 0; goto label_7007; } } else { init__tmp___19 = 0; goto label_4214; } } } else { goto label_7001; } } } else { if (!(init__r312 == 0)) { if (!(ep12 == 0)) { init__tmp___18 = 1; goto label_4209; } else { label_7016:; if (!(init__r342 == 0)) { if (!(ep42 == 0)) { init__tmp___18 = 1; label_7022:; goto label_4209; } else { init__tmp___18 = 0; goto label_7022; } } else { init__tmp___18 = 0; goto label_4209; } } } else { goto label_7016; } } } else { if (!(init__r322 == 0)) { if (!(ep21 == 0)) { init__tmp___17 = 1; goto label_4204; } else { label_7031:; if (!(init__r342 == 0)) { if (!(ep41 == 0)) { init__tmp___17 = 1; label_7037:; goto label_4204; } else { init__tmp___17 = 0; goto label_7037; } } else { init__tmp___17 = 0; goto label_4204; } } } else { goto label_7031; } } } else { if (!(init__r212 == 0)) { if (!(ep14 == 0)) { init__tmp___16 = 1; goto label_4199; } else { label_7046:; if (!(init__r232 == 0)) { if (!(ep34 == 0)) { init__tmp___16 = 1; label_7052:; goto label_4199; } else { init__tmp___16 = 0; goto label_7052; } } else { init__tmp___16 = 0; goto label_4199; } } } else { goto label_7046; } } } else { if (!(init__r212 == 0)) { if (!(ep13 == 0)) { init__tmp___15 = 1; goto label_4194; } else { label_7061:; if (!(init__r242 == 0)) { if (!(ep43 == 0)) { init__tmp___15 = 1; label_7067:; goto label_4194; } else { init__tmp___15 = 0; goto label_7067; } } else { init__tmp___15 = 0; goto label_4194; } } } else { goto label_7061; } } } else { if (!(init__r232 == 0)) { if (!(ep31 == 0)) { init__tmp___14 = 1; goto label_4189; } else { label_7076:; if (!(init__r242 == 0)) { if (!(ep41 == 0)) { init__tmp___14 = 1; label_7082:; goto label_4189; } else { init__tmp___14 = 0; goto label_7082; } } else { init__tmp___14 = 0; goto label_4189; } } } else { goto label_7076; } } } else { if (!(init__r122 == 0)) { if (!(ep24 == 0)) { init__tmp___13 = 1; goto label_4184; } else { label_7091:; if (!(init__r132 == 0)) { if (!(ep34 == 0)) { init__tmp___13 = 1; label_7097:; goto label_4184; } else { init__tmp___13 = 0; goto label_7097; } } else { init__tmp___13 = 0; goto label_4184; } } } else { goto label_7091; } } } else { if (!(init__r122 == 0)) { if (!(ep23 == 0)) { init__tmp___12 = 1; goto label_4179; } else { label_7106:; if (!(init__r142 == 0)) { if (!(ep43 == 0)) { init__tmp___12 = 1; label_7112:; goto label_4179; } else { init__tmp___12 = 0; goto label_7112; } } else { init__tmp___12 = 0; goto label_4179; } } } else { goto label_7106; } } } else { if (!(init__r132 == 0)) { if (!(ep32 == 0)) { init__tmp___11 = 1; goto label_4174; } else { label_7121:; if (!(init__r142 == 0)) { if (!(ep42 == 0)) { init__tmp___11 = 1; label_7127:; goto label_4174; } else { init__tmp___11 = 0; goto label_7127; } } else { init__tmp___11 = 0; goto label_4174; } } } else { goto label_7121; } } } else { if (!(init__r411 == 0)) { if (!(ep13 == 0)) { init__tmp___10 = 1; goto label_4169; } else { label_7136:; if (!(init__r421 == 0)) { if (!(ep23 == 0)) { init__tmp___10 = 1; label_7142:; goto label_4169; } else { init__tmp___10 = 0; goto label_7142; } } else { init__tmp___10 = 0; goto label_4169; } } } else { goto label_7136; } } } else { if (!(init__r411 == 0)) { if (!(ep12 == 0)) { init__tmp___9 = 1; goto label_4164; } else { label_7151:; if (!(init__r431 == 0)) { if (!(ep32 == 0)) { init__tmp___9 = 1; label_7157:; goto label_4164; } else { init__tmp___9 = 0; goto label_7157; } } else { init__tmp___9 = 0; goto label_4164; } } } else { goto label_7151; } } } else { if (!(init__r421 == 0)) { if (!(ep21 == 0)) { init__tmp___8 = 1; goto label_4159; } else { label_7166:; if (!(init__r431 == 0)) { if (!(ep31 == 0)) { init__tmp___8 = 1; label_7172:; goto label_4159; } else { init__tmp___8 = 0; goto label_7172; } } else { init__tmp___8 = 0; goto label_4159; } } } else { goto label_7166; } } } else { if (!(init__r311 == 0)) { if (!(ep14 == 0)) { init__tmp___7 = 1; goto label_4154; } else { label_7181:; if (!(init__r321 == 0)) { if (!(ep24 == 0)) { init__tmp___7 = 1; label_7187:; goto label_4154; } else { init__tmp___7 = 0; goto label_7187; } } else { init__tmp___7 = 0; goto label_4154; } } } else { goto label_7181; } } } else { if (!(init__r311 == 0)) { if (!(ep12 == 0)) { init__tmp___6 = 1; goto label_4149; } else { label_7196:; if (!(init__r341 == 0)) { if (!(ep42 == 0)) { init__tmp___6 = 1; label_7202:; goto label_4149; } else { init__tmp___6 = 0; goto label_7202; } } else { init__tmp___6 = 0; goto label_4149; } } } else { goto label_7196; } } } else { if (!(init__r321 == 0)) { if (!(ep21 == 0)) { init__tmp___5 = 1; goto label_4144; } else { label_7211:; if (!(init__r341 == 0)) { if (!(ep41 == 0)) { init__tmp___5 = 1; label_7217:; goto label_4144; } else { init__tmp___5 = 0; goto label_7217; } } else { init__tmp___5 = 0; goto label_4144; } } } else { goto label_7211; } } } else { if (!(init__r211 == 0)) { if (!(ep14 == 0)) { init__tmp___4 = 1; goto label_4139; } else { label_7226:; if (!(init__r231 == 0)) { if (!(ep34 == 0)) { init__tmp___4 = 1; label_7232:; goto label_4139; } else { init__tmp___4 = 0; goto label_7232; } } else { init__tmp___4 = 0; goto label_4139; } } } else { goto label_7226; } } } else { if (!(init__r211 == 0)) { if (!(ep13 == 0)) { init__tmp___3 = 1; goto label_4134; } else { label_7241:; if (!(init__r241 == 0)) { if (!(ep43 == 0)) { init__tmp___3 = 1; label_7247:; goto label_4134; } else { init__tmp___3 = 0; goto label_7247; } } else { init__tmp___3 = 0; goto label_4134; } } } else { goto label_7241; } } } else { if (!(init__r231 == 0)) { if (!(ep31 == 0)) { init__tmp___2 = 1; goto label_4129; } else { label_7256:; if (!(init__r241 == 0)) { if (!(ep41 == 0)) { init__tmp___2 = 1; label_7262:; goto label_4129; } else { init__tmp___2 = 0; goto label_7262; } } else { init__tmp___2 = 0; goto label_4129; } } } else { goto label_7256; } } } else { if (!(init__r121 == 0)) { if (!(ep24 == 0)) { init__tmp___1 = 1; goto label_4124; } else { label_7271:; if (!(init__r131 == 0)) { if (!(ep34 == 0)) { init__tmp___1 = 1; label_7277:; goto label_4124; } else { init__tmp___1 = 0; goto label_7277; } } else { init__tmp___1 = 0; goto label_4124; } } } else { goto label_7271; } } } else { if (!(init__r121 == 0)) { if (!(ep23 == 0)) { init__tmp___0 = 1; goto label_4119; } else { label_7286:; if (!(init__r141 == 0)) { if (!(ep43 == 0)) { init__tmp___0 = 1; label_7292:; goto label_4119; } else { init__tmp___0 = 0; goto label_7292; } } else { init__tmp___0 = 0; goto label_4119; } } } else { goto label_7286; } } } else { if (!(init__r131 == 0)) { if (!(ep32 == 0)) { init__tmp = 1; goto label_4114; } else { label_7301:; if (!(init__r141 == 0)) { if (!(ep42 == 0)) { init__tmp = 1; label_7307:; goto label_4114; } else { init__tmp = 0; goto label_7307; } } else { init__tmp = 0; goto label_4114; } } } else { goto label_7301; } } } }