// 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.p+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_4496; int __return_4694; int __return_4870; int __return_5046; int __return_5222; int __return_5398; int __return_5574; int __return_5751; 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_4375:; init__r122 = (_Bool)init__tmp; if (!(init__r131 == 0)) { init__tmp___0 = 1; label_4380:; init__r132 = (_Bool)init__tmp___0; if (!(init__r141 == 0)) { init__tmp___1 = 1; label_4385:; init__r142 = (_Bool)init__tmp___1; if (!(init__r211 == 0)) { init__tmp___2 = 1; label_4390:; init__r212 = (_Bool)init__tmp___2; if (!(init__r231 == 0)) { init__tmp___3 = 1; label_4395:; init__r232 = (_Bool)init__tmp___3; if (!(init__r241 == 0)) { init__tmp___4 = 1; label_4400:; init__r242 = (_Bool)init__tmp___4; if (!(init__r311 == 0)) { init__tmp___5 = 1; label_4405:; init__r312 = (_Bool)init__tmp___5; if (!(init__r321 == 0)) { init__tmp___6 = 1; label_4410:; init__r322 = (_Bool)init__tmp___6; if (!(init__r341 == 0)) { init__tmp___7 = 1; label_4415:; init__r342 = (_Bool)init__tmp___7; if (!(init__r411 == 0)) { init__tmp___8 = 1; label_4420:; init__r412 = (_Bool)init__tmp___8; if (!(init__r421 == 0)) { init__tmp___9 = 1; label_4425:; init__r422 = (_Bool)init__tmp___9; if (!(init__r431 == 0)) { init__tmp___10 = 1; label_4430:; init__r432 = (_Bool)init__tmp___10; if (!(init__r122 == 0)) { init__tmp___11 = 1; label_4435:; init__r123 = (_Bool)init__tmp___11; if (!(init__r132 == 0)) { init__tmp___12 = 1; label_4440:; init__r133 = (_Bool)init__tmp___12; if (!(init__r142 == 0)) { init__tmp___13 = 1; label_4445:; init__r143 = (_Bool)init__tmp___13; if (!(init__r212 == 0)) { init__tmp___14 = 1; label_4450:; init__r213 = (_Bool)init__tmp___14; if (!(init__r232 == 0)) { init__tmp___15 = 1; label_4455:; init__r233 = (_Bool)init__tmp___15; if (!(init__r242 == 0)) { init__tmp___16 = 1; label_4460:; init__r243 = (_Bool)init__tmp___16; if (!(init__r312 == 0)) { init__tmp___17 = 1; label_4465:; init__r313 = (_Bool)init__tmp___17; if (!(init__r322 == 0)) { init__tmp___18 = 1; label_4470:; init__r323 = (_Bool)init__tmp___18; if (!(init__r342 == 0)) { init__tmp___19 = 1; label_4475:; init__r343 = (_Bool)init__tmp___19; if (!(init__r412 == 0)) { init__tmp___20 = 1; label_4480:; init__r413 = (_Bool)init__tmp___20; if (!(init__r422 == 0)) { init__tmp___21 = 1; label_4485:; init__r423 = (_Bool)init__tmp___21; if (!(init__r432 == 0)) { init__tmp___22 = 1; label_4490:; 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; label_7124:; label_7120:; label_7116:; label_7112:; label_7108:; label_7104:; label_7100:; label_7096:; label_7092:; label_7088:; label_7084:; label_7080:; label_7076:; label_7072:; label_7068:; label_7052:; label_7053:; label_7054:; label_7055:; label_7056:; label_7057:; label_7058:; label_7059:; label_7060:; label_7061:; label_7062:; label_7063:; label_7064:; label_7024:; label_7020:; label_7016:; label_7012:; label_7008:; label_7004:; label_7000:; label_6996:; label_6992:; label_6988:; label_6984:; label_6980:; label_6976:; label_4495:; __return_4496 = init__tmp___23; main__i2 = __return_4496; 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)) { if (r1 == 255) { r1 = 3; label_4532:; r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4534:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4541:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4548:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_4556:; mode1 = 0; label_4558:; { if (!(mode2 == 0)) { if (r2 == 255) { r2 = 3; label_4566:; r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4568:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4575:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4582:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_4590:; mode2 = 0; label_4592:; { if (!(mode3 == 0)) { if (r3 == 255) { r3 = 3; label_4600:; 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) { if (((int)max3) == ((int)id3)) { st3 = 1; label_4624:; mode3 = 0; label_4626:; { if (!(mode4 == 0)) { if (r4 == 255) { r4 = 3; label_4634:; r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4636:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4643:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4650:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_4658:; mode4 = 0; label_4660:; 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_6822:; if (((int)r1) < 3) { label_6829:; if (((int)r1) >= 3) { label_6836:; if (((int)r1) < 3) { check__tmp = 1; label_6842:; label_6835:; label_6828:; label_6821:; label_6815:; label_6811:; label_6807:; label_6803:; label_4693:; __return_4694 = check__tmp; main__c1 = __return_4694; { _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) { r1 = 3; label_4708:; r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4710:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4717:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4724:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_4732:; mode1 = 0; label_4734:; { if (!(mode2 == 0)) { if (r2 == 255) { r2 = 3; label_4742:; r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4744:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4751:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4758:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_4766:; mode2 = 0; label_4768:; { if (!(mode3 == 0)) { if (r3 == 255) { r3 = 3; label_4776:; r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4778:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4785:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4792:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_4800:; mode3 = 0; label_4802:; { if (!(mode4 == 0)) { if (r4 == 255) { r4 = 3; label_4810:; r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4812:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4819:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4826:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_4834:; mode4 = 0; label_4836:; 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_6649:; if (((int)r1) < 3) { label_6656:; if (((int)r1) >= 3) { label_6663:; if (((int)r1) < 3) { check__tmp = 1; label_6669:; label_6662:; label_6655:; label_6648:; label_6642:; label_6638:; label_6634:; label_6630:; label_4869:; __return_4870 = check__tmp; main__c1 = __return_4870; { _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)) { if (r1 == 255) { r1 = 3; label_4884:; r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4886:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4893:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4900:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_4908:; mode1 = 0; label_4910:; { if (!(mode2 == 0)) { if (r2 == 255) { r2 = 3; label_4918:; r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4920:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4927:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4934:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_4942:; mode2 = 0; label_4944:; { if (!(mode3 == 0)) { if (r3 == 255) { r3 = 3; label_4952:; r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4954:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4961:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4968:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_4976:; mode3 = 0; label_4978:; { if (!(mode4 == 0)) { if (r4 == 255) { r4 = 3; label_4986:; r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4988:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4995:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5002:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5010:; mode4 = 0; label_5012:; 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_6476:; if (((int)r1) < 3) { label_6483:; if (((int)r1) >= 3) { label_6490:; if (((int)r1) < 3) { check__tmp = 1; label_6496:; label_6489:; label_6482:; label_6475:; label_6469:; label_6465:; label_6461:; label_6457:; label_5045:; __return_5046 = check__tmp; main__c1 = __return_5046; { _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) { r1 = 3; label_5060:; r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5062:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5069:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5076:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5084:; mode1 = 0; label_5086:; { if (!(mode2 == 0)) { if (r2 == 255) { r2 = 3; label_5094:; r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5096:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5103:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5110:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5118:; mode2 = 0; label_5120:; { if (!(mode3 == 0)) { if (r3 == 255) { r3 = 3; label_5128:; r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5130:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5137:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5144:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5152:; mode3 = 0; label_5154:; { if (!(mode4 == 0)) { if (r4 == 255) { r4 = 3; label_5162:; r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5164:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5171:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5178:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5186:; mode4 = 0; label_5188:; 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_6303:; if (((int)r1) < 3) { label_6310:; if (((int)r1) >= 3) { label_6317:; if (((int)r1) < 3) { check__tmp = 1; label_6323:; label_6316:; label_6309:; label_6302:; label_6296:; label_6292:; label_6288:; label_6284:; label_5221:; __return_5222 = check__tmp; main__c1 = __return_5222; { _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)) { if (r1 == 255) { r1 = 3; label_5236:; r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5238:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5245:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5252:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5260:; mode1 = 0; label_5262:; { if (!(mode2 == 0)) { if (r2 == 255) { r2 = 3; label_5270:; r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5272:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5279:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5286:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5294:; mode2 = 0; label_5296:; { if (!(mode3 == 0)) { if (r3 == 255) { r3 = 3; label_5304:; r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5306:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5313:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5320:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5328:; mode3 = 0; label_5330:; { if (!(mode4 == 0)) { if (r4 == 255) { r4 = 3; label_5338:; r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5340:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5347:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5354:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5362:; mode4 = 0; label_5364:; 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_6130:; if (((int)r1) < 3) { label_6137:; if (((int)r1) >= 3) { label_6144:; if (((int)r1) < 3) { check__tmp = 1; label_6150:; label_6143:; label_6136:; label_6129:; label_6123:; label_6119:; label_6115:; label_6111:; label_5397:; __return_5398 = check__tmp; main__c1 = __return_5398; { _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) { r1 = 3; label_5412:; r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5414:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5421:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5428:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5436:; mode1 = 0; label_5438:; { if (!(mode2 == 0)) { if (r2 == 255) { r2 = 3; label_5446:; r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5448:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5455:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5462:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5470:; mode2 = 0; label_5472:; { if (!(mode3 == 0)) { if (r3 == 255) { r3 = 3; label_5480:; r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5482:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5489:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5496:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5504:; mode3 = 0; label_5506:; { if (!(mode4 == 0)) { if (r4 == 255) { r4 = 3; label_5514:; r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5516:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5523:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5530:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5538:; mode4 = 0; label_5540:; 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_5957:; if (((int)r1) < 3) { label_5964:; if (((int)r1) >= 3) { label_5971:; if (((int)r1) < 3) { check__tmp = 1; label_5977:; label_5970:; label_5963:; label_5956:; label_5950:; label_5946:; label_5942:; label_5938:; label_5573:; __return_5574 = check__tmp; main__c1 = __return_5574; { _Bool __tmp_6; __tmp_6 = main__c1; _Bool assert__arg; assert__arg = __tmp_6; if (assert__arg == 0) { {reach_error();} return __return_main; } else { label_5581:; { if (!(mode1 == 0)) { if (r1 == 255) { r1 = 3; label_5589:; r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5591:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5598:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5605:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5613:; mode1 = 0; label_5615:; { if (!(mode2 == 0)) { if (r2 == 255) { r2 = 3; label_5623:; r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5625:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5632:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5639:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5647:; mode2 = 0; label_5649:; { if (!(mode3 == 0)) { if (r3 == 255) { r3 = 3; label_5657:; r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5659:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5666:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5673:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5681:; mode3 = 0; label_5683:; { if (!(mode4 == 0)) { if (r4 == 255) { r4 = 3; label_5691:; r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5693:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5700:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5707:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5715:; mode4 = 0; label_5717:; 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_5782:; if (((int)r1) < 3) { label_5789:; if (((int)r1) >= 3) { label_5796:; if (((int)r1) < 3) { check__tmp = 1; label_5802:; label_5795:; label_5788:; label_5781:; label_5775:; label_5771:; label_5767:; label_5763:; label_5750:; __return_5751 = check__tmp; main__c1 = __return_5751; { _Bool __tmp_7; __tmp_7 = main__c1; _Bool assert__arg; assert__arg = __tmp_7; if (assert__arg == 0) { {reach_error();} return __return_main; } else { goto label_5581; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5802; } else { check__tmp = 0; goto label_5802; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5796; } else { check__tmp = 0; goto label_5795; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_5789; } else { check__tmp = 0; goto label_5788; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_5782; } else { check__tmp = 0; goto label_5781; } } } else { check__tmp = 0; goto label_5775; } } else { check__tmp = 0; goto label_5771; } } else { check__tmp = 0; goto label_5767; } } else { check__tmp = 0; goto label_5763; } } else { check__tmp = 0; goto label_5750; } } } else { nl4 = 1; goto label_5715; } } else { goto label_5715; } } else { goto label_5707; } } else { goto label_5707; } } else { goto label_5700; } } else { goto label_5700; } } else { goto label_5693; } } else { goto label_5693; } } else { goto label_5691; } } 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_5818:; p41_new = node4____CPAchecker_TMP_0; label_5813:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5826:; p42_new = node4____CPAchecker_TMP_1; label_5821:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5834:; p43_new = node4____CPAchecker_TMP_2; label_5811:; mode4 = 1; goto label_5717; } else { label_5833:; node4____CPAchecker_TMP_2 = p43_new; goto label_5834; } } else { goto label_5833; } } else { goto label_5811; } } else { label_5825:; node4____CPAchecker_TMP_1 = p42_new; goto label_5826; } } else { goto label_5825; } } else { goto label_5821; } } else { label_5817:; node4____CPAchecker_TMP_0 = p41_new; goto label_5818; } } else { goto label_5817; } } else { goto label_5813; } } else { goto label_5811; } } } } else { nl3 = 1; goto label_5681; } } else { goto label_5681; } } else { goto label_5673; } } else { goto label_5673; } } else { goto label_5666; } } else { goto label_5666; } } else { goto label_5659; } } else { goto label_5659; } } else { goto label_5657; } } 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_5850:; p31_new = node3____CPAchecker_TMP_0; label_5845:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5858:; p32_new = node3____CPAchecker_TMP_1; label_5853:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5866:; p34_new = node3____CPAchecker_TMP_2; label_5843:; mode3 = 1; goto label_5683; } else { label_5865:; node3____CPAchecker_TMP_2 = p34_new; goto label_5866; } } else { goto label_5865; } } else { goto label_5843; } } else { label_5857:; node3____CPAchecker_TMP_1 = p32_new; goto label_5858; } } else { goto label_5857; } } else { goto label_5853; } } else { label_5849:; node3____CPAchecker_TMP_0 = p31_new; goto label_5850; } } else { goto label_5849; } } else { goto label_5845; } } else { goto label_5843; } } } } else { nl2 = 1; goto label_5647; } } else { goto label_5647; } } else { goto label_5639; } } else { goto label_5639; } } else { goto label_5632; } } else { goto label_5632; } } else { goto label_5625; } } else { goto label_5625; } } else { goto label_5623; } } 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_5882:; p21_new = node2____CPAchecker_TMP_0; label_5877:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5890:; p23_new = node2____CPAchecker_TMP_1; label_5885:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5898:; p24_new = node2____CPAchecker_TMP_2; label_5875:; mode2 = 1; goto label_5649; } else { label_5897:; node2____CPAchecker_TMP_2 = p24_new; goto label_5898; } } else { goto label_5897; } } else { goto label_5875; } } else { label_5889:; node2____CPAchecker_TMP_1 = p23_new; goto label_5890; } } else { goto label_5889; } } else { goto label_5885; } } else { label_5881:; node2____CPAchecker_TMP_0 = p21_new; goto label_5882; } } else { goto label_5881; } } else { goto label_5877; } } else { goto label_5875; } } } } else { nl1 = 1; goto label_5613; } } else { goto label_5613; } } else { goto label_5605; } } else { goto label_5605; } } else { goto label_5598; } } else { goto label_5598; } } else { goto label_5591; } } else { goto label_5591; } } else { goto label_5589; } } 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_5914:; p12_new = node1____CPAchecker_TMP_0; label_5909:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5922:; p13_new = node1____CPAchecker_TMP_1; label_5917:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5930:; p14_new = node1____CPAchecker_TMP_2; label_5907:; mode1 = 1; goto label_5615; } else { label_5929:; node1____CPAchecker_TMP_2 = p14_new; goto label_5930; } } else { goto label_5929; } } else { goto label_5907; } } else { label_5921:; node1____CPAchecker_TMP_1 = p13_new; goto label_5922; } } else { goto label_5921; } } else { goto label_5917; } } else { label_5913:; node1____CPAchecker_TMP_0 = p12_new; goto label_5914; } } else { goto label_5913; } } else { goto label_5909; } } else { goto label_5907; } } } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5977; } else { check__tmp = 0; goto label_5977; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5971; } else { check__tmp = 0; goto label_5970; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_5964; } else { check__tmp = 0; goto label_5963; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_5957; } else { check__tmp = 0; goto label_5956; } } } else { check__tmp = 0; goto label_5950; } } else { check__tmp = 0; goto label_5946; } } else { check__tmp = 0; goto label_5942; } } else { check__tmp = 0; goto label_5938; } } else { check__tmp = 0; goto label_5573; } } } else { nl4 = 1; goto label_5538; } } else { goto label_5538; } } else { goto label_5530; } } else { goto label_5530; } } else { goto label_5523; } } else { goto label_5523; } } else { goto label_5516; } } else { goto label_5516; } } else { goto label_5514; } } 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_5993:; p41_new = node4____CPAchecker_TMP_0; label_5988:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_6001:; p42_new = node4____CPAchecker_TMP_1; label_5996:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_6009:; p43_new = node4____CPAchecker_TMP_2; label_5986:; mode4 = 1; goto label_5540; } else { label_6008:; node4____CPAchecker_TMP_2 = p43_new; goto label_6009; } } else { goto label_6008; } } else { goto label_5986; } } else { label_6000:; node4____CPAchecker_TMP_1 = p42_new; goto label_6001; } } else { goto label_6000; } } else { goto label_5996; } } else { label_5992:; node4____CPAchecker_TMP_0 = p41_new; goto label_5993; } } else { goto label_5992; } } else { goto label_5988; } } else { goto label_5986; } } } } else { nl3 = 1; goto label_5504; } } else { goto label_5504; } } else { goto label_5496; } } else { goto label_5496; } } else { goto label_5489; } } else { goto label_5489; } } else { goto label_5482; } } else { goto label_5482; } } else { goto label_5480; } } 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_6025:; p31_new = node3____CPAchecker_TMP_0; label_6020:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_6033:; p32_new = node3____CPAchecker_TMP_1; label_6028:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_6041:; p34_new = node3____CPAchecker_TMP_2; label_6018:; mode3 = 1; goto label_5506; } else { label_6040:; node3____CPAchecker_TMP_2 = p34_new; goto label_6041; } } else { goto label_6040; } } else { goto label_6018; } } else { label_6032:; node3____CPAchecker_TMP_1 = p32_new; goto label_6033; } } else { goto label_6032; } } else { goto label_6028; } } else { label_6024:; node3____CPAchecker_TMP_0 = p31_new; goto label_6025; } } else { goto label_6024; } } else { goto label_6020; } } else { goto label_6018; } } } } else { nl2 = 1; goto label_5470; } } else { goto label_5470; } } else { goto label_5462; } } else { goto label_5462; } } else { goto label_5455; } } else { goto label_5455; } } else { goto label_5448; } } else { goto label_5448; } } else { goto label_5446; } } 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_6057:; p21_new = node2____CPAchecker_TMP_0; label_6052:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_6065:; p23_new = node2____CPAchecker_TMP_1; label_6060:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_6073:; p24_new = node2____CPAchecker_TMP_2; label_6050:; mode2 = 1; goto label_5472; } else { label_6072:; node2____CPAchecker_TMP_2 = p24_new; goto label_6073; } } else { goto label_6072; } } else { goto label_6050; } } else { label_6064:; node2____CPAchecker_TMP_1 = p23_new; goto label_6065; } } else { goto label_6064; } } else { goto label_6060; } } else { label_6056:; node2____CPAchecker_TMP_0 = p21_new; goto label_6057; } } else { goto label_6056; } } else { goto label_6052; } } else { goto label_6050; } } } } else { nl1 = 1; goto label_5436; } } else { goto label_5436; } } else { goto label_5428; } } else { goto label_5428; } } else { goto label_5421; } } else { goto label_5421; } } else { goto label_5414; } } else { goto label_5414; } } else { goto label_5412; } } 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_6089:; p12_new = node1____CPAchecker_TMP_0; label_6084:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_6097:; p13_new = node1____CPAchecker_TMP_1; label_6092:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_6105:; p14_new = node1____CPAchecker_TMP_2; label_6082:; mode1 = 1; goto label_5438; } else { label_6104:; node1____CPAchecker_TMP_2 = p14_new; goto label_6105; } } else { goto label_6104; } } else { goto label_6082; } } else { label_6096:; node1____CPAchecker_TMP_1 = p13_new; goto label_6097; } } else { goto label_6096; } } else { goto label_6092; } } else { label_6088:; node1____CPAchecker_TMP_0 = p12_new; goto label_6089; } } else { goto label_6088; } } else { goto label_6084; } } else { goto label_6082; } } } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6150; } else { check__tmp = 0; goto label_6150; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6144; } else { check__tmp = 0; goto label_6143; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_6137; } else { check__tmp = 0; goto label_6136; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_6130; } else { check__tmp = 0; goto label_6129; } } } else { check__tmp = 0; goto label_6123; } } else { check__tmp = 0; goto label_6119; } } else { check__tmp = 0; goto label_6115; } } else { check__tmp = 0; goto label_6111; } } else { check__tmp = 0; goto label_5397; } } } else { nl4 = 1; goto label_5362; } } else { goto label_5362; } } else { goto label_5354; } } else { goto label_5354; } } else { goto label_5347; } } else { goto label_5347; } } else { goto label_5340; } } else { goto label_5340; } } else { goto label_5338; } } 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_6166:; p41_new = node4____CPAchecker_TMP_0; label_6161:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_6174:; p42_new = node4____CPAchecker_TMP_1; label_6169:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_6182:; p43_new = node4____CPAchecker_TMP_2; label_6159:; mode4 = 1; goto label_5364; } else { label_6181:; node4____CPAchecker_TMP_2 = p43_new; goto label_6182; } } else { goto label_6181; } } else { goto label_6159; } } else { label_6173:; node4____CPAchecker_TMP_1 = p42_new; goto label_6174; } } else { goto label_6173; } } else { goto label_6169; } } else { label_6165:; node4____CPAchecker_TMP_0 = p41_new; goto label_6166; } } else { goto label_6165; } } else { goto label_6161; } } else { goto label_6159; } } } } else { nl3 = 1; goto label_5328; } } else { goto label_5328; } } else { goto label_5320; } } else { goto label_5320; } } else { goto label_5313; } } else { goto label_5313; } } else { goto label_5306; } } else { goto label_5306; } } else { goto label_5304; } } 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_6198:; p31_new = node3____CPAchecker_TMP_0; label_6193:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_6206:; p32_new = node3____CPAchecker_TMP_1; label_6201:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_6214:; p34_new = node3____CPAchecker_TMP_2; label_6191:; mode3 = 1; goto label_5330; } else { label_6213:; node3____CPAchecker_TMP_2 = p34_new; goto label_6214; } } else { goto label_6213; } } else { goto label_6191; } } else { label_6205:; node3____CPAchecker_TMP_1 = p32_new; goto label_6206; } } else { goto label_6205; } } else { goto label_6201; } } else { label_6197:; node3____CPAchecker_TMP_0 = p31_new; goto label_6198; } } else { goto label_6197; } } else { goto label_6193; } } else { goto label_6191; } } } } else { nl2 = 1; goto label_5294; } } else { goto label_5294; } } else { goto label_5286; } } else { goto label_5286; } } else { goto label_5279; } } else { goto label_5279; } } else { goto label_5272; } } else { goto label_5272; } } else { goto label_5270; } } 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_6230:; p21_new = node2____CPAchecker_TMP_0; label_6225:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_6238:; p23_new = node2____CPAchecker_TMP_1; label_6233:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_6246:; p24_new = node2____CPAchecker_TMP_2; label_6223:; mode2 = 1; goto label_5296; } else { label_6245:; node2____CPAchecker_TMP_2 = p24_new; goto label_6246; } } else { goto label_6245; } } else { goto label_6223; } } else { label_6237:; node2____CPAchecker_TMP_1 = p23_new; goto label_6238; } } else { goto label_6237; } } else { goto label_6233; } } else { label_6229:; node2____CPAchecker_TMP_0 = p21_new; goto label_6230; } } else { goto label_6229; } } else { goto label_6225; } } else { goto label_6223; } } } } else { nl1 = 1; goto label_5260; } } else { goto label_5260; } } else { goto label_5252; } } else { goto label_5252; } } else { goto label_5245; } } else { goto label_5245; } } else { goto label_5238; } } else { goto label_5238; } } else { goto label_5236; } } 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_6262:; p12_new = node1____CPAchecker_TMP_0; label_6257:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_6270:; p13_new = node1____CPAchecker_TMP_1; label_6265:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_6278:; p14_new = node1____CPAchecker_TMP_2; label_6255:; mode1 = 1; goto label_5262; } else { label_6277:; node1____CPAchecker_TMP_2 = p14_new; goto label_6278; } } else { goto label_6277; } } else { goto label_6255; } } else { label_6269:; node1____CPAchecker_TMP_1 = p13_new; goto label_6270; } } else { goto label_6269; } } else { goto label_6265; } } else { label_6261:; node1____CPAchecker_TMP_0 = p12_new; goto label_6262; } } else { goto label_6261; } } else { goto label_6257; } } else { goto label_6255; } } } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6323; } else { check__tmp = 0; goto label_6323; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6317; } else { check__tmp = 0; goto label_6316; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_6310; } else { check__tmp = 0; goto label_6309; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_6303; } else { check__tmp = 0; goto label_6302; } } } else { check__tmp = 0; goto label_6296; } } else { check__tmp = 0; goto label_6292; } } else { check__tmp = 0; goto label_6288; } } else { check__tmp = 0; goto label_6284; } } else { check__tmp = 0; goto label_5221; } } } else { nl4 = 1; goto label_5186; } } else { goto label_5186; } } else { goto label_5178; } } else { goto label_5178; } } else { goto label_5171; } } else { goto label_5171; } } else { goto label_5164; } } else { goto label_5164; } } else { goto label_5162; } } 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_6339:; p41_new = node4____CPAchecker_TMP_0; label_6334:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_6347:; p42_new = node4____CPAchecker_TMP_1; label_6342:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_6355:; p43_new = node4____CPAchecker_TMP_2; label_6332:; mode4 = 1; goto label_5188; } else { label_6354:; node4____CPAchecker_TMP_2 = p43_new; goto label_6355; } } else { goto label_6354; } } else { goto label_6332; } } else { label_6346:; node4____CPAchecker_TMP_1 = p42_new; goto label_6347; } } else { goto label_6346; } } else { goto label_6342; } } else { label_6338:; node4____CPAchecker_TMP_0 = p41_new; goto label_6339; } } else { goto label_6338; } } else { goto label_6334; } } else { goto label_6332; } } } } else { nl3 = 1; goto label_5152; } } else { goto label_5152; } } else { goto label_5144; } } else { goto label_5144; } } else { goto label_5137; } } else { goto label_5137; } } else { goto label_5130; } } else { goto label_5130; } } else { goto label_5128; } } 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_6371:; p31_new = node3____CPAchecker_TMP_0; label_6366:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_6379:; p32_new = node3____CPAchecker_TMP_1; label_6374:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_6387:; p34_new = node3____CPAchecker_TMP_2; label_6364:; mode3 = 1; goto label_5154; } else { label_6386:; node3____CPAchecker_TMP_2 = p34_new; goto label_6387; } } else { goto label_6386; } } else { goto label_6364; } } else { label_6378:; node3____CPAchecker_TMP_1 = p32_new; goto label_6379; } } else { goto label_6378; } } else { goto label_6374; } } else { label_6370:; node3____CPAchecker_TMP_0 = p31_new; goto label_6371; } } else { goto label_6370; } } else { goto label_6366; } } else { goto label_6364; } } } } else { nl2 = 1; goto label_5118; } } else { goto label_5118; } } else { goto label_5110; } } else { goto label_5110; } } else { goto label_5103; } } else { goto label_5103; } } else { goto label_5096; } } else { goto label_5096; } } else { goto label_5094; } } 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_6403:; p21_new = node2____CPAchecker_TMP_0; label_6398:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_6411:; p23_new = node2____CPAchecker_TMP_1; label_6406:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_6419:; p24_new = node2____CPAchecker_TMP_2; label_6396:; mode2 = 1; goto label_5120; } else { label_6418:; node2____CPAchecker_TMP_2 = p24_new; goto label_6419; } } else { goto label_6418; } } else { goto label_6396; } } else { label_6410:; node2____CPAchecker_TMP_1 = p23_new; goto label_6411; } } else { goto label_6410; } } else { goto label_6406; } } else { label_6402:; node2____CPAchecker_TMP_0 = p21_new; goto label_6403; } } else { goto label_6402; } } else { goto label_6398; } } else { goto label_6396; } } } } else { nl1 = 1; goto label_5084; } } else { goto label_5084; } } else { goto label_5076; } } else { goto label_5076; } } else { goto label_5069; } } else { goto label_5069; } } else { goto label_5062; } } else { goto label_5062; } } else { goto label_5060; } } 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_6435:; p12_new = node1____CPAchecker_TMP_0; label_6430:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_6443:; p13_new = node1____CPAchecker_TMP_1; label_6438:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_6451:; p14_new = node1____CPAchecker_TMP_2; label_6428:; mode1 = 1; goto label_5086; } else { label_6450:; node1____CPAchecker_TMP_2 = p14_new; goto label_6451; } } else { goto label_6450; } } else { goto label_6428; } } else { label_6442:; node1____CPAchecker_TMP_1 = p13_new; goto label_6443; } } else { goto label_6442; } } else { goto label_6438; } } else { label_6434:; node1____CPAchecker_TMP_0 = p12_new; goto label_6435; } } else { goto label_6434; } } else { goto label_6430; } } else { goto label_6428; } } } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6496; } else { check__tmp = 0; goto label_6496; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6490; } else { check__tmp = 0; goto label_6489; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_6483; } else { check__tmp = 0; goto label_6482; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_6476; } else { check__tmp = 0; goto label_6475; } } } else { check__tmp = 0; goto label_6469; } } else { check__tmp = 0; goto label_6465; } } else { check__tmp = 0; goto label_6461; } } else { check__tmp = 0; goto label_6457; } } else { check__tmp = 0; goto label_5045; } } } else { nl4 = 1; goto label_5010; } } else { goto label_5010; } } else { goto label_5002; } } else { goto label_5002; } } else { goto label_4995; } } else { goto label_4995; } } else { goto label_4988; } } else { goto label_4988; } } else { goto label_4986; } } 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_6512:; p41_new = node4____CPAchecker_TMP_0; label_6507:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_6520:; p42_new = node4____CPAchecker_TMP_1; label_6515:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_6528:; p43_new = node4____CPAchecker_TMP_2; label_6505:; mode4 = 1; goto label_5012; } else { label_6527:; node4____CPAchecker_TMP_2 = p43_new; goto label_6528; } } else { goto label_6527; } } else { goto label_6505; } } else { label_6519:; node4____CPAchecker_TMP_1 = p42_new; goto label_6520; } } else { goto label_6519; } } else { goto label_6515; } } else { label_6511:; node4____CPAchecker_TMP_0 = p41_new; goto label_6512; } } else { goto label_6511; } } else { goto label_6507; } } else { goto label_6505; } } } } else { nl3 = 1; goto label_4976; } } else { goto label_4976; } } else { goto label_4968; } } else { goto label_4968; } } else { goto label_4961; } } else { goto label_4961; } } else { goto label_4954; } } else { goto label_4954; } } else { goto label_4952; } } 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_6544:; p31_new = node3____CPAchecker_TMP_0; label_6539:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_6552:; p32_new = node3____CPAchecker_TMP_1; label_6547:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_6560:; p34_new = node3____CPAchecker_TMP_2; label_6537:; mode3 = 1; goto label_4978; } else { label_6559:; node3____CPAchecker_TMP_2 = p34_new; goto label_6560; } } else { goto label_6559; } } else { goto label_6537; } } else { label_6551:; node3____CPAchecker_TMP_1 = p32_new; goto label_6552; } } else { goto label_6551; } } else { goto label_6547; } } else { label_6543:; node3____CPAchecker_TMP_0 = p31_new; goto label_6544; } } else { goto label_6543; } } else { goto label_6539; } } else { goto label_6537; } } } } else { nl2 = 1; goto label_4942; } } else { goto label_4942; } } else { goto label_4934; } } else { goto label_4934; } } else { goto label_4927; } } else { goto label_4927; } } else { goto label_4920; } } else { goto label_4920; } } else { goto label_4918; } } 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_6576:; p21_new = node2____CPAchecker_TMP_0; label_6571:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_6584:; p23_new = node2____CPAchecker_TMP_1; label_6579:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_6592:; p24_new = node2____CPAchecker_TMP_2; label_6569:; mode2 = 1; goto label_4944; } else { label_6591:; node2____CPAchecker_TMP_2 = p24_new; goto label_6592; } } else { goto label_6591; } } else { goto label_6569; } } else { label_6583:; node2____CPAchecker_TMP_1 = p23_new; goto label_6584; } } else { goto label_6583; } } else { goto label_6579; } } else { label_6575:; node2____CPAchecker_TMP_0 = p21_new; goto label_6576; } } else { goto label_6575; } } else { goto label_6571; } } else { goto label_6569; } } } } else { nl1 = 1; goto label_4908; } } else { goto label_4908; } } else { goto label_4900; } } else { goto label_4900; } } else { goto label_4893; } } else { goto label_4893; } } else { goto label_4886; } } else { goto label_4886; } } else { goto label_4884; } } 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_6608:; p12_new = node1____CPAchecker_TMP_0; label_6603:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_6616:; p13_new = node1____CPAchecker_TMP_1; label_6611:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_6624:; p14_new = node1____CPAchecker_TMP_2; label_6601:; mode1 = 1; goto label_4910; } else { label_6623:; node1____CPAchecker_TMP_2 = p14_new; goto label_6624; } } else { goto label_6623; } } else { goto label_6601; } } else { label_6615:; node1____CPAchecker_TMP_1 = p13_new; goto label_6616; } } else { goto label_6615; } } else { goto label_6611; } } else { label_6607:; node1____CPAchecker_TMP_0 = p12_new; goto label_6608; } } else { goto label_6607; } } else { goto label_6603; } } else { goto label_6601; } } } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6669; } else { check__tmp = 0; goto label_6669; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6663; } else { check__tmp = 0; goto label_6662; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_6656; } else { check__tmp = 0; goto label_6655; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_6649; } else { check__tmp = 0; goto label_6648; } } } else { check__tmp = 0; goto label_6642; } } else { check__tmp = 0; goto label_6638; } } else { check__tmp = 0; goto label_6634; } } else { check__tmp = 0; goto label_6630; } } else { check__tmp = 0; goto label_4869; } } } else { nl4 = 1; goto label_4834; } } else { goto label_4834; } } else { goto label_4826; } } else { goto label_4826; } } else { goto label_4819; } } else { goto label_4819; } } else { goto label_4812; } } else { goto label_4812; } } else { goto label_4810; } } 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_6685:; p41_new = node4____CPAchecker_TMP_0; label_6680:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_6693:; p42_new = node4____CPAchecker_TMP_1; label_6688:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_6701:; p43_new = node4____CPAchecker_TMP_2; label_6678:; mode4 = 1; goto label_4836; } else { label_6700:; node4____CPAchecker_TMP_2 = p43_new; goto label_6701; } } else { goto label_6700; } } else { goto label_6678; } } else { label_6692:; node4____CPAchecker_TMP_1 = p42_new; goto label_6693; } } else { goto label_6692; } } else { goto label_6688; } } else { label_6684:; node4____CPAchecker_TMP_0 = p41_new; goto label_6685; } } else { goto label_6684; } } else { goto label_6680; } } else { goto label_6678; } } } } else { nl3 = 1; goto label_4800; } } else { goto label_4800; } } else { goto label_4792; } } else { goto label_4792; } } else { goto label_4785; } } else { goto label_4785; } } else { goto label_4778; } } else { goto label_4778; } } else { goto label_4776; } } 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_6717:; p31_new = node3____CPAchecker_TMP_0; label_6712:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_6725:; p32_new = node3____CPAchecker_TMP_1; label_6720:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_6733:; p34_new = node3____CPAchecker_TMP_2; label_6710:; mode3 = 1; goto label_4802; } else { label_6732:; node3____CPAchecker_TMP_2 = p34_new; goto label_6733; } } else { goto label_6732; } } else { goto label_6710; } } else { label_6724:; node3____CPAchecker_TMP_1 = p32_new; goto label_6725; } } else { goto label_6724; } } else { goto label_6720; } } else { label_6716:; node3____CPAchecker_TMP_0 = p31_new; goto label_6717; } } else { goto label_6716; } } else { goto label_6712; } } else { goto label_6710; } } } } else { nl2 = 1; goto label_4766; } } else { goto label_4766; } } else { goto label_4758; } } else { goto label_4758; } } else { goto label_4751; } } else { goto label_4751; } } else { goto label_4744; } } else { goto label_4744; } } else { goto label_4742; } } 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_6749:; p21_new = node2____CPAchecker_TMP_0; label_6744:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_6757:; p23_new = node2____CPAchecker_TMP_1; label_6752:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_6765:; p24_new = node2____CPAchecker_TMP_2; label_6742:; mode2 = 1; goto label_4768; } else { label_6764:; node2____CPAchecker_TMP_2 = p24_new; goto label_6765; } } else { goto label_6764; } } else { goto label_6742; } } else { label_6756:; node2____CPAchecker_TMP_1 = p23_new; goto label_6757; } } else { goto label_6756; } } else { goto label_6752; } } else { label_6748:; node2____CPAchecker_TMP_0 = p21_new; goto label_6749; } } else { goto label_6748; } } else { goto label_6744; } } else { goto label_6742; } } } } else { nl1 = 1; goto label_4732; } } else { goto label_4732; } } else { goto label_4724; } } else { goto label_4724; } } else { goto label_4717; } } else { goto label_4717; } } else { goto label_4710; } } else { goto label_4710; } } else { goto label_4708; } } 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_6781:; p12_new = node1____CPAchecker_TMP_0; label_6776:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_6789:; p13_new = node1____CPAchecker_TMP_1; label_6784:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_6797:; p14_new = node1____CPAchecker_TMP_2; label_6774:; mode1 = 1; goto label_4734; } else { label_6796:; node1____CPAchecker_TMP_2 = p14_new; goto label_6797; } } else { goto label_6796; } } else { goto label_6774; } } else { label_6788:; node1____CPAchecker_TMP_1 = p13_new; goto label_6789; } } else { goto label_6788; } } else { goto label_6784; } } else { label_6780:; node1____CPAchecker_TMP_0 = p12_new; goto label_6781; } } else { goto label_6780; } } else { goto label_6776; } } else { goto label_6774; } } } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_6842; } else { check__tmp = 0; goto label_6842; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_6836; } else { check__tmp = 0; goto label_6835; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_6829; } else { check__tmp = 0; goto label_6828; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_6822; } else { check__tmp = 0; goto label_6821; } } } else { check__tmp = 0; goto label_6815; } } else { check__tmp = 0; goto label_6811; } } else { check__tmp = 0; goto label_6807; } } else { check__tmp = 0; goto label_6803; } } else { check__tmp = 0; goto label_4693; } } } else { nl4 = 1; goto label_4658; } } else { goto label_4658; } } else { goto label_4650; } } else { goto label_4650; } } else { goto label_4643; } } else { goto label_4643; } } else { goto label_4636; } } else { goto label_4636; } } else { goto label_4634; } } 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_6858:; p41_new = node4____CPAchecker_TMP_0; label_6853:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_6866:; p42_new = node4____CPAchecker_TMP_1; label_6861:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_6874:; p43_new = node4____CPAchecker_TMP_2; label_6851:; mode4 = 1; goto label_4660; } else { label_6873:; node4____CPAchecker_TMP_2 = p43_new; goto label_6874; } } else { goto label_6873; } } else { goto label_6851; } } else { label_6865:; node4____CPAchecker_TMP_1 = p42_new; goto label_6866; } } else { goto label_6865; } } else { goto label_6861; } } else { label_6857:; node4____CPAchecker_TMP_0 = p41_new; goto label_6858; } } else { goto label_6857; } } else { goto label_6853; } } else { goto label_6851; } } } } else { nl3 = 1; goto label_4624; } } else { goto label_4624; } } 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 { goto label_4600; } } 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_6890:; p31_new = node3____CPAchecker_TMP_0; label_6885:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_6898:; p32_new = node3____CPAchecker_TMP_1; label_6893:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_6906:; p34_new = node3____CPAchecker_TMP_2; label_6883:; mode3 = 1; goto label_4626; } else { label_6905:; node3____CPAchecker_TMP_2 = p34_new; goto label_6906; } } else { goto label_6905; } } else { goto label_6883; } } else { label_6897:; node3____CPAchecker_TMP_1 = p32_new; goto label_6898; } } else { goto label_6897; } } else { goto label_6893; } } else { label_6889:; node3____CPAchecker_TMP_0 = p31_new; goto label_6890; } } else { goto label_6889; } } else { goto label_6885; } } else { goto label_6883; } } } } else { nl2 = 1; goto label_4590; } } else { goto label_4590; } } else { goto label_4582; } } else { goto label_4582; } } else { goto label_4575; } } else { goto label_4575; } } else { goto label_4568; } } else { goto label_4568; } } else { goto label_4566; } } 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_6922:; p21_new = node2____CPAchecker_TMP_0; label_6917:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_6930:; p23_new = node2____CPAchecker_TMP_1; label_6925:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_6938:; p24_new = node2____CPAchecker_TMP_2; label_6915:; mode2 = 1; goto label_4592; } else { label_6937:; node2____CPAchecker_TMP_2 = p24_new; goto label_6938; } } else { goto label_6937; } } else { goto label_6915; } } else { label_6929:; node2____CPAchecker_TMP_1 = p23_new; goto label_6930; } } else { goto label_6929; } } else { goto label_6925; } } else { label_6921:; node2____CPAchecker_TMP_0 = p21_new; goto label_6922; } } else { goto label_6921; } } else { goto label_6917; } } else { goto label_6915; } } } } else { nl1 = 1; goto label_4556; } } else { goto label_4556; } } else { goto label_4548; } } else { goto label_4548; } } else { goto label_4541; } } else { goto label_4541; } } else { goto label_4534; } } else { goto label_4534; } } else { goto label_4532; } } 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_6954:; p12_new = node1____CPAchecker_TMP_0; label_6949:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_6962:; p13_new = node1____CPAchecker_TMP_1; label_6957:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_6970:; p14_new = node1____CPAchecker_TMP_2; label_6947:; mode1 = 1; goto label_4558; } else { label_6969:; node1____CPAchecker_TMP_2 = p14_new; goto label_6970; } } else { goto label_6969; } } else { goto label_6947; } } else { label_6961:; node1____CPAchecker_TMP_1 = p13_new; goto label_6962; } } else { goto label_6961; } } else { goto label_6957; } } else { label_6953:; node1____CPAchecker_TMP_0 = p12_new; goto label_6954; } } else { goto label_6953; } } else { goto label_6949; } } else { goto label_6947; } } } } else { return __return_main; } } else { init__tmp___23 = 0; goto label_7124; } } else { init__tmp___23 = 0; goto label_7120; } } else { init__tmp___23 = 0; goto label_7116; } } else { init__tmp___23 = 0; goto label_7112; } } else { init__tmp___23 = 0; goto label_7108; } } else { init__tmp___23 = 0; goto label_7104; } } else { init__tmp___23 = 0; goto label_7100; } } else { init__tmp___23 = 0; goto label_7096; } } else { init__tmp___23 = 0; goto label_7092; } } else { init__tmp___23 = 0; goto label_7088; } } else { init__tmp___23 = 0; goto label_7084; } } else { init__tmp___23 = 0; goto label_7080; } } else { init__tmp___23 = 0; goto label_7076; } } else { init__tmp___23 = 0; goto label_7072; } } else { init__tmp___23 = 0; goto label_7068; } } else { init__tmp___23 = 0; goto label_7052; } } else { init__tmp___23 = 0; goto label_7053; } } else { init__tmp___23 = 0; goto label_7054; } } else { init__tmp___23 = 0; goto label_7055; } } else { init__tmp___23 = 0; goto label_7056; } } else { init__tmp___23 = 0; goto label_7057; } } else { init__tmp___23 = 0; goto label_7058; } } else { init__tmp___23 = 0; goto label_7059; } } else { init__tmp___23 = 0; goto label_7060; } } else { init__tmp___23 = 0; goto label_7061; } } else { init__tmp___23 = 0; goto label_7062; } } else { init__tmp___23 = 0; goto label_7063; } } else { init__tmp___23 = 0; goto label_7064; } } else { init__tmp___23 = 0; goto label_7024; } } else { init__tmp___23 = 0; goto label_7020; } } else { init__tmp___23 = 0; goto label_7016; } } else { init__tmp___23 = 0; goto label_7012; } } else { init__tmp___23 = 0; goto label_7008; } } else { init__tmp___23 = 0; goto label_7004; } } else { init__tmp___23 = 0; goto label_7000; } } else { init__tmp___23 = 0; goto label_6996; } } else { init__tmp___23 = 0; goto label_6992; } } else { init__tmp___23 = 0; goto label_6988; } } else { init__tmp___23 = 0; goto label_6984; } } else { init__tmp___23 = 0; goto label_6980; } } else { init__tmp___23 = 0; goto label_6976; } } else { init__tmp___23 = 0; goto label_4495; } } else { if (!(init__r412 == 0)) { if (!(ep13 == 0)) { init__tmp___22 = 1; goto label_4490; } else { label_7144:; if (!(init__r422 == 0)) { if (!(ep23 == 0)) { init__tmp___22 = 1; label_7150:; goto label_4490; } else { init__tmp___22 = 0; goto label_7150; } } else { init__tmp___22 = 0; goto label_4490; } } } else { goto label_7144; } } } else { if (!(init__r412 == 0)) { if (!(ep12 == 0)) { init__tmp___21 = 1; goto label_4485; } else { label_7159:; if (!(init__r432 == 0)) { if (!(ep32 == 0)) { init__tmp___21 = 1; label_7165:; goto label_4485; } else { init__tmp___21 = 0; goto label_7165; } } else { init__tmp___21 = 0; goto label_4485; } } } else { goto label_7159; } } } else { if (!(init__r422 == 0)) { if (!(ep21 == 0)) { init__tmp___20 = 1; goto label_4480; } else { label_7174:; if (!(init__r432 == 0)) { if (!(ep31 == 0)) { init__tmp___20 = 1; label_7180:; goto label_4480; } else { init__tmp___20 = 0; goto label_7180; } } else { init__tmp___20 = 0; goto label_4480; } } } else { goto label_7174; } } } else { if (!(init__r312 == 0)) { if (!(ep14 == 0)) { init__tmp___19 = 1; goto label_4475; } else { label_7189:; if (!(init__r322 == 0)) { if (!(ep24 == 0)) { init__tmp___19 = 1; label_7195:; goto label_4475; } else { init__tmp___19 = 0; goto label_7195; } } else { init__tmp___19 = 0; goto label_4475; } } } else { goto label_7189; } } } else { if (!(init__r312 == 0)) { if (!(ep12 == 0)) { init__tmp___18 = 1; goto label_4470; } else { label_7204:; if (!(init__r342 == 0)) { if (!(ep42 == 0)) { init__tmp___18 = 1; label_7210:; goto label_4470; } else { init__tmp___18 = 0; goto label_7210; } } else { init__tmp___18 = 0; goto label_4470; } } } else { goto label_7204; } } } else { if (!(init__r322 == 0)) { if (!(ep21 == 0)) { init__tmp___17 = 1; goto label_4465; } else { label_7219:; if (!(init__r342 == 0)) { if (!(ep41 == 0)) { init__tmp___17 = 1; label_7225:; goto label_4465; } else { init__tmp___17 = 0; goto label_7225; } } else { init__tmp___17 = 0; goto label_4465; } } } else { goto label_7219; } } } else { if (!(init__r212 == 0)) { if (!(ep14 == 0)) { init__tmp___16 = 1; goto label_4460; } else { label_7234:; if (!(init__r232 == 0)) { if (!(ep34 == 0)) { init__tmp___16 = 1; label_7240:; goto label_4460; } else { init__tmp___16 = 0; goto label_7240; } } else { init__tmp___16 = 0; goto label_4460; } } } else { goto label_7234; } } } else { if (!(init__r212 == 0)) { if (!(ep13 == 0)) { init__tmp___15 = 1; goto label_4455; } else { label_7249:; if (!(init__r242 == 0)) { if (!(ep43 == 0)) { init__tmp___15 = 1; label_7255:; goto label_4455; } else { init__tmp___15 = 0; goto label_7255; } } else { init__tmp___15 = 0; goto label_4455; } } } else { goto label_7249; } } } else { if (!(init__r232 == 0)) { if (!(ep31 == 0)) { init__tmp___14 = 1; goto label_4450; } else { label_7264:; if (!(init__r242 == 0)) { if (!(ep41 == 0)) { init__tmp___14 = 1; label_7270:; goto label_4450; } else { init__tmp___14 = 0; goto label_7270; } } else { init__tmp___14 = 0; goto label_4450; } } } else { goto label_7264; } } } else { if (!(init__r122 == 0)) { if (!(ep24 == 0)) { init__tmp___13 = 1; goto label_4445; } else { label_7279:; if (!(init__r132 == 0)) { if (!(ep34 == 0)) { init__tmp___13 = 1; label_7285:; goto label_4445; } else { init__tmp___13 = 0; goto label_7285; } } else { init__tmp___13 = 0; goto label_4445; } } } else { goto label_7279; } } } else { if (!(init__r122 == 0)) { if (!(ep23 == 0)) { init__tmp___12 = 1; goto label_4440; } else { label_7294:; if (!(init__r142 == 0)) { if (!(ep43 == 0)) { init__tmp___12 = 1; label_7300:; goto label_4440; } else { init__tmp___12 = 0; goto label_7300; } } else { init__tmp___12 = 0; goto label_4440; } } } else { goto label_7294; } } } else { if (!(init__r132 == 0)) { if (!(ep32 == 0)) { init__tmp___11 = 1; goto label_4435; } else { label_7309:; if (!(init__r142 == 0)) { if (!(ep42 == 0)) { init__tmp___11 = 1; label_7315:; goto label_4435; } else { init__tmp___11 = 0; goto label_7315; } } else { init__tmp___11 = 0; goto label_4435; } } } else { goto label_7309; } } } else { if (!(init__r411 == 0)) { if (!(ep13 == 0)) { init__tmp___10 = 1; goto label_4430; } else { label_7324:; if (!(init__r421 == 0)) { if (!(ep23 == 0)) { init__tmp___10 = 1; label_7330:; goto label_4430; } else { init__tmp___10 = 0; goto label_7330; } } else { init__tmp___10 = 0; goto label_4430; } } } else { goto label_7324; } } } else { if (!(init__r411 == 0)) { if (!(ep12 == 0)) { init__tmp___9 = 1; goto label_4425; } else { label_7339:; if (!(init__r431 == 0)) { if (!(ep32 == 0)) { init__tmp___9 = 1; label_7345:; goto label_4425; } else { init__tmp___9 = 0; goto label_7345; } } else { init__tmp___9 = 0; goto label_4425; } } } else { goto label_7339; } } } else { if (!(init__r421 == 0)) { if (!(ep21 == 0)) { init__tmp___8 = 1; goto label_4420; } else { label_7354:; if (!(init__r431 == 0)) { if (!(ep31 == 0)) { init__tmp___8 = 1; label_7360:; goto label_4420; } else { init__tmp___8 = 0; goto label_7360; } } else { init__tmp___8 = 0; goto label_4420; } } } else { goto label_7354; } } } else { if (!(init__r311 == 0)) { if (!(ep14 == 0)) { init__tmp___7 = 1; goto label_4415; } else { label_7369:; if (!(init__r321 == 0)) { if (!(ep24 == 0)) { init__tmp___7 = 1; label_7375:; goto label_4415; } else { init__tmp___7 = 0; goto label_7375; } } else { init__tmp___7 = 0; goto label_4415; } } } else { goto label_7369; } } } else { if (!(init__r311 == 0)) { if (!(ep12 == 0)) { init__tmp___6 = 1; goto label_4410; } else { label_7384:; if (!(init__r341 == 0)) { if (!(ep42 == 0)) { init__tmp___6 = 1; label_7390:; goto label_4410; } else { init__tmp___6 = 0; goto label_7390; } } else { init__tmp___6 = 0; goto label_4410; } } } else { goto label_7384; } } } else { if (!(init__r321 == 0)) { if (!(ep21 == 0)) { init__tmp___5 = 1; goto label_4405; } else { label_7399:; if (!(init__r341 == 0)) { if (!(ep41 == 0)) { init__tmp___5 = 1; label_7405:; goto label_4405; } else { init__tmp___5 = 0; goto label_7405; } } else { init__tmp___5 = 0; goto label_4405; } } } else { goto label_7399; } } } else { if (!(init__r211 == 0)) { if (!(ep14 == 0)) { init__tmp___4 = 1; goto label_4400; } else { label_7414:; if (!(init__r231 == 0)) { if (!(ep34 == 0)) { init__tmp___4 = 1; label_7420:; goto label_4400; } else { init__tmp___4 = 0; goto label_7420; } } else { init__tmp___4 = 0; goto label_4400; } } } else { goto label_7414; } } } else { if (!(init__r211 == 0)) { if (!(ep13 == 0)) { init__tmp___3 = 1; goto label_4395; } else { label_7429:; if (!(init__r241 == 0)) { if (!(ep43 == 0)) { init__tmp___3 = 1; label_7435:; goto label_4395; } else { init__tmp___3 = 0; goto label_7435; } } else { init__tmp___3 = 0; goto label_4395; } } } else { goto label_7429; } } } else { if (!(init__r231 == 0)) { if (!(ep31 == 0)) { init__tmp___2 = 1; goto label_4390; } else { label_7444:; if (!(init__r241 == 0)) { if (!(ep41 == 0)) { init__tmp___2 = 1; label_7450:; goto label_4390; } else { init__tmp___2 = 0; goto label_7450; } } else { init__tmp___2 = 0; goto label_4390; } } } else { goto label_7444; } } } else { if (!(init__r121 == 0)) { if (!(ep24 == 0)) { init__tmp___1 = 1; goto label_4385; } else { label_7459:; if (!(init__r131 == 0)) { if (!(ep34 == 0)) { init__tmp___1 = 1; label_7465:; goto label_4385; } else { init__tmp___1 = 0; goto label_7465; } } else { init__tmp___1 = 0; goto label_4385; } } } else { goto label_7459; } } } else { if (!(init__r121 == 0)) { if (!(ep23 == 0)) { init__tmp___0 = 1; goto label_4380; } else { label_7474:; if (!(init__r141 == 0)) { if (!(ep43 == 0)) { init__tmp___0 = 1; label_7480:; goto label_4380; } else { init__tmp___0 = 0; goto label_7480; } } else { init__tmp___0 = 0; goto label_4380; } } } else { goto label_7474; } } } else { if (!(init__r131 == 0)) { if (!(ep32 == 0)) { init__tmp = 1; goto label_4375; } else { label_7489:; if (!(init__r141 == 0)) { if (!(ep42 == 0)) { init__tmp = 1; label_7495:; goto label_4375; } else { init__tmp = 0; goto label_7495; } } else { init__tmp = 0; goto label_4375; } } } else { goto label_7489; } } } }