// 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.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c", 4, "reach_error"); } char __VERIFIER_nondet_char(); _Bool __VERIFIER_nondet_bool(); void assert(_Bool arg); void abort(void); void assume_abort_if_not(int cond) { if(!cond) {abort();} } typedef char msg_t; typedef int port_t; void read(port_t p, msg_t m); void write(port_t p, msg_t m); msg_t nomsg = (msg_t )-1; port_t p12 = 0; char p12_old = '\x0'; char p12_new = '\x0'; _Bool ep12 = 0; port_t p13 = 0; char p13_old = '\x0'; char p13_new = '\x0'; _Bool ep13 = 0; port_t p14 = 0; char p14_old = '\x0'; char p14_new = '\x0'; _Bool ep14 = 0; port_t p21 = 0; char p21_old = '\x0'; char p21_new = '\x0'; _Bool ep21 = 0; port_t p23 = 0; char p23_old = '\x0'; char p23_new = '\x0'; _Bool ep23 = 0; port_t p24 = 0; char p24_old = '\x0'; char p24_new = '\x0'; _Bool ep24 = 0; port_t p31 = 0; char p31_old = '\x0'; char p31_new = '\x0'; _Bool ep31 = 0; port_t p32 = 0; char p32_old = '\x0'; char p32_new = '\x0'; _Bool ep32 = 0; port_t p34 = 0; char p34_old = '\x0'; char p34_new = '\x0'; _Bool ep34 = 0; port_t p41 = 0; char p41_old = '\x0'; char p41_new = '\x0'; _Bool ep41 = 0; port_t p42 = 0; char p42_old = '\x0'; char p42_new = '\x0'; _Bool ep42 = 0; port_t p43 = 0; char p43_old = '\x0'; char p43_new = '\x0'; _Bool ep43 = 0; char id1 = '\x0'; char r1 = '\x0'; char st1 = '\x0'; char nl1 = '\x0'; char m1 = '\x0'; char max1 = '\x0'; _Bool mode1 = 0; char id2 = '\x0'; char r2 = '\x0'; char st2 = '\x0'; char nl2 = '\x0'; char m2 = '\x0'; char max2 = '\x0'; _Bool mode2 = 0; char id3 = '\x0'; char r3 = '\x0'; char st3 = '\x0'; char nl3 = '\x0'; char m3 = '\x0'; char max3 = '\x0'; _Bool mode3 = 0; char id4 = '\x0'; char r4 = '\x0'; char st4 = '\x0'; char nl4 = '\x0'; char m4 = '\x0'; char max4 = '\x0'; _Bool mode4 = 0; void node1(); void node2(); void node3(); void node4(); void (*nodes[4])() = { &node1, &node2, &node3, &node4 }; int init(); int check(); int main(); int __return_2814; int __return_3024; int __return_3207; int __return_3398; int __return_4065; int __return_3582; int __tmp_3583_0; int __return_3756; int __return_3596; int main() { int main__c1; int main__i2; main__c1 = 0; ep12 = __VERIFIER_nondet_bool(); ep13 = __VERIFIER_nondet_bool(); ep14 = __VERIFIER_nondet_bool(); ep21 = __VERIFIER_nondet_bool(); ep23 = __VERIFIER_nondet_bool(); ep24 = __VERIFIER_nondet_bool(); ep31 = __VERIFIER_nondet_bool(); ep32 = __VERIFIER_nondet_bool(); ep34 = __VERIFIER_nondet_bool(); ep41 = __VERIFIER_nondet_bool(); ep42 = __VERIFIER_nondet_bool(); ep43 = __VERIFIER_nondet_bool(); id1 = __VERIFIER_nondet_char(); r1 = __VERIFIER_nondet_char(); st1 = __VERIFIER_nondet_char(); nl1 = __VERIFIER_nondet_char(); m1 = __VERIFIER_nondet_char(); max1 = __VERIFIER_nondet_char(); mode1 = __VERIFIER_nondet_bool(); id2 = __VERIFIER_nondet_char(); r2 = __VERIFIER_nondet_char(); st2 = __VERIFIER_nondet_char(); nl2 = __VERIFIER_nondet_char(); m2 = __VERIFIER_nondet_char(); max2 = __VERIFIER_nondet_char(); mode2 = __VERIFIER_nondet_bool(); id3 = __VERIFIER_nondet_char(); r3 = __VERIFIER_nondet_char(); st3 = __VERIFIER_nondet_char(); nl3 = __VERIFIER_nondet_char(); m3 = __VERIFIER_nondet_char(); max3 = __VERIFIER_nondet_char(); mode3 = __VERIFIER_nondet_bool(); id4 = __VERIFIER_nondet_char(); r4 = __VERIFIER_nondet_char(); st4 = __VERIFIER_nondet_char(); nl4 = __VERIFIER_nondet_char(); m4 = __VERIFIER_nondet_char(); max4 = __VERIFIER_nondet_char(); mode4 = __VERIFIER_nondet_bool(); { _Bool init__r121; _Bool init__r131; _Bool init__r141; _Bool init__r211; _Bool init__r231; _Bool init__r241; _Bool init__r311; _Bool init__r321; _Bool init__r341; _Bool init__r411; _Bool init__r421; _Bool init__r431; _Bool init__r122; int init__tmp; _Bool init__r132; int init__tmp___0; _Bool init__r142; int init__tmp___1; _Bool init__r212; int init__tmp___2; _Bool init__r232; int init__tmp___3; _Bool init__r242; int init__tmp___4; _Bool init__r312; int init__tmp___5; _Bool init__r322; int init__tmp___6; _Bool init__r342; int init__tmp___7; _Bool init__r412; int init__tmp___8; _Bool init__r422; int init__tmp___9; _Bool init__r432; int init__tmp___10; _Bool init__r123; int init__tmp___11; _Bool init__r133; int init__tmp___12; _Bool init__r143; int init__tmp___13; _Bool init__r213; int init__tmp___14; _Bool init__r233; int init__tmp___15; _Bool init__r243; int init__tmp___16; _Bool init__r313; int init__tmp___17; _Bool init__r323; int init__tmp___18; _Bool init__r343; int init__tmp___19; _Bool init__r413; int init__tmp___20; _Bool init__r423; int init__tmp___21; _Bool init__r433; int init__tmp___22; int init__tmp___23; init__r121 = ep12; init__r131 = ep13; init__r141 = ep14; init__r211 = ep21; init__r231 = ep23; init__r241 = ep24; init__r311 = ep31; init__r321 = ep32; init__r341 = ep34; init__r411 = ep41; init__r421 = ep42; init__r431 = ep43; if (!(init__r121 == 0)) { init__tmp = 1; label_2612:; init__r122 = (_Bool)init__tmp; if (!(init__r131 == 0)) { init__tmp___0 = 1; label_2617:; init__r132 = (_Bool)init__tmp___0; if (!(init__r141 == 0)) { init__tmp___1 = 1; label_2622:; init__r142 = (_Bool)init__tmp___1; if (!(init__r211 == 0)) { init__tmp___2 = 1; label_2627:; init__r212 = (_Bool)init__tmp___2; if (!(init__r231 == 0)) { init__tmp___3 = 1; label_2632:; init__r232 = (_Bool)init__tmp___3; if (!(init__r241 == 0)) { init__tmp___4 = 1; label_2637:; init__r242 = (_Bool)init__tmp___4; if (!(init__r311 == 0)) { init__tmp___5 = 1; label_2642:; init__r312 = (_Bool)init__tmp___5; if (!(init__r321 == 0)) { init__tmp___6 = 1; label_2647:; init__r322 = (_Bool)init__tmp___6; if (!(init__r341 == 0)) { init__tmp___7 = 1; label_2652:; init__r342 = (_Bool)init__tmp___7; if (!(init__r411 == 0)) { init__tmp___8 = 1; label_2657:; init__r412 = (_Bool)init__tmp___8; if (!(init__r421 == 0)) { init__tmp___9 = 1; label_2662:; init__r422 = (_Bool)init__tmp___9; if (!(init__r431 == 0)) { init__tmp___10 = 1; label_2667:; init__r432 = (_Bool)init__tmp___10; if (!(init__r122 == 0)) { init__tmp___11 = 1; label_2672:; init__r123 = (_Bool)init__tmp___11; if (!(init__r132 == 0)) { init__tmp___12 = 1; label_2677:; init__r133 = (_Bool)init__tmp___12; if (!(init__r142 == 0)) { init__tmp___13 = 1; label_2682:; init__r143 = (_Bool)init__tmp___13; if (!(init__r212 == 0)) { init__tmp___14 = 1; label_2687:; init__r213 = (_Bool)init__tmp___14; if (!(init__r232 == 0)) { init__tmp___15 = 1; label_2692:; init__r233 = (_Bool)init__tmp___15; if (!(init__r242 == 0)) { init__tmp___16 = 1; label_2697:; init__r243 = (_Bool)init__tmp___16; if (!(init__r312 == 0)) { init__tmp___17 = 1; label_2702:; init__r313 = (_Bool)init__tmp___17; if (!(init__r322 == 0)) { init__tmp___18 = 1; label_2707:; init__r323 = (_Bool)init__tmp___18; if (!(init__r342 == 0)) { init__tmp___19 = 1; label_2712:; init__r343 = (_Bool)init__tmp___19; if (!(init__r412 == 0)) { init__tmp___20 = 1; label_2717:; init__r413 = (_Bool)init__tmp___20; if (!(init__r422 == 0)) { init__tmp___21 = 1; label_2722:; init__r423 = (_Bool)init__tmp___21; if (!(init__r432 == 0)) { init__tmp___22 = 1; label_2727:; init__r433 = (_Bool)init__tmp___22; if (((int)id1) != ((int)id2)) { if (((int)id1) != ((int)id3)) { if (((int)id1) != ((int)id4)) { if (((int)id2) != ((int)id3)) { if (((int)id2) != ((int)id4)) { if (((int)id3) != ((int)id4)) { if (((int)id1) >= 0) { if (((int)id2) >= 0) { if (((int)id3) >= 0) { if (((int)id4) >= 0) { if (((int)r1) == 0) { if (((int)r2) == 0) { if (((int)r3) == 0) { if (((int)r4) == 0) { if (!(init__r123 == 0)) { if (!(init__r133 == 0)) { if (!(init__r143 == 0)) { if (!(init__r213 == 0)) { if (!(init__r233 == 0)) { if (!(init__r243 == 0)) { if (!(init__r313 == 0)) { if (!(init__r323 == 0)) { if (!(init__r343 == 0)) { if (!(init__r413 == 0)) { if (!(init__r423 == 0)) { if (!(init__r433 == 0)) { if (((int)max1) == ((int)id1)) { if (((int)max2) == ((int)id2)) { if (((int)max3) == ((int)id3)) { if (((int)max4) == ((int)id4)) { if (((int)st1) == 0) { if (((int)st2) == 0) { if (((int)st3) == 0) { if (((int)st4) == 0) { if (((int)nl1) == 0) { if (((int)nl2) == 0) { if (((int)nl3) == 0) { if (((int)nl4) == 0) { if (((int)mode1) == 0) { if (((int)mode2) == 0) { if (((int)mode3) == 0) { if (((int)mode4) == 0) { init__tmp___23 = 1; __return_2814 = init__tmp___23; main__i2 = __return_2814; if (main__i2 != 0) { p12_old = nomsg; p12_new = nomsg; p13_old = nomsg; p13_new = nomsg; p14_old = nomsg; p14_new = nomsg; p21_old = nomsg; p21_new = nomsg; p23_old = nomsg; p23_new = nomsg; p24_old = nomsg; p24_new = nomsg; p31_old = nomsg; p31_new = nomsg; p32_old = nomsg; p32_new = nomsg; p34_old = nomsg; p34_new = nomsg; p41_old = nomsg; p41_new = nomsg; p42_old = nomsg; p42_new = nomsg; p43_old = nomsg; p43_new = nomsg; main__i2 = 0; if (main__i2 < 8) { { if (!(mode1 == 0)) { return __return_main; } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_2854:; p12_new = node1____CPAchecker_TMP_0; label_2849:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_2862:; p13_new = node1____CPAchecker_TMP_1; label_2857:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_2870:; p14_new = node1____CPAchecker_TMP_2; label_2872:; 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_2886:; p21_new = node2____CPAchecker_TMP_0; label_2881:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_2894:; p23_new = node2____CPAchecker_TMP_1; label_2889:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_2902:; p24_new = node2____CPAchecker_TMP_2; label_2904:; 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_2918:; p31_new = node3____CPAchecker_TMP_0; label_2913:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_2926:; p32_new = node3____CPAchecker_TMP_1; label_2921:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_2934:; p34_new = node3____CPAchecker_TMP_2; label_2936:; 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_2950:; p41_new = node4____CPAchecker_TMP_0; label_2945:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_2958:; p42_new = node4____CPAchecker_TMP_1; label_2953:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_2966:; p43_new = node4____CPAchecker_TMP_2; label_2968:; 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_3024 = check__tmp; main__c1 = __return_3024; { _Bool __tmp_1; __tmp_1 = main__c1; _Bool assert__arg; assert__arg = __tmp_1; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_3040:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_3047:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_3054:; if (((int)r1) == 2) { return __return_main; } else { mode1 = 0; { if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_3070:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_3077:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_3084:; if (((int)r2) == 3) { return __return_main; } else { mode2 = 0; { if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_3100:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_3107:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_3114:; if (((int)r3) == 3) { return __return_main; } else { mode3 = 0; { if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_3130:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_3137:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_3144:; 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_3207 = check__tmp; main__c1 = __return_3207; { _Bool __tmp_2; __tmp_2 = main__c1; _Bool assert__arg; assert__arg = __tmp_2; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { return __return_main; } else { if (((int)r1) < 3) { if (!(ep12 == 0)) { int node1____CPAchecker_TMP_0; if (max1 != nomsg) { if (p12_new == nomsg) { node1____CPAchecker_TMP_0 = max1; label_3228:; p12_new = node1____CPAchecker_TMP_0; label_3223:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_3236:; p13_new = node1____CPAchecker_TMP_1; label_3231:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_3244:; p14_new = node1____CPAchecker_TMP_2; label_3246:; 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_3260:; p21_new = node2____CPAchecker_TMP_0; label_3255:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_3268:; p23_new = node2____CPAchecker_TMP_1; label_3263:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_3276:; p24_new = node2____CPAchecker_TMP_2; label_3278:; 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_3292:; p31_new = node3____CPAchecker_TMP_0; label_3287:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_3300:; p32_new = node3____CPAchecker_TMP_1; label_3295:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_3308:; p34_new = node3____CPAchecker_TMP_2; label_3310:; 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_3324:; p41_new = node4____CPAchecker_TMP_0; label_3319:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_3332:; p42_new = node4____CPAchecker_TMP_1; label_3327:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_3340:; p43_new = node4____CPAchecker_TMP_2; label_3342:; 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_3398 = check__tmp; main__c1 = __return_3398; { _Bool __tmp_3; __tmp_3 = main__c1; _Bool assert__arg; assert__arg = __tmp_3; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_3414:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_3421:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_3428:; if (((int)r1) == 2) { if (((int)max1) == ((int)id1)) { st1 = 1; mode1 = 0; { if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_3938:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_3945:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_3952:; if (((int)r2) == 3) { return __return_main; } else { mode2 = 0; { if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_3968:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_3975:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_3982:; if (((int)r3) == 3) { return __return_main; } else { mode3 = 0; { if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_3998:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4005:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_4012:; 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) { return __return_main; } else { check__tmp = 0; __return_4065 = check__tmp; main__c1 = __return_4065; { _Bool __tmp_4; __tmp_4 = main__c1; _Bool assert__arg; assert__arg = __tmp_4; if (assert__arg == 0) { {reach_error();} 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_4012; } } else { goto label_4012; } } else { goto label_4005; } } else { goto label_4005; } } else { goto label_3998; } } else { goto label_3998; } } else { return __return_main; } } } } else { goto label_3982; } } else { goto label_3982; } } else { goto label_3975; } } else { goto label_3975; } } else { goto label_3968; } } else { goto label_3968; } } else { return __return_main; } } } } else { goto label_3952; } } else { goto label_3952; } } else { goto label_3945; } } else { goto label_3945; } } else { goto label_3938; } } else { goto label_3938; } } else { return __return_main; } } } else { nl1 = 1; mode1 = 0; { if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_3448:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_3455:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_3462:; if (((int)r2) == 3) { return __return_main; } else { mode2 = 0; { if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_3478:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_3485:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_3492:; if (((int)r3) == 3) { return __return_main; } else { mode3 = 0; { if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_3508:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_3515:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_3522:; 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) { return __return_main; } else { check__tmp = 0; __return_3582 = check__tmp; main__c1 = __return_3582; __tmp_3583_0 = main____CPAchecker_TMP_0; label_3583:; main____CPAchecker_TMP_0 = __tmp_3583_0; { _Bool __tmp_5; __tmp_5 = main__c1; _Bool assert__arg; assert__arg = __tmp_5; if (assert__arg == 0) { {reach_error();} return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; if (main__i2 < 8) { { if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); if (!(ep21 == 0)) { m1 = p21_old; p21_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_3602:; if (!(ep31 == 0)) { m1 = p31_old; p31_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_3609:; if (!(ep41 == 0)) { m1 = p41_old; p41_old = nomsg; if (((int)m1) > ((int)max1)) { max1 = m1; label_3616:; if (((int)r1) == 2) { if (((int)max1) == ((int)id1)) { st1 = 1; label_3624:; mode1 = 0; label_3626:; { if (!(mode2 == 0)) { r2 = (char)(((int)r2) + 1); if (!(ep12 == 0)) { m2 = p12_old; p12_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_3634:; if (!(ep32 == 0)) { m2 = p32_old; p32_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_3641:; if (!(ep42 == 0)) { m2 = p42_old; p42_old = nomsg; if (((int)m2) > ((int)max2)) { max2 = m2; label_3648:; if (((int)r2) == 3) { if (((int)max2) == ((int)id2)) { st2 = 1; label_3656:; mode2 = 0; label_3658:; { if (!(mode3 == 0)) { r3 = (char)(((int)r3) + 1); if (!(ep13 == 0)) { m3 = p13_old; p13_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_3666:; if (!(ep23 == 0)) { m3 = p23_old; p23_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_3673:; if (!(ep43 == 0)) { m3 = p43_old; p43_old = nomsg; if (((int)m3) > ((int)max3)) { max3 = m3; label_3680:; if (((int)r3) == 3) { if (((int)max3) == ((int)id3)) { st3 = 1; label_3688:; mode3 = 0; label_3690:; { if (!(mode4 == 0)) { r4 = (char)(((int)r4) + 1); if (!(ep14 == 0)) { m4 = p14_old; p14_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_3698:; if (!(ep24 == 0)) { m4 = p24_old; p24_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_3705:; if (!(ep34 == 0)) { m4 = p34_old; p34_old = nomsg; if (((int)m4) > ((int)max4)) { max4 = m4; label_3712:; if (((int)r4) == 3) { if (((int)max4) == ((int)id4)) { st4 = 1; label_3720:; mode4 = 0; label_3722:; 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_3779:; if (((int)r1) < 3) { label_3786:; if (((int)r1) >= 3) { label_3793:; if (((int)r1) < 3) { check__tmp = 1; label_3799:; label_3792:; label_3785:; label_3778:; label_3772:; label_3768:; label_3764:; label_3760:; label_3755:; __return_3756 = check__tmp; main__c1 = __return_3756; __tmp_3583_0 = main____CPAchecker_TMP_0; goto label_3583; } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 3) { check__tmp = 1; goto label_3799; } else { check__tmp = 0; goto label_3799; } } } else { if ((((((int)nl1) + ((int)nl2)) + ((int)nl3)) + ((int)nl4)) == 0) { goto label_3793; } else { check__tmp = 0; goto label_3792; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 1) { goto label_3786; } else { check__tmp = 0; goto label_3785; } } } else { if ((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) == 0) { goto label_3779; } else { check__tmp = 0; goto label_3778; } } } else { check__tmp = 0; goto label_3772; } } else { check__tmp = 0; goto label_3768; } } else { check__tmp = 0; goto label_3764; } } else { check__tmp = 0; goto label_3760; } } else { check__tmp = 0; goto label_3755; } } } else { nl4 = 1; goto label_3720; } } else { goto label_3720; } } else { goto label_3712; } } else { goto label_3712; } } else { goto label_3705; } } else { goto label_3705; } } else { goto label_3698; } } else { goto label_3698; } } 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_3814:; p41_new = node4____CPAchecker_TMP_0; label_3809:; if (!(ep42 == 0)) { int node4____CPAchecker_TMP_1; if (max4 != nomsg) { if (p42_new == nomsg) { node4____CPAchecker_TMP_1 = max4; label_3822:; p42_new = node4____CPAchecker_TMP_1; label_3817:; if (!(ep43 == 0)) { int node4____CPAchecker_TMP_2; if (max4 != nomsg) { if (p43_new == nomsg) { node4____CPAchecker_TMP_2 = max4; label_3830:; p43_new = node4____CPAchecker_TMP_2; label_3807:; mode4 = 1; goto label_3722; } else { label_3829:; node4____CPAchecker_TMP_2 = p43_new; goto label_3830; } } else { goto label_3829; } } else { goto label_3807; } } else { label_3821:; node4____CPAchecker_TMP_1 = p42_new; goto label_3822; } } else { goto label_3821; } } else { goto label_3817; } } else { label_3813:; node4____CPAchecker_TMP_0 = p41_new; goto label_3814; } } else { goto label_3813; } } else { goto label_3809; } } else { goto label_3807; } } } } else { nl3 = 1; goto label_3688; } } else { goto label_3688; } } else { goto label_3680; } } else { goto label_3680; } } else { goto label_3673; } } else { goto label_3673; } } else { goto label_3666; } } else { goto label_3666; } } 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_3845:; p31_new = node3____CPAchecker_TMP_0; label_3840:; if (!(ep32 == 0)) { int node3____CPAchecker_TMP_1; if (max3 != nomsg) { if (p32_new == nomsg) { node3____CPAchecker_TMP_1 = max3; label_3853:; p32_new = node3____CPAchecker_TMP_1; label_3848:; if (!(ep34 == 0)) { int node3____CPAchecker_TMP_2; if (max3 != nomsg) { if (p34_new == nomsg) { node3____CPAchecker_TMP_2 = max3; label_3861:; p34_new = node3____CPAchecker_TMP_2; label_3838:; mode3 = 1; goto label_3690; } else { label_3860:; node3____CPAchecker_TMP_2 = p34_new; goto label_3861; } } else { goto label_3860; } } else { goto label_3838; } } else { label_3852:; node3____CPAchecker_TMP_1 = p32_new; goto label_3853; } } else { goto label_3852; } } else { goto label_3848; } } else { label_3844:; node3____CPAchecker_TMP_0 = p31_new; goto label_3845; } } else { goto label_3844; } } else { goto label_3840; } } else { goto label_3838; } } } } else { nl2 = 1; goto label_3656; } } else { goto label_3656; } } else { goto label_3648; } } else { goto label_3648; } } else { goto label_3641; } } else { goto label_3641; } } else { goto label_3634; } } else { goto label_3634; } } 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_3876:; p21_new = node2____CPAchecker_TMP_0; label_3871:; if (!(ep23 == 0)) { int node2____CPAchecker_TMP_1; if (max2 != nomsg) { if (p23_new == nomsg) { node2____CPAchecker_TMP_1 = max2; label_3884:; p23_new = node2____CPAchecker_TMP_1; label_3879:; if (!(ep24 == 0)) { int node2____CPAchecker_TMP_2; if (max2 != nomsg) { if (p24_new == nomsg) { node2____CPAchecker_TMP_2 = max2; label_3892:; p24_new = node2____CPAchecker_TMP_2; label_3869:; mode2 = 1; goto label_3658; } else { label_3891:; node2____CPAchecker_TMP_2 = p24_new; goto label_3892; } } else { goto label_3891; } } else { goto label_3869; } } else { label_3883:; node2____CPAchecker_TMP_1 = p23_new; goto label_3884; } } else { goto label_3883; } } else { goto label_3879; } } else { label_3875:; node2____CPAchecker_TMP_0 = p21_new; goto label_3876; } } else { goto label_3875; } } else { goto label_3871; } } else { goto label_3869; } } } } else { nl1 = 1; goto label_3624; } } else { goto label_3624; } } else { goto label_3616; } } else { goto label_3616; } } else { goto label_3609; } } else { goto label_3609; } } else { goto label_3602; } } else { goto label_3602; } } 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_3907:; p12_new = node1____CPAchecker_TMP_0; label_3902:; if (!(ep13 == 0)) { int node1____CPAchecker_TMP_1; if (max1 != nomsg) { if (p13_new == nomsg) { node1____CPAchecker_TMP_1 = max1; label_3915:; p13_new = node1____CPAchecker_TMP_1; label_3910:; if (!(ep14 == 0)) { int node1____CPAchecker_TMP_2; if (max1 != nomsg) { if (p14_new == nomsg) { node1____CPAchecker_TMP_2 = max1; label_3923:; p14_new = node1____CPAchecker_TMP_2; label_3900:; mode1 = 1; goto label_3626; } else { label_3922:; node1____CPAchecker_TMP_2 = p14_new; goto label_3923; } } else { goto label_3922; } } else { goto label_3900; } } else { label_3914:; node1____CPAchecker_TMP_1 = p13_new; goto label_3915; } } else { goto label_3914; } } else { goto label_3910; } } else { label_3906:; node1____CPAchecker_TMP_0 = p12_new; goto label_3907; } } else { goto label_3906; } } else { goto label_3902; } } else { goto label_3900; } } } } else { __return_3596 = 0; return __return_3596; } } } } } } else { 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_3522; } } else { goto label_3522; } } else { goto label_3515; } } else { goto label_3515; } } else { goto label_3508; } } else { goto label_3508; } } else { return __return_main; } } } } else { goto label_3492; } } else { goto label_3492; } } else { goto label_3485; } } else { goto label_3485; } } else { goto label_3478; } } else { goto label_3478; } } else { return __return_main; } } } } else { goto label_3462; } } else { goto label_3462; } } else { goto label_3455; } } else { goto label_3455; } } else { goto label_3448; } } else { goto label_3448; } } else { return __return_main; } } } } else { return __return_main; } } else { goto label_3428; } } else { goto label_3428; } } else { goto label_3421; } } else { goto label_3421; } } else { goto label_3414; } } else { goto label_3414; } } else { return __return_main; } } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } } else { label_3339:; node4____CPAchecker_TMP_2 = p43_new; goto label_3340; } } else { goto label_3339; } } else { goto label_3342; } } else { label_3331:; node4____CPAchecker_TMP_1 = p42_new; goto label_3332; } } else { goto label_3331; } } else { goto label_3327; } } else { label_3323:; node4____CPAchecker_TMP_0 = p41_new; goto label_3324; } } else { goto label_3323; } } else { goto label_3319; } } else { return __return_main; } } } } else { label_3307:; node3____CPAchecker_TMP_2 = p34_new; goto label_3308; } } else { goto label_3307; } } else { goto label_3310; } } else { label_3299:; node3____CPAchecker_TMP_1 = p32_new; goto label_3300; } } else { goto label_3299; } } else { goto label_3295; } } else { label_3291:; node3____CPAchecker_TMP_0 = p31_new; goto label_3292; } } else { goto label_3291; } } else { goto label_3287; } } else { return __return_main; } } } } else { label_3275:; node2____CPAchecker_TMP_2 = p24_new; goto label_3276; } } else { goto label_3275; } } else { goto label_3278; } } else { label_3267:; node2____CPAchecker_TMP_1 = p23_new; goto label_3268; } } else { goto label_3267; } } else { goto label_3263; } } else { label_3259:; node2____CPAchecker_TMP_0 = p21_new; goto label_3260; } } else { goto label_3259; } } else { goto label_3255; } } else { return __return_main; } } } } else { label_3243:; node1____CPAchecker_TMP_2 = p14_new; goto label_3244; } } else { goto label_3243; } } else { goto label_3246; } } else { label_3235:; node1____CPAchecker_TMP_1 = p13_new; goto label_3236; } } else { goto label_3235; } } else { goto label_3231; } } else { label_3227:; node1____CPAchecker_TMP_0 = p12_new; goto label_3228; } } else { goto label_3227; } } else { goto label_3223; } } else { return __return_main; } } } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } } } else { goto label_3144; } } else { goto label_3144; } } else { goto label_3137; } } else { goto label_3137; } } else { goto label_3130; } } else { goto label_3130; } } else { return __return_main; } } } } else { goto label_3114; } } else { goto label_3114; } } else { goto label_3107; } } else { goto label_3107; } } else { goto label_3100; } } else { goto label_3100; } } else { return __return_main; } } } } else { goto label_3084; } } else { goto label_3084; } } else { goto label_3077; } } else { goto label_3077; } } else { goto label_3070; } } else { goto label_3070; } } else { return __return_main; } } } } else { goto label_3054; } } else { goto label_3054; } } else { goto label_3047; } } else { goto label_3047; } } else { goto label_3040; } } else { goto label_3040; } } else { return __return_main; } } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } } else { label_2965:; node4____CPAchecker_TMP_2 = p43_new; goto label_2966; } } else { goto label_2965; } } else { goto label_2968; } } else { label_2957:; node4____CPAchecker_TMP_1 = p42_new; goto label_2958; } } else { goto label_2957; } } else { goto label_2953; } } else { label_2949:; node4____CPAchecker_TMP_0 = p41_new; goto label_2950; } } else { goto label_2949; } } else { goto label_2945; } } else { return __return_main; } } } } else { label_2933:; node3____CPAchecker_TMP_2 = p34_new; goto label_2934; } } else { goto label_2933; } } else { goto label_2936; } } else { label_2925:; node3____CPAchecker_TMP_1 = p32_new; goto label_2926; } } else { goto label_2925; } } else { goto label_2921; } } else { label_2917:; node3____CPAchecker_TMP_0 = p31_new; goto label_2918; } } else { goto label_2917; } } else { goto label_2913; } } else { return __return_main; } } } } else { label_2901:; node2____CPAchecker_TMP_2 = p24_new; goto label_2902; } } else { goto label_2901; } } else { goto label_2904; } } else { label_2893:; node2____CPAchecker_TMP_1 = p23_new; goto label_2894; } } else { goto label_2893; } } else { goto label_2889; } } else { label_2885:; node2____CPAchecker_TMP_0 = p21_new; goto label_2886; } } else { goto label_2885; } } else { goto label_2881; } } else { return __return_main; } } } } else { label_2869:; node1____CPAchecker_TMP_2 = p14_new; goto label_2870; } } else { goto label_2869; } } else { goto label_2872; } } else { label_2861:; node1____CPAchecker_TMP_1 = p13_new; goto label_2862; } } else { goto label_2861; } } else { goto label_2857; } } else { label_2853:; node1____CPAchecker_TMP_0 = p12_new; goto label_2854; } } else { goto label_2853; } } else { goto label_2849; } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { if (!(init__r412 == 0)) { if (!(ep13 == 0)) { init__tmp___22 = 1; goto label_2727; } else { label_4086:; if (!(init__r422 == 0)) { if (!(ep23 == 0)) { init__tmp___22 = 1; label_4092:; goto label_2727; } else { init__tmp___22 = 0; goto label_4092; } } else { init__tmp___22 = 0; goto label_2727; } } } else { goto label_4086; } } } else { if (!(init__r412 == 0)) { if (!(ep12 == 0)) { init__tmp___21 = 1; goto label_2722; } else { label_4101:; if (!(init__r432 == 0)) { if (!(ep32 == 0)) { init__tmp___21 = 1; label_4107:; goto label_2722; } else { init__tmp___21 = 0; goto label_4107; } } else { init__tmp___21 = 0; goto label_2722; } } } else { goto label_4101; } } } else { if (!(init__r422 == 0)) { if (!(ep21 == 0)) { init__tmp___20 = 1; goto label_2717; } else { label_4116:; if (!(init__r432 == 0)) { if (!(ep31 == 0)) { init__tmp___20 = 1; label_4122:; goto label_2717; } else { init__tmp___20 = 0; goto label_4122; } } else { init__tmp___20 = 0; goto label_2717; } } } else { goto label_4116; } } } else { if (!(init__r312 == 0)) { if (!(ep14 == 0)) { init__tmp___19 = 1; goto label_2712; } else { label_4131:; if (!(init__r322 == 0)) { if (!(ep24 == 0)) { init__tmp___19 = 1; label_4137:; goto label_2712; } else { init__tmp___19 = 0; goto label_4137; } } else { init__tmp___19 = 0; goto label_2712; } } } else { goto label_4131; } } } else { if (!(init__r312 == 0)) { if (!(ep12 == 0)) { init__tmp___18 = 1; goto label_2707; } else { label_4146:; if (!(init__r342 == 0)) { if (!(ep42 == 0)) { init__tmp___18 = 1; label_4152:; goto label_2707; } else { init__tmp___18 = 0; goto label_4152; } } else { init__tmp___18 = 0; goto label_2707; } } } else { goto label_4146; } } } else { if (!(init__r322 == 0)) { if (!(ep21 == 0)) { init__tmp___17 = 1; goto label_2702; } else { label_4161:; if (!(init__r342 == 0)) { if (!(ep41 == 0)) { init__tmp___17 = 1; label_4167:; goto label_2702; } else { init__tmp___17 = 0; goto label_4167; } } else { init__tmp___17 = 0; goto label_2702; } } } else { goto label_4161; } } } else { if (!(init__r212 == 0)) { if (!(ep14 == 0)) { init__tmp___16 = 1; goto label_2697; } else { label_4176:; if (!(init__r232 == 0)) { if (!(ep34 == 0)) { init__tmp___16 = 1; label_4182:; goto label_2697; } else { init__tmp___16 = 0; goto label_4182; } } else { init__tmp___16 = 0; goto label_2697; } } } else { goto label_4176; } } } else { if (!(init__r212 == 0)) { if (!(ep13 == 0)) { init__tmp___15 = 1; goto label_2692; } else { label_4191:; if (!(init__r242 == 0)) { if (!(ep43 == 0)) { init__tmp___15 = 1; label_4197:; goto label_2692; } else { init__tmp___15 = 0; goto label_4197; } } else { init__tmp___15 = 0; goto label_2692; } } } else { goto label_4191; } } } else { if (!(init__r232 == 0)) { if (!(ep31 == 0)) { init__tmp___14 = 1; goto label_2687; } else { label_4206:; if (!(init__r242 == 0)) { if (!(ep41 == 0)) { init__tmp___14 = 1; label_4212:; goto label_2687; } else { init__tmp___14 = 0; goto label_4212; } } else { init__tmp___14 = 0; goto label_2687; } } } else { goto label_4206; } } } else { if (!(init__r122 == 0)) { if (!(ep24 == 0)) { init__tmp___13 = 1; goto label_2682; } else { label_4221:; if (!(init__r132 == 0)) { if (!(ep34 == 0)) { init__tmp___13 = 1; label_4227:; goto label_2682; } else { init__tmp___13 = 0; goto label_4227; } } else { init__tmp___13 = 0; goto label_2682; } } } else { goto label_4221; } } } else { if (!(init__r122 == 0)) { if (!(ep23 == 0)) { init__tmp___12 = 1; goto label_2677; } else { label_4236:; if (!(init__r142 == 0)) { if (!(ep43 == 0)) { init__tmp___12 = 1; label_4242:; goto label_2677; } else { init__tmp___12 = 0; goto label_4242; } } else { init__tmp___12 = 0; goto label_2677; } } } else { goto label_4236; } } } else { if (!(init__r132 == 0)) { if (!(ep32 == 0)) { init__tmp___11 = 1; goto label_2672; } else { label_4251:; if (!(init__r142 == 0)) { if (!(ep42 == 0)) { init__tmp___11 = 1; label_4257:; goto label_2672; } else { init__tmp___11 = 0; goto label_4257; } } else { init__tmp___11 = 0; goto label_2672; } } } else { goto label_4251; } } } else { if (!(init__r411 == 0)) { if (!(ep13 == 0)) { init__tmp___10 = 1; goto label_2667; } else { label_4266:; if (!(init__r421 == 0)) { if (!(ep23 == 0)) { init__tmp___10 = 1; label_4272:; goto label_2667; } else { init__tmp___10 = 0; goto label_4272; } } else { init__tmp___10 = 0; goto label_2667; } } } else { goto label_4266; } } } else { if (!(init__r411 == 0)) { if (!(ep12 == 0)) { init__tmp___9 = 1; goto label_2662; } else { label_4281:; if (!(init__r431 == 0)) { if (!(ep32 == 0)) { init__tmp___9 = 1; label_4287:; goto label_2662; } else { init__tmp___9 = 0; goto label_4287; } } else { init__tmp___9 = 0; goto label_2662; } } } else { goto label_4281; } } } else { if (!(init__r421 == 0)) { if (!(ep21 == 0)) { init__tmp___8 = 1; goto label_2657; } else { label_4296:; if (!(init__r431 == 0)) { if (!(ep31 == 0)) { init__tmp___8 = 1; label_4302:; goto label_2657; } else { init__tmp___8 = 0; goto label_4302; } } else { init__tmp___8 = 0; goto label_2657; } } } else { goto label_4296; } } } else { if (!(init__r311 == 0)) { if (!(ep14 == 0)) { init__tmp___7 = 1; goto label_2652; } else { label_4311:; if (!(init__r321 == 0)) { if (!(ep24 == 0)) { init__tmp___7 = 1; label_4317:; goto label_2652; } else { init__tmp___7 = 0; goto label_4317; } } else { init__tmp___7 = 0; goto label_2652; } } } else { goto label_4311; } } } else { if (!(init__r311 == 0)) { if (!(ep12 == 0)) { init__tmp___6 = 1; goto label_2647; } else { label_4326:; if (!(init__r341 == 0)) { if (!(ep42 == 0)) { init__tmp___6 = 1; label_4332:; goto label_2647; } else { init__tmp___6 = 0; goto label_4332; } } else { init__tmp___6 = 0; goto label_2647; } } } else { goto label_4326; } } } else { if (!(init__r321 == 0)) { if (!(ep21 == 0)) { init__tmp___5 = 1; goto label_2642; } else { label_4341:; if (!(init__r341 == 0)) { if (!(ep41 == 0)) { init__tmp___5 = 1; label_4347:; goto label_2642; } else { init__tmp___5 = 0; goto label_4347; } } else { init__tmp___5 = 0; goto label_2642; } } } else { goto label_4341; } } } else { if (!(init__r211 == 0)) { if (!(ep14 == 0)) { init__tmp___4 = 1; goto label_2637; } else { label_4356:; if (!(init__r231 == 0)) { if (!(ep34 == 0)) { init__tmp___4 = 1; label_4362:; goto label_2637; } else { init__tmp___4 = 0; goto label_4362; } } else { init__tmp___4 = 0; goto label_2637; } } } else { goto label_4356; } } } else { if (!(init__r211 == 0)) { if (!(ep13 == 0)) { init__tmp___3 = 1; goto label_2632; } else { label_4371:; if (!(init__r241 == 0)) { if (!(ep43 == 0)) { init__tmp___3 = 1; label_4377:; goto label_2632; } else { init__tmp___3 = 0; goto label_4377; } } else { init__tmp___3 = 0; goto label_2632; } } } else { goto label_4371; } } } else { if (!(init__r231 == 0)) { if (!(ep31 == 0)) { init__tmp___2 = 1; goto label_2627; } else { label_4386:; if (!(init__r241 == 0)) { if (!(ep41 == 0)) { init__tmp___2 = 1; label_4392:; goto label_2627; } else { init__tmp___2 = 0; goto label_4392; } } else { init__tmp___2 = 0; goto label_2627; } } } else { goto label_4386; } } } else { if (!(init__r121 == 0)) { if (!(ep24 == 0)) { init__tmp___1 = 1; goto label_2622; } else { label_4401:; if (!(init__r131 == 0)) { if (!(ep34 == 0)) { init__tmp___1 = 1; label_4407:; goto label_2622; } else { init__tmp___1 = 0; goto label_4407; } } else { init__tmp___1 = 0; goto label_2622; } } } else { goto label_4401; } } } else { if (!(init__r121 == 0)) { if (!(ep23 == 0)) { init__tmp___0 = 1; goto label_2617; } else { label_4416:; if (!(init__r141 == 0)) { if (!(ep43 == 0)) { init__tmp___0 = 1; label_4422:; goto label_2617; } else { init__tmp___0 = 0; goto label_4422; } } else { init__tmp___0 = 0; goto label_2617; } } } else { goto label_4416; } } } else { if (!(init__r131 == 0)) { if (!(ep32 == 0)) { init__tmp = 1; goto label_2612; } else { label_4431:; if (!(init__r141 == 0)) { if (!(ep42 == 0)) { init__tmp = 1; label_4437:; goto label_2612; } else { init__tmp = 0; goto label_4437; } } else { init__tmp = 0; goto label_2612; } } } else { goto label_4431; } } } }