// This file is part of the SV-Benchmarks collection of verification tasks: // https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks // // SPDX-FileCopyrightText: 2013 Carnegie Mellon University // SPDX-FileCopyrightText: 2014-2021 The SV-Benchmarks Community // SPDX-FileCopyrightText: 2018 Marie-Christine Jakobs, LMU Munich // // SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU-LMU int __return_main; void abort(void); extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); void reach_error() { __assert_fail("0", "pals_floodmax.4.1.ufo.UNBOUNDED.pals.c.v+nlh-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_4268; int __return_4478; int __return_4662; int __return_4850; int __return_5034; int __return_5222; int __return_5415; int __return_5592; 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_4090:; init__r122 = (_Bool)init__tmp; if (!(init__r131 == 0)) { init__tmp___0 = 1; label_4095:; init__r132 = (_Bool)init__tmp___0; if (!(init__r141 == 0)) { init__tmp___1 = 1; label_4100:; init__r142 = (_Bool)init__tmp___1; if (!(init__r211 == 0)) { init__tmp___2 = 1; label_4105:; init__r212 = (_Bool)init__tmp___2; if (!(init__r231 == 0)) { init__tmp___3 = 1; label_4110:; init__r232 = (_Bool)init__tmp___3; if (!(init__r241 == 0)) { init__tmp___4 = 1; label_4115:; init__r242 = (_Bool)init__tmp___4; if (!(init__r311 == 0)) { init__tmp___5 = 1; label_4120:; init__r312 = (_Bool)init__tmp___5; if (!(init__r321 == 0)) { init__tmp___6 = 1; label_4125:; init__r322 = (_Bool)init__tmp___6; if (!(init__r341 == 0)) { init__tmp___7 = 1; label_4130:; init__r342 = (_Bool)init__tmp___7; if (!(init__r411 == 0)) { init__tmp___8 = 1; label_4135:; init__r412 = (_Bool)init__tmp___8; if (!(init__r421 == 0)) { init__tmp___9 = 1; label_4140:; init__r422 = (_Bool)init__tmp___9; if (!(init__r431 == 0)) { init__tmp___10 = 1; label_4145:; init__r432 = (_Bool)init__tmp___10; if (!(init__r122 == 0)) { init__tmp___11 = 1; label_4150:; init__r123 = (_Bool)init__tmp___11; if (!(init__r132 == 0)) { init__tmp___12 = 1; label_4155:; init__r133 = (_Bool)init__tmp___12; if (!(init__r142 == 0)) { init__tmp___13 = 1; label_4160:; init__r143 = (_Bool)init__tmp___13; if (!(init__r212 == 0)) { init__tmp___14 = 1; label_4165:; init__r213 = (_Bool)init__tmp___14; if (!(init__r232 == 0)) { init__tmp___15 = 1; label_4170:; init__r233 = (_Bool)init__tmp___15; if (!(init__r242 == 0)) { init__tmp___16 = 1; label_4175:; init__r243 = (_Bool)init__tmp___16; if (!(init__r312 == 0)) { init__tmp___17 = 1; label_4180:; init__r313 = (_Bool)init__tmp___17; if (!(init__r322 == 0)) { init__tmp___18 = 1; label_4185:; init__r323 = (_Bool)init__tmp___18; if (!(init__r342 == 0)) { init__tmp___19 = 1; label_4190:; init__r343 = (_Bool)init__tmp___19; if (!(init__r412 == 0)) { init__tmp___20 = 1; label_4195:; init__r413 = (_Bool)init__tmp___20; if (!(init__r422 == 0)) { init__tmp___21 = 1; label_4200:; init__r423 = (_Bool)init__tmp___21; if (!(init__r432 == 0)) { init__tmp___22 = 1; label_4205:; init__r433 = (_Bool)init__tmp___22; if (((int)id1) != ((int)id2)) { if (((int)id1) != ((int)id3)) { if (((int)id1) != ((int)id4)) { if (((int)id2) != ((int)id3)) { if (((int)id2) != ((int)id4)) { if (((int)id3) != ((int)id4)) { if (((int)id1) >= 0) { if (((int)id2) >= 0) { if (((int)id3) >= 0) { if (((int)id4) >= 0) { if (((int)r1) == 0) { if (((int)r2) == 0) { if (((int)r3) == 0) { if (((int)r4) == 0) { if (((int)max1) == ((int)id1)) { if (((int)max2) == ((int)id2)) { if (((int)max3) == ((int)id3)) { if (((int)max4) == ((int)id4)) { if (((int)st1) == 0) { if (((int)st2) == 0) { if (((int)st3) == 0) { if (((int)st4) == 0) { if (((int)nl1) == 0) { if (((int)nl2) == 0) { if (((int)nl3) == 0) { if (((int)nl4) == 0) { if (((int)mode1) == 0) { if (((int)mode2) == 0) { if (((int)mode3) == 0) { if (((int)mode4) == 0) { init__tmp___23 = 1; __return_4268 = init__tmp___23; main__i2 = __return_4268; 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_4308:; p12_new = node1____CPAchecker_TMP_0; label_4303:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4316:; p13_new = node1____CPAchecker_TMP_1; label_4311:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4324:; p14_new = node1____CPAchecker_TMP_2; label_4326:; 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_4340:; p21_new = node2____CPAchecker_TMP_0; label_4335:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4348:; p23_new = node2____CPAchecker_TMP_1; label_4343:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4356:; p24_new = node2____CPAchecker_TMP_2; label_4358:; 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_4372:; p31_new = node3____CPAchecker_TMP_0; label_4367:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4380:; p32_new = node3____CPAchecker_TMP_1; label_4375:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4388:; p34_new = node3____CPAchecker_TMP_2; label_4390:; 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_4404:; p41_new = node4____CPAchecker_TMP_0; label_4399:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4412:; p42_new = node4____CPAchecker_TMP_1; label_4407:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4420:; p43_new = node4____CPAchecker_TMP_2; label_4422:; 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_4478 = check__tmp; main__c1 = __return_4478; { _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_4492:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4499:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4506:; 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_4523:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4530:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4537:; 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_4554:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4561:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4568:; 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_4585:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4592:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4599:; 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_4662 = check__tmp; main__c1 = __return_4662; { _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_4680:; p12_new = node1____CPAchecker_TMP_0; label_4675:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_4688:; p13_new = node1____CPAchecker_TMP_1; label_4683:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_4696:; p14_new = node1____CPAchecker_TMP_2; label_4698:; 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_4712:; p21_new = node2____CPAchecker_TMP_0; label_4707:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_4720:; p23_new = node2____CPAchecker_TMP_1; label_4715:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_4728:; p24_new = node2____CPAchecker_TMP_2; label_4730:; 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_4744:; p31_new = node3____CPAchecker_TMP_0; label_4739:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_4752:; p32_new = node3____CPAchecker_TMP_1; label_4747:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_4760:; p34_new = node3____CPAchecker_TMP_2; label_4762:; 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_4776:; p41_new = node4____CPAchecker_TMP_0; label_4771:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_4784:; p42_new = node4____CPAchecker_TMP_1; label_4779:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_4792:; p43_new = node4____CPAchecker_TMP_2; label_4794:; 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_4850 = check__tmp; main__c1 = __return_4850; { _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_4864:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4871:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_4878:; 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_4895:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4902:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_4909:; 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_4926:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4933:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_4940:; 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_4957:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4964:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4971:; 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_5034 = check__tmp; main__c1 = __return_5034; { _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_5052:; p12_new = node1____CPAchecker_TMP_0; label_5047:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5060:; p13_new = node1____CPAchecker_TMP_1; label_5055:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5068:; p14_new = node1____CPAchecker_TMP_2; label_5070:; 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_5084:; p21_new = node2____CPAchecker_TMP_0; label_5079:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5092:; p23_new = node2____CPAchecker_TMP_1; label_5087:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5100:; p24_new = node2____CPAchecker_TMP_2; label_5102:; 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_5116:; p31_new = node3____CPAchecker_TMP_0; label_5111:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5124:; p32_new = node3____CPAchecker_TMP_1; label_5119:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5132:; p34_new = node3____CPAchecker_TMP_2; label_5134:; 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_5148:; p41_new = node4____CPAchecker_TMP_0; label_5143:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5156:; p42_new = node4____CPAchecker_TMP_1; label_5151:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5164:; p43_new = node4____CPAchecker_TMP_2; label_5166:; 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_5222 = check__tmp; main__c1 = __return_5222; { _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_5236:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5243:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5250:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5261:; 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_5271:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5278:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5285:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5296:; 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_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_5331:; 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_5341:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5348:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5355:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5366:; 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_5777:; if (((int)r1) < 3) { check__tmp = 1; label_5783:; label_5776:; label_5408:; label_5414:; __return_5415 = check__tmp; main__c1 = __return_5415; label_5416:; { _Bool __tmp_6; __tmp_6 = main__c1; _Bool assert__arg; assert__arg = __tmp_6; if (assert__arg == 0) { {reach_error();} return __return_main; } else { { if (!(mode1 == 0)) { if (r1 == 255) { r1 = 3; label_5430:; r1 = r1 + 1; if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5432:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5439:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_5446:; if (((int)r1) == 3) { if (((int)max1) == ((int)id1)) { st1 = 1; label_5454:; mode1 = 0; label_5456:; { if (!(mode2 == 0)) { if (r2 == 255) { r2 = 3; label_5464:; r2 = r2 + 1; if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5466:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5473:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_5480:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_5488:; mode2 = 0; label_5490:; { if (!(mode3 == 0)) { if (r3 == 255) { r3 = 3; label_5498:; r3 = r3 + 1; if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5500:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5507:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_5514:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_5522:; mode3 = 0; label_5524:; { if (!(mode4 == 0)) { if (r4 == 255) { r4 = 3; label_5532:; r4 = r4 + 1; if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5534:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5541:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_5548:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_5556:; mode4 = 0; label_5558:; 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_5615:; if (((int)r1) < 3) { label_5622:; if (((int)r1) >= 3) { label_5629:; if (((int)r1) < 3) { check__tmp = 1; label_5635:; label_5628:; label_5621:; label_5614:; label_5608:; label_5604:; label_5600:; label_5596:; label_5591:; __return_5592 = check__tmp; main__c1 = __return_5592; goto label_5416; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5635; } else { check__tmp = 0; goto label_5635; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5629; } else { check__tmp = 0; goto label_5628; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_5622; } else { check__tmp = 0; goto label_5621; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_5615; } else { check__tmp = 0; goto label_5614; } } } else { check__tmp = 0; goto label_5608; } } else { check__tmp = 0; goto label_5604; } } else { check__tmp = 0; goto label_5600; } } else { check__tmp = 0; goto label_5596; } } else { check__tmp = 0; goto label_5591; } } } else { nl4 = 1; goto label_5556; } } else { goto label_5556; } } else { goto label_5548; } } else { goto label_5548; } } else { goto label_5541; } } else { goto label_5541; } } else { goto label_5534; } } else { goto label_5534; } } else { goto label_5532; } } 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_5651:; p41_new = node4____CPAchecker_TMP_0; label_5646:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_5659:; p42_new = node4____CPAchecker_TMP_1; label_5654:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_5667:; p43_new = node4____CPAchecker_TMP_2; label_5644:; mode4 = 1; goto label_5558; } else { label_5666:; node4____CPAchecker_TMP_2 = p43_new; goto label_5667; } } else { goto label_5666; } } else { goto label_5644; } } else { label_5658:; node4____CPAchecker_TMP_1 = p42_new; goto label_5659; } } else { goto label_5658; } } else { goto label_5654; } } else { label_5650:; node4____CPAchecker_TMP_0 = p41_new; goto label_5651; } } else { goto label_5650; } } else { goto label_5646; } } else { goto label_5644; } } } } else { nl3 = 1; goto label_5522; } } else { goto label_5522; } } else { goto label_5514; } } else { goto label_5514; } } else { goto label_5507; } } else { goto label_5507; } } else { goto label_5500; } } else { goto label_5500; } } else { goto label_5498; } } 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_5683:; p31_new = node3____CPAchecker_TMP_0; label_5678:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_5691:; p32_new = node3____CPAchecker_TMP_1; label_5686:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_5699:; p34_new = node3____CPAchecker_TMP_2; label_5676:; mode3 = 1; goto label_5524; } else { label_5698:; node3____CPAchecker_TMP_2 = p34_new; goto label_5699; } } else { goto label_5698; } } else { goto label_5676; } } else { label_5690:; node3____CPAchecker_TMP_1 = p32_new; goto label_5691; } } else { goto label_5690; } } else { goto label_5686; } } else { label_5682:; node3____CPAchecker_TMP_0 = p31_new; goto label_5683; } } else { goto label_5682; } } else { goto label_5678; } } else { goto label_5676; } } } } else { nl2 = 1; goto label_5488; } } else { goto label_5488; } } else { goto label_5480; } } else { goto label_5480; } } else { goto label_5473; } } else { goto label_5473; } } else { goto label_5466; } } else { goto label_5466; } } else { goto label_5464; } } 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_5715:; p21_new = node2____CPAchecker_TMP_0; label_5710:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_5723:; p23_new = node2____CPAchecker_TMP_1; label_5718:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_5731:; p24_new = node2____CPAchecker_TMP_2; label_5708:; mode2 = 1; goto label_5490; } else { label_5730:; node2____CPAchecker_TMP_2 = p24_new; goto label_5731; } } else { goto label_5730; } } else { goto label_5708; } } else { label_5722:; node2____CPAchecker_TMP_1 = p23_new; goto label_5723; } } else { goto label_5722; } } else { goto label_5718; } } else { label_5714:; node2____CPAchecker_TMP_0 = p21_new; goto label_5715; } } else { goto label_5714; } } else { goto label_5710; } } else { goto label_5708; } } } } else { nl1 = 1; goto label_5454; } } else { goto label_5454; } } else { goto label_5446; } } else { goto label_5446; } } else { goto label_5439; } } else { goto label_5439; } } else { goto label_5432; } } else { goto label_5432; } } else { goto label_5430; } } 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_5747:; p12_new = node1____CPAchecker_TMP_0; label_5742:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_5755:; p13_new = node1____CPAchecker_TMP_1; label_5750:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_5763:; p14_new = node1____CPAchecker_TMP_2; label_5740:; mode1 = 1; goto label_5456; } else { label_5762:; node1____CPAchecker_TMP_2 = p14_new; goto label_5763; } } else { goto label_5762; } } else { goto label_5740; } } else { label_5754:; node1____CPAchecker_TMP_1 = p13_new; goto label_5755; } } else { goto label_5754; } } else { goto label_5750; } } else { label_5746:; node1____CPAchecker_TMP_0 = p12_new; goto label_5747; } } else { goto label_5746; } } else { goto label_5742; } } else { goto label_5740; } } } } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_5783; } else { check__tmp = 0; goto label_5783; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_5777; } else { check__tmp = 0; goto label_5776; } } } else { check__tmp = 0; goto label_5408; } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { check__tmp = 0; goto label_5414; } } } else { nl4 = 1; goto label_5366; } } else { return __return_main; } } else { goto label_5355; } } else { goto label_5355; } } else { goto label_5348; } } else { goto label_5348; } } else { goto label_5341; } } else { goto label_5341; } } } else { return __return_main; } } } else { nl3 = 1; goto label_5331; } } else { return __return_main; } } 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 { return __return_main; } } } else { nl2 = 1; goto label_5296; } } else { return __return_main; } } else { goto label_5285; } } else { goto label_5285; } } else { goto label_5278; } } else { goto label_5278; } } else { goto label_5271; } } else { goto label_5271; } } } else { return __return_main; } } } else { nl1 = 1; goto label_5261; } } else { return __return_main; } } else { goto label_5250; } } else { goto label_5250; } } else { goto label_5243; } } else { goto label_5243; } } else { goto label_5236; } } else { goto label_5236; } } } else { return __return_main; } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_5163:; node4____CPAchecker_TMP_2 = p43_new; goto label_5164; } } else { goto label_5163; } } else { goto label_5166; } } else { label_5155:; node4____CPAchecker_TMP_1 = p42_new; goto label_5156; } } else { goto label_5155; } } else { goto label_5151; } } else { label_5147:; node4____CPAchecker_TMP_0 = p41_new; goto label_5148; } } else { goto label_5147; } } else { goto label_5143; } } else { return __return_main; } } } } else { label_5131:; node3____CPAchecker_TMP_2 = p34_new; goto label_5132; } } else { goto label_5131; } } else { goto label_5134; } } else { label_5123:; node3____CPAchecker_TMP_1 = p32_new; goto label_5124; } } else { goto label_5123; } } else { goto label_5119; } } else { label_5115:; node3____CPAchecker_TMP_0 = p31_new; goto label_5116; } } else { goto label_5115; } } else { goto label_5111; } } else { return __return_main; } } } } else { label_5099:; node2____CPAchecker_TMP_2 = p24_new; goto label_5100; } } else { goto label_5099; } } else { goto label_5102; } } else { label_5091:; node2____CPAchecker_TMP_1 = p23_new; goto label_5092; } } else { goto label_5091; } } else { goto label_5087; } } else { label_5083:; node2____CPAchecker_TMP_0 = p21_new; goto label_5084; } } else { goto label_5083; } } else { goto label_5079; } } else { return __return_main; } } } } else { label_5067:; node1____CPAchecker_TMP_2 = p14_new; goto label_5068; } } else { goto label_5067; } } else { goto label_5070; } } else { label_5059:; node1____CPAchecker_TMP_1 = p13_new; goto label_5060; } } else { goto label_5059; } } else { goto label_5055; } } else { label_5051:; node1____CPAchecker_TMP_0 = p12_new; goto label_5052; } } else { goto label_5051; } } else { goto label_5047; } } else { return __return_main; } } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4971; } } else { goto label_4971; } } else { goto label_4964; } } else { goto label_4964; } } else { goto label_4957; } } else { goto label_4957; } } } else { return __return_main; } } } } else { goto label_4940; } } else { goto label_4940; } } else { goto label_4933; } } else { goto label_4933; } } else { goto label_4926; } } else { goto label_4926; } } } else { return __return_main; } } } } else { goto label_4909; } } else { goto label_4909; } } else { goto label_4902; } } else { goto label_4902; } } else { goto label_4895; } } else { goto label_4895; } } } else { return __return_main; } } } } else { goto label_4878; } } else { goto label_4878; } } else { goto label_4871; } } else { goto label_4871; } } else { goto label_4864; } } else { goto label_4864; } } } else { return __return_main; } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4791:; node4____CPAchecker_TMP_2 = p43_new; goto label_4792; } } else { goto label_4791; } } else { goto label_4794; } } else { label_4783:; node4____CPAchecker_TMP_1 = p42_new; goto label_4784; } } else { goto label_4783; } } else { goto label_4779; } } else { label_4775:; node4____CPAchecker_TMP_0 = p41_new; goto label_4776; } } else { goto label_4775; } } else { goto label_4771; } } else { return __return_main; } } } } else { label_4759:; node3____CPAchecker_TMP_2 = p34_new; goto label_4760; } } else { goto label_4759; } } else { goto label_4762; } } else { label_4751:; node3____CPAchecker_TMP_1 = p32_new; goto label_4752; } } else { goto label_4751; } } else { goto label_4747; } } else { label_4743:; node3____CPAchecker_TMP_0 = p31_new; goto label_4744; } } else { goto label_4743; } } else { goto label_4739; } } else { return __return_main; } } } } else { label_4727:; node2____CPAchecker_TMP_2 = p24_new; goto label_4728; } } else { goto label_4727; } } else { goto label_4730; } } else { label_4719:; node2____CPAchecker_TMP_1 = p23_new; goto label_4720; } } else { goto label_4719; } } else { goto label_4715; } } else { label_4711:; node2____CPAchecker_TMP_0 = p21_new; goto label_4712; } } else { goto label_4711; } } else { goto label_4707; } } else { return __return_main; } } } } else { label_4695:; node1____CPAchecker_TMP_2 = p14_new; goto label_4696; } } else { goto label_4695; } } else { goto label_4698; } } else { label_4687:; node1____CPAchecker_TMP_1 = p13_new; goto label_4688; } } else { goto label_4687; } } else { goto label_4683; } } else { label_4679:; node1____CPAchecker_TMP_0 = p12_new; goto label_4680; } } else { goto label_4679; } } else { goto label_4675; } } else { return __return_main; } } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4599; } } else { goto label_4599; } } else { goto label_4592; } } else { goto label_4592; } } else { goto label_4585; } } else { goto label_4585; } } } else { return __return_main; } } } } else { goto label_4568; } } else { goto label_4568; } } else { goto label_4561; } } else { goto label_4561; } } else { goto label_4554; } } else { goto label_4554; } } } else { return __return_main; } } } } else { goto label_4537; } } else { goto label_4537; } } else { goto label_4530; } } else { goto label_4530; } } else { goto label_4523; } } else { goto label_4523; } } } else { return __return_main; } } } } else { goto label_4506; } } else { goto label_4506; } } else { goto label_4499; } } else { goto label_4499; } } else { goto label_4492; } } else { goto label_4492; } } } else { return __return_main; } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { 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_4419:; node4____CPAchecker_TMP_2 = p43_new; goto label_4420; } } else { goto label_4419; } } else { goto label_4422; } } else { label_4411:; node4____CPAchecker_TMP_1 = p42_new; goto label_4412; } } else { goto label_4411; } } else { goto label_4407; } } else { label_4403:; node4____CPAchecker_TMP_0 = p41_new; goto label_4404; } } else { goto label_4403; } } else { goto label_4399; } } else { return __return_main; } } } } else { label_4387:; node3____CPAchecker_TMP_2 = p34_new; goto label_4388; } } else { goto label_4387; } } else { goto label_4390; } } else { label_4379:; node3____CPAchecker_TMP_1 = p32_new; goto label_4380; } } else { goto label_4379; } } else { goto label_4375; } } else { label_4371:; node3____CPAchecker_TMP_0 = p31_new; goto label_4372; } } else { goto label_4371; } } else { goto label_4367; } } else { return __return_main; } } } } else { label_4355:; node2____CPAchecker_TMP_2 = p24_new; goto label_4356; } } else { goto label_4355; } } else { goto label_4358; } } else { label_4347:; node2____CPAchecker_TMP_1 = p23_new; goto label_4348; } } else { goto label_4347; } } else { goto label_4343; } } else { label_4339:; node2____CPAchecker_TMP_0 = p21_new; goto label_4340; } } else { goto label_4339; } } else { goto label_4335; } } else { return __return_main; } } } } else { label_4323:; node1____CPAchecker_TMP_2 = p14_new; goto label_4324; } } else { goto label_4323; } } else { goto label_4326; } } else { label_4315:; node1____CPAchecker_TMP_1 = p13_new; goto label_4316; } } else { goto label_4315; } } else { goto label_4311; } } else { label_4307:; node1____CPAchecker_TMP_0 = p12_new; goto label_4308; } } else { goto label_4307; } } else { goto label_4303; } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { 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_4205; } else { label_5809:; if (!(init__r422 == 0)) { if (!(ep23 == 0)) { init__tmp___22 = 1; label_5815:; goto label_4205; } else { init__tmp___22 = 0; goto label_5815; } } else { init__tmp___22 = 0; goto label_4205; } } } else { goto label_5809; } } } else { if (!(init__r412 == 0)) { if (!(ep12 == 0)) { init__tmp___21 = 1; goto label_4200; } else { label_5824:; if (!(init__r432 == 0)) { if (!(ep32 == 0)) { init__tmp___21 = 1; label_5830:; goto label_4200; } else { init__tmp___21 = 0; goto label_5830; } } else { init__tmp___21 = 0; goto label_4200; } } } else { goto label_5824; } } } else { if (!(init__r422 == 0)) { if (!(ep21 == 0)) { init__tmp___20 = 1; goto label_4195; } else { label_5839:; if (!(init__r432 == 0)) { if (!(ep31 == 0)) { init__tmp___20 = 1; label_5845:; goto label_4195; } else { init__tmp___20 = 0; goto label_5845; } } else { init__tmp___20 = 0; goto label_4195; } } } else { goto label_5839; } } } else { if (!(init__r312 == 0)) { if (!(ep14 == 0)) { init__tmp___19 = 1; goto label_4190; } else { label_5854:; if (!(init__r322 == 0)) { if (!(ep24 == 0)) { init__tmp___19 = 1; label_5860:; goto label_4190; } else { init__tmp___19 = 0; goto label_5860; } } else { init__tmp___19 = 0; goto label_4190; } } } else { goto label_5854; } } } else { if (!(init__r312 == 0)) { if (!(ep12 == 0)) { init__tmp___18 = 1; goto label_4185; } else { label_5869:; if (!(init__r342 == 0)) { if (!(ep42 == 0)) { init__tmp___18 = 1; label_5875:; goto label_4185; } else { init__tmp___18 = 0; goto label_5875; } } else { init__tmp___18 = 0; goto label_4185; } } } else { goto label_5869; } } } else { if (!(init__r322 == 0)) { if (!(ep21 == 0)) { init__tmp___17 = 1; goto label_4180; } else { label_5884:; if (!(init__r342 == 0)) { if (!(ep41 == 0)) { init__tmp___17 = 1; label_5890:; goto label_4180; } else { init__tmp___17 = 0; goto label_5890; } } else { init__tmp___17 = 0; goto label_4180; } } } else { goto label_5884; } } } else { if (!(init__r212 == 0)) { if (!(ep14 == 0)) { init__tmp___16 = 1; goto label_4175; } else { label_5899:; if (!(init__r232 == 0)) { if (!(ep34 == 0)) { init__tmp___16 = 1; label_5905:; goto label_4175; } else { init__tmp___16 = 0; goto label_5905; } } else { init__tmp___16 = 0; goto label_4175; } } } else { goto label_5899; } } } else { if (!(init__r212 == 0)) { if (!(ep13 == 0)) { init__tmp___15 = 1; goto label_4170; } else { label_5914:; if (!(init__r242 == 0)) { if (!(ep43 == 0)) { init__tmp___15 = 1; label_5920:; goto label_4170; } else { init__tmp___15 = 0; goto label_5920; } } else { init__tmp___15 = 0; goto label_4170; } } } else { goto label_5914; } } } else { if (!(init__r232 == 0)) { if (!(ep31 == 0)) { init__tmp___14 = 1; goto label_4165; } else { label_5929:; if (!(init__r242 == 0)) { if (!(ep41 == 0)) { init__tmp___14 = 1; label_5935:; goto label_4165; } else { init__tmp___14 = 0; goto label_5935; } } else { init__tmp___14 = 0; goto label_4165; } } } else { goto label_5929; } } } else { if (!(init__r122 == 0)) { if (!(ep24 == 0)) { init__tmp___13 = 1; goto label_4160; } else { label_5944:; if (!(init__r132 == 0)) { if (!(ep34 == 0)) { init__tmp___13 = 1; label_5950:; goto label_4160; } else { init__tmp___13 = 0; goto label_5950; } } else { init__tmp___13 = 0; goto label_4160; } } } else { goto label_5944; } } } else { if (!(init__r122 == 0)) { if (!(ep23 == 0)) { init__tmp___12 = 1; goto label_4155; } else { label_5959:; if (!(init__r142 == 0)) { if (!(ep43 == 0)) { init__tmp___12 = 1; label_5965:; goto label_4155; } else { init__tmp___12 = 0; goto label_5965; } } else { init__tmp___12 = 0; goto label_4155; } } } else { goto label_5959; } } } else { if (!(init__r132 == 0)) { if (!(ep32 == 0)) { init__tmp___11 = 1; goto label_4150; } else { label_5974:; if (!(init__r142 == 0)) { if (!(ep42 == 0)) { init__tmp___11 = 1; label_5980:; goto label_4150; } else { init__tmp___11 = 0; goto label_5980; } } else { init__tmp___11 = 0; goto label_4150; } } } else { goto label_5974; } } } else { if (!(init__r411 == 0)) { if (!(ep13 == 0)) { init__tmp___10 = 1; goto label_4145; } else { label_5989:; if (!(init__r421 == 0)) { if (!(ep23 == 0)) { init__tmp___10 = 1; label_5995:; goto label_4145; } else { init__tmp___10 = 0; goto label_5995; } } else { init__tmp___10 = 0; goto label_4145; } } } else { goto label_5989; } } } else { if (!(init__r411 == 0)) { if (!(ep12 == 0)) { init__tmp___9 = 1; goto label_4140; } else { label_6004:; if (!(init__r431 == 0)) { if (!(ep32 == 0)) { init__tmp___9 = 1; label_6010:; goto label_4140; } else { init__tmp___9 = 0; goto label_6010; } } else { init__tmp___9 = 0; goto label_4140; } } } else { goto label_6004; } } } else { if (!(init__r421 == 0)) { if (!(ep21 == 0)) { init__tmp___8 = 1; goto label_4135; } else { label_6019:; if (!(init__r431 == 0)) { if (!(ep31 == 0)) { init__tmp___8 = 1; label_6025:; goto label_4135; } else { init__tmp___8 = 0; goto label_6025; } } else { init__tmp___8 = 0; goto label_4135; } } } else { goto label_6019; } } } else { if (!(init__r311 == 0)) { if (!(ep14 == 0)) { init__tmp___7 = 1; goto label_4130; } else { label_6034:; if (!(init__r321 == 0)) { if (!(ep24 == 0)) { init__tmp___7 = 1; label_6040:; goto label_4130; } else { init__tmp___7 = 0; goto label_6040; } } else { init__tmp___7 = 0; goto label_4130; } } } else { goto label_6034; } } } else { if (!(init__r311 == 0)) { if (!(ep12 == 0)) { init__tmp___6 = 1; goto label_4125; } else { label_6049:; if (!(init__r341 == 0)) { if (!(ep42 == 0)) { init__tmp___6 = 1; label_6055:; goto label_4125; } else { init__tmp___6 = 0; goto label_6055; } } else { init__tmp___6 = 0; goto label_4125; } } } else { goto label_6049; } } } else { if (!(init__r321 == 0)) { if (!(ep21 == 0)) { init__tmp___5 = 1; goto label_4120; } else { label_6064:; if (!(init__r341 == 0)) { if (!(ep41 == 0)) { init__tmp___5 = 1; label_6070:; goto label_4120; } else { init__tmp___5 = 0; goto label_6070; } } else { init__tmp___5 = 0; goto label_4120; } } } else { goto label_6064; } } } else { if (!(init__r211 == 0)) { if (!(ep14 == 0)) { init__tmp___4 = 1; goto label_4115; } else { label_6079:; if (!(init__r231 == 0)) { if (!(ep34 == 0)) { init__tmp___4 = 1; label_6085:; goto label_4115; } else { init__tmp___4 = 0; goto label_6085; } } else { init__tmp___4 = 0; goto label_4115; } } } else { goto label_6079; } } } else { if (!(init__r211 == 0)) { if (!(ep13 == 0)) { init__tmp___3 = 1; goto label_4110; } else { label_6094:; if (!(init__r241 == 0)) { if (!(ep43 == 0)) { init__tmp___3 = 1; label_6100:; goto label_4110; } else { init__tmp___3 = 0; goto label_6100; } } else { init__tmp___3 = 0; goto label_4110; } } } else { goto label_6094; } } } else { if (!(init__r231 == 0)) { if (!(ep31 == 0)) { init__tmp___2 = 1; goto label_4105; } else { label_6109:; if (!(init__r241 == 0)) { if (!(ep41 == 0)) { init__tmp___2 = 1; label_6115:; goto label_4105; } else { init__tmp___2 = 0; goto label_6115; } } else { init__tmp___2 = 0; goto label_4105; } } } else { goto label_6109; } } } else { if (!(init__r121 == 0)) { if (!(ep24 == 0)) { init__tmp___1 = 1; goto label_4100; } else { label_6124:; if (!(init__r131 == 0)) { if (!(ep34 == 0)) { init__tmp___1 = 1; label_6130:; goto label_4100; } else { init__tmp___1 = 0; goto label_6130; } } else { init__tmp___1 = 0; goto label_4100; } } } else { goto label_6124; } } } else { if (!(init__r121 == 0)) { if (!(ep23 == 0)) { init__tmp___0 = 1; goto label_4095; } else { label_6139:; if (!(init__r141 == 0)) { if (!(ep43 == 0)) { init__tmp___0 = 1; label_6145:; goto label_4095; } else { init__tmp___0 = 0; goto label_6145; } } else { init__tmp___0 = 0; goto label_4095; } } } else { goto label_6139; } } } else { if (!(init__r131 == 0)) { if (!(ep32 == 0)) { init__tmp = 1; goto label_4090; } else { label_6154:; if (!(init__r141 == 0)) { if (!(ep42 == 0)) { init__tmp = 1; label_6160:; goto label_4090; } else { init__tmp = 0; goto label_6160; } } else { init__tmp = 0; goto label_4090; } } } else { goto label_6154; } } } }