// 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_lcr-var-start-time.5.2.ufo.BOUNDED-10.pals.c.v+lhb-reducer.c", 4, "reach_error"); } _Bool __VERIFIER_nondet_bool(); char __VERIFIER_nondet_char(); 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; char r1 = '\x0'; port_t p1 = 0; char p1_old = '\x0'; char p1_new = '\x0'; char id1 = '\x0'; char st1 = '\x0'; msg_t send1 = '\x0'; _Bool mode1 = 0; _Bool alive1 = 0; port_t p2 = 0; char p2_old = '\x0'; char p2_new = '\x0'; char id2 = '\x0'; char st2 = '\x0'; msg_t send2 = '\x0'; _Bool mode2 = 0; _Bool alive2 = 0; port_t p3 = 0; char p3_old = '\x0'; char p3_new = '\x0'; char id3 = '\x0'; char st3 = '\x0'; msg_t send3 = '\x0'; _Bool mode3 = 0; _Bool alive3 = 0; port_t p4 = 0; char p4_old = '\x0'; char p4_new = '\x0'; char id4 = '\x0'; char st4 = '\x0'; msg_t send4 = '\x0'; _Bool mode4 = 0; _Bool alive4 = 0; port_t p5 = 0; char p5_old = '\x0'; char p5_new = '\x0'; char id5 = '\x0'; char st5 = '\x0'; msg_t send5 = '\x0'; _Bool mode5 = 0; _Bool alive5 = 0; void node1(); void node2(); void node3(); void node4(); void node5(); void (*nodes[5])() = { &node1, &node2, &node3, &node4, &node5 }; int init(); int check(); int main(); int __return_33017; int __return_36426; int __tmp_33147_0; int __return_33230; int __tmp_33240_0; int __tmp_33298_0; int __tmp_36186_0; int __return_36203; int __tmp_33331_0; int __tmp_33337_0; int __return_33343; int __return_33874; int __return_34342; int __return_34623; int __return_35473; int __return_35790; int __return_33556; int __return_33922; int __return_34402; int __return_35545; int __return_33654; int __return_33962; int __return_34454; int __return_35609; int __return_33732; int __return_36507; int __return_36147; int __return_36367; int __return_36662; int __return_36698; int __return_36565; int __return_36601; int __return_35746; int __return_35879; int __return_35403; int __return_35687; int __return_36034; int __return_36070; int __return_35937; int __return_35973; int __return_36869; int __return_36905; int __return_36774; int __return_36810; int __return_37060; int __return_37096; int __return_36963; int __return_36999; int __return_34579; int __return_34712; int __return_34284; int __return_34520; int __return_34867; int __return_34903; int __return_34770; int __return_34806; int __return_33828; int __return_34016; int __return_33137; int __return_33769; int __return_34171; int __return_34207; int __return_34074; int __return_34110; int __return_35074; int __return_35110; int __return_34979; int __return_35015; int __return_35265; int __return_35301; int __return_35168; int __return_35204; int __return_37691; int __return_37727; int __return_37596; int __return_37632; int __return_37882; int __return_37918; int __return_37785; int __return_37821; int __return_37292; int __return_37328; int __return_37197; int __return_37233; int __return_37483; int __return_37519; int __return_37386; int __return_37422; int __return_38089; int __return_38125; int __return_37994; int __return_38030; int __return_38280; int __return_38316; int __return_38183; int __return_38219; int __return_40155; int __return_40191; int __return_40060; int __return_40096; int __return_40346; int __return_40382; int __return_40249; int __return_40285; int __return_39756; int __return_39792; int __return_39661; int __return_39697; int __return_39947; int __return_39983; int __return_39850; int __return_39886; int __return_40553; int __return_40589; int __return_40458; int __return_40494; int __return_40744; int __return_40780; int __return_40647; int __return_40683; int __return_38934; int __return_38970; int __return_38839; int __return_38875; int __return_39125; int __return_39161; int __return_39028; int __return_39064; int __return_38535; int __return_38571; int __return_38440; int __return_38476; int __return_38726; int __return_38762; int __return_38629; int __return_38665; int __return_39332; int __return_39368; int __return_39237; int __return_39273; int __return_39523; int __return_39559; int __return_39426; int __return_39462; int __return_41375; int __return_41411; int __return_41280; int __return_41316; int __return_41566; int __return_41602; int __return_41469; int __return_41505; int __return_40976; int __return_41012; int __return_40881; int __return_40917; int __return_41167; int __return_41203; int __return_41070; int __return_41106; int __return_41773; int __return_41809; int __return_41678; int __return_41714; int __return_41964; int __return_42000; int __return_41867; int __return_41903; int main() { int main__c1; int main__i2; main__c1 = 0; r1 = __VERIFIER_nondet_char(); id1 = __VERIFIER_nondet_char(); st1 = __VERIFIER_nondet_char(); send1 = __VERIFIER_nondet_char(); mode1 = __VERIFIER_nondet_bool(); alive1 = __VERIFIER_nondet_bool(); id2 = __VERIFIER_nondet_char(); st2 = __VERIFIER_nondet_char(); send2 = __VERIFIER_nondet_char(); mode2 = __VERIFIER_nondet_bool(); alive2 = __VERIFIER_nondet_bool(); id3 = __VERIFIER_nondet_char(); st3 = __VERIFIER_nondet_char(); send3 = __VERIFIER_nondet_char(); mode3 = __VERIFIER_nondet_bool(); alive3 = __VERIFIER_nondet_bool(); id4 = __VERIFIER_nondet_char(); st4 = __VERIFIER_nondet_char(); send4 = __VERIFIER_nondet_char(); mode4 = __VERIFIER_nondet_bool(); alive4 = __VERIFIER_nondet_bool(); id5 = __VERIFIER_nondet_char(); st5 = __VERIFIER_nondet_char(); send5 = __VERIFIER_nondet_char(); mode5 = __VERIFIER_nondet_bool(); alive5 = __VERIFIER_nondet_bool(); { int init__tmp; if (((int)r1) == 0) { if (((((((int)alive1) + ((int)alive2)) + ((int)alive3)) + ((int)alive4)) + ((int)alive5)) >= 1) { if (((int)id1) >= 0) { if (((int)st1) == 0) { if (((int)send1) == ((int)id1)) { if (((int)mode1) == 0) { if (((int)id2) >= 0) { if (((int)st2) == 0) { if (((int)send2) == ((int)id2)) { if (((int)mode2) == 0) { if (((int)id3) >= 0) { if (((int)st3) == 0) { if (((int)send3) == ((int)id3)) { if (((int)mode3) == 0) { if (((int)id4) >= 0) { if (((int)st4) == 0) { if (((int)send4) == ((int)id4)) { if (((int)mode4) == 0) { if (((int)id5) >= 0) { if (((int)st5) == 0) { if (((int)send5) == ((int)id5)) { if (((int)mode5) == 0) { if (((int)id1) != ((int)id2)) { if (((int)id1) != ((int)id3)) { if (((int)id1) != ((int)id4)) { if (((int)id1) != ((int)id5)) { if (((int)id2) != ((int)id3)) { if (((int)id2) != ((int)id4)) { if (((int)id2) != ((int)id5)) { if (((int)id3) != ((int)id4)) { if (((int)id3) != ((int)id5)) { if (((int)id4) != ((int)id5)) { init__tmp = 1; __return_33017 = init__tmp; main__i2 = __return_33017; if (main__i2 != 0) { p1_old = nomsg; p1_new = nomsg; p2_old = nomsg; p2_new = nomsg; p3_old = nomsg; p3_new = nomsg; p4_old = nomsg; p4_new = nomsg; p5_old = nomsg; p5_new = nomsg; main__i2 = 0; if (main__i2 < 10) { { msg_t node1__m1; node1__m1 = nomsg; if (!(mode1 == 0)) { return __return_main; } else { if (!(alive1 == 0)) { int node1____CPAchecker_TMP_0; if (send1 != nomsg) { if (p1_new == nomsg) { node1____CPAchecker_TMP_0 = send1; label_33044:; p1_new = node1____CPAchecker_TMP_0; mode1 = 1; { msg_t node2__m2; node2__m2 = nomsg; if (!(mode2 == 0)) { return __return_main; } else { if (!(alive2 == 0)) { int node2____CPAchecker_TMP_0; if (send2 != nomsg) { if (p2_new == nomsg) { node2____CPAchecker_TMP_0 = send2; p2_new = node2____CPAchecker_TMP_0; label_35329:; mode2 = 1; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { return __return_main; } else { if (!(alive3 == 0)) { int node3____CPAchecker_TMP_0; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_0 = send3; p3_new = node3____CPAchecker_TMP_0; label_36090:; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_36401:; p5_new = node5____CPAchecker_TMP_0; label_36403:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36426 = check__tmp; main__c1 = __return_36426; { _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; __tmp_33147_0 = main____CPAchecker_TMP_0; label_33147:; main____CPAchecker_TMP_0 = __tmp_33147_0; if (main__i2 < 10) { { msg_t node1__m1; node1__m1 = nomsg; if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); node1__m1 = p5_old; p5_old = nomsg; if (((int)node1__m1) != ((int)nomsg)) { if (!(alive1 == 0)) { if (((int)node1__m1) > ((int)id1)) { send1 = node1__m1; label_33576:; mode1 = 0; label_33161:; { msg_t node2__m2; node2__m2 = nomsg; if (!(mode2 == 0)) { node2__m2 = p1_old; p1_old = nomsg; if (((int)node2__m2) != ((int)nomsg)) { if (!(alive2 == 0)) { if (((int)node2__m2) > ((int)id2)) { send2 = node2__m2; label_33491:; mode2 = 0; label_33174:; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { node3__m3 = p2_old; p2_old = nomsg; if (((int)node3__m3) != ((int)nomsg)) { if (!(alive3 == 0)) { if (((int)node3__m3) > ((int)id3)) { send3 = node3__m3; label_35420:; mode3 = 0; label_33186:; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { node4__m4 = p3_old; p3_old = nomsg; if (((int)node4__m4) != ((int)nomsg)) { if (!(alive4 == 0)) { if (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_34301:; mode4 = 0; label_33198:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_33845:; mode5 = 0; label_33210:; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_33230 = check__tmp; main__c1 = __return_33230; { _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; __tmp_33240_0 = main____CPAchecker_TMP_0; label_33240:; main____CPAchecker_TMP_0 = __tmp_33240_0; if (main__i2 < 10) { { msg_t node1__m1; node1__m1 = nomsg; if (!(mode1 == 0)) { r1 = (char)(((int)r1) + 1); node1__m1 = p5_old; p5_old = nomsg; if (((int)node1__m1) != ((int)nomsg)) { if (!(alive1 == 0)) { if (((int)node1__m1) > ((int)id1)) { send1 = node1__m1; label_33472:; label_33252:; mode1 = 0; label_33254:; { msg_t node2__m2; node2__m2 = nomsg; if (!(mode2 == 0)) { node2__m2 = p1_old; p1_old = nomsg; if (((int)node2__m2) != ((int)nomsg)) { if (!(alive2 == 0)) { if (((int)node2__m2) > ((int)id2)) { send2 = node2__m2; label_33444:; label_33266:; mode2 = 0; label_33268:; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { node3__m3 = p2_old; p2_old = nomsg; if (((int)node3__m3) != ((int)nomsg)) { if (!(alive3 == 0)) { if (((int)node3__m3) > ((int)id3)) { send3 = node3__m3; label_33416:; label_33280:; mode3 = 0; label_33282:; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { node4__m4 = p3_old; p3_old = nomsg; if (((int)node4__m4) != ((int)nomsg)) { if (!(alive4 == 0)) { if (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_33388:; label_33294:; mode4 = 0; label_33296:; __tmp_33298_0 = main____CPAchecker_TMP_0; label_33298:; main____CPAchecker_TMP_0 = __tmp_33298_0; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_33360:; label_33308:; mode5 = 0; label_33310:; __tmp_36186_0 = main____CPAchecker_TMP_0; label_36186:; main____CPAchecker_TMP_0 = __tmp_36186_0; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; label_33351:; label_36202:; __return_36203 = check__tmp; main__c1 = __return_36203; __tmp_33331_0 = main____CPAchecker_TMP_0; label_33331:; main____CPAchecker_TMP_0 = __tmp_33331_0; { _Bool __tmp_3; __tmp_3 = main__c1; _Bool assert__arg; assert__arg = __tmp_3; if (assert__arg == 0) { {reach_error();} return __return_main; } else { __tmp_33337_0 = main____CPAchecker_TMP_0; label_33337:; main____CPAchecker_TMP_0 = __tmp_33337_0; int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33240_0 = main____CPAchecker_TMP_0; goto label_33240; } } } else { if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) == 1) { check__tmp = 1; goto label_33351; } else { check__tmp = 0; goto label_33351; } } } else { check__tmp = 0; goto label_36202; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; goto label_33360; } else { goto label_33360; } } } else { send5 = node5__m5; goto label_33308; } } else { goto label_33308; } } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_33369:; p5_new = node5____CPAchecker_TMP_0; label_33371:; mode5 = 1; goto label_33310; } else { label_33368:; node5____CPAchecker_TMP_0 = p5_new; goto label_33369; } } else { goto label_33368; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_33379:; p5_new = node5____CPAchecker_TMP_1; goto label_33371; } else { label_33378:; node5____CPAchecker_TMP_1 = p5_new; goto label_33379; } } else { goto label_33378; } } else { goto label_33371; } } } } } else { if (((int)node4__m4) == ((int)id4)) { st4 = 1; goto label_33388; } else { goto label_33388; } } } else { send4 = node4__m4; goto label_33294; } } else { goto label_33294; } } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; label_33397:; p4_new = node4____CPAchecker_TMP_0; label_33399:; mode4 = 1; goto label_33296; } else { label_33396:; node4____CPAchecker_TMP_0 = p4_new; goto label_33397; } } else { goto label_33396; } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_33407:; p4_new = node4____CPAchecker_TMP_1; goto label_33399; } else { label_33406:; node4____CPAchecker_TMP_1 = p4_new; goto label_33407; } } else { goto label_33406; } } else { goto label_33399; } } } } } else { if (((int)node3__m3) == ((int)id3)) { st3 = 1; goto label_33416; } else { goto label_33416; } } } else { send3 = node3__m3; goto label_33280; } } else { goto label_33280; } } else { if (!(alive3 == 0)) { int node3____CPAchecker_TMP_0; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_0 = send3; label_33425:; p3_new = node3____CPAchecker_TMP_0; label_33427:; mode3 = 1; goto label_33282; } else { label_33424:; node3____CPAchecker_TMP_0 = p3_new; goto label_33425; } } else { goto label_33424; } } else { if (((int)send3) != ((int)id3)) { int node3____CPAchecker_TMP_1; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_1 = send3; label_33435:; p3_new = node3____CPAchecker_TMP_1; goto label_33427; } else { label_33434:; node3____CPAchecker_TMP_1 = p3_new; goto label_33435; } } else { goto label_33434; } } else { goto label_33427; } } } } } else { if (((int)node2__m2) == ((int)id2)) { st2 = 1; goto label_33444; } else { goto label_33444; } } } else { send2 = node2__m2; goto label_33266; } } else { goto label_33266; } } else { if (!(alive2 == 0)) { int node2____CPAchecker_TMP_0; if (send2 != nomsg) { if (p2_new == nomsg) { node2____CPAchecker_TMP_0 = send2; label_33453:; p2_new = node2____CPAchecker_TMP_0; label_33455:; mode2 = 1; goto label_33268; } else { label_33452:; node2____CPAchecker_TMP_0 = p2_new; goto label_33453; } } else { goto label_33452; } } else { if (((int)send2) != ((int)id2)) { int node2____CPAchecker_TMP_1; if (send2 != nomsg) { if (p2_new == nomsg) { node2____CPAchecker_TMP_1 = send2; label_33463:; p2_new = node2____CPAchecker_TMP_1; goto label_33455; } else { label_33462:; node2____CPAchecker_TMP_1 = p2_new; goto label_33463; } } else { goto label_33462; } } else { goto label_33455; } } } } } else { if (((int)node1__m1) == ((int)id1)) { st1 = 1; goto label_33472; } else { goto label_33472; } } } else { send1 = node1__m1; goto label_33252; } } else { goto label_33252; } } else { if (!(alive1 == 0)) { int node1____CPAchecker_TMP_0; if (send1 != nomsg) { if (p1_new == nomsg) { node1____CPAchecker_TMP_0 = send1; label_33481:; p1_new = node1____CPAchecker_TMP_0; label_33476:; mode1 = 1; goto label_33254; } else { label_33480:; node1____CPAchecker_TMP_0 = p1_new; goto label_33481; } } else { goto label_33480; } } else { goto label_33476; } } } } else { __return_33343 = 0; return __return_33343; } } } } else { return __return_main; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_33874 = check__tmp; main__c1 = __return_33874; { _Bool __tmp_4; __tmp_4 = main__c1; _Bool assert__arg; assert__arg = __tmp_4; if (assert__arg == 0) { {reach_error();} return __return_main; } else { __tmp_33337_0 = main____CPAchecker_TMP_0; goto label_33337; } } } else { return __return_main; } } else { return __return_main; } } } else { goto label_33845; } } } else { send5 = node5__m5; mode5 = 0; goto label_33210; } } else { mode5 = 0; goto label_33210; } } else { return __return_main; } } } else { if (((int)node4__m4) == ((int)id4)) { st4 = 1; mode4 = 0; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_34596:; mode5 = 0; label_34322:; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34342 = check__tmp; main__c1 = __return_34342; { _Bool __tmp_5; __tmp_5 = main__c1; _Bool assert__arg; assert__arg = __tmp_5; if (assert__arg == 0) { {reach_error();} return __return_main; } else { __tmp_33337_0 = main____CPAchecker_TMP_0; goto label_33337; } } } else { return __return_main; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { return __return_main; } else { check__tmp = 0; __return_34623 = check__tmp; main__c1 = __return_34623; __tmp_33331_0 = main____CPAchecker_TMP_0; goto label_33331; } } } else { goto label_34596; } } } else { send5 = node5__m5; mode5 = 0; goto label_34322; } } else { mode5 = 0; goto label_34322; } } else { return __return_main; } } } else { goto label_34301; } } } else { send4 = node4__m4; mode4 = 0; goto label_33198; } } else { mode4 = 0; goto label_33198; } } else { return __return_main; } } } else { if (((int)node3__m3) == ((int)id3)) { st3 = 1; mode3 = 0; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { node4__m4 = p3_old; p3_old = nomsg; if (((int)node4__m4) != ((int)nomsg)) { if (!(alive4 == 0)) { if (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_36164:; mode4 = 0; label_35441:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_35763:; mode5 = 0; label_35453:; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_35473 = check__tmp; main__c1 = __return_35473; { _Bool __tmp_6; __tmp_6 = main__c1; _Bool assert__arg; assert__arg = __tmp_6; if (assert__arg == 0) { {reach_error();} return __return_main; } else { __tmp_33337_0 = main____CPAchecker_TMP_0; goto label_33337; } } } else { return __return_main; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { return __return_main; } else { check__tmp = 0; __return_35790 = check__tmp; main__c1 = __return_35790; __tmp_33331_0 = main____CPAchecker_TMP_0; goto label_33331; } } } else { goto label_35763; } } } else { send5 = node5__m5; mode5 = 0; goto label_35453; } } else { mode5 = 0; goto label_35453; } } else { return __return_main; } } } else { if (((int)node4__m4) == ((int)id4)) { st4 = 1; mode4 = 0; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_36443:; mode5 = 0; label_36446:; label_36185:; __tmp_36186_0 = main____CPAchecker_TMP_0; goto label_36186; } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; goto label_36446; } else { goto label_36443; } } } else { send5 = node5__m5; mode5 = 0; goto label_36185; } } else { mode5 = 0; goto label_36185; } } else { return __return_main; } } } else { goto label_36164; } } } else { send4 = node4__m4; mode4 = 0; goto label_35441; } } else { mode4 = 0; goto label_35441; } } else { return __return_main; } } } else { goto label_35420; } } } else { send3 = node3__m3; mode3 = 0; goto label_33186; } } else { mode3 = 0; goto label_33186; } } else { return __return_main; } } } else { if (((int)node2__m2) == ((int)id2)) { st2 = 1; mode2 = 0; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { node3__m3 = p2_old; p2_old = nomsg; if (((int)node3__m3) != ((int)nomsg)) { if (!(alive3 == 0)) { if (((int)node3__m3) > ((int)id3)) { send3 = node3__m3; label_35494:; mode3 = 0; label_33512:; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { node4__m4 = p3_old; p3_old = nomsg; if (((int)node4__m4) != ((int)nomsg)) { if (!(alive4 == 0)) { if (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_34363:; mode4 = 0; label_33524:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_33895:; mode5 = 0; label_33536:; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_33556 = check__tmp; main__c1 = __return_33556; { _Bool __tmp_7; __tmp_7 = main__c1; _Bool assert__arg; assert__arg = __tmp_7; if (assert__arg == 0) { {reach_error();} return __return_main; } else { __tmp_33337_0 = main____CPAchecker_TMP_0; goto label_33337; } } } else { return __return_main; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { return __return_main; } else { check__tmp = 0; __return_33922 = check__tmp; main__c1 = __return_33922; __tmp_33331_0 = main____CPAchecker_TMP_0; goto label_33331; } } } else { goto label_33895; } } } else { send5 = node5__m5; mode5 = 0; goto label_33536; } } else { mode5 = 0; goto label_33536; } } else { return __return_main; } } } else { if (((int)node4__m4) == ((int)id4)) { st4 = 1; mode4 = 0; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_34636:; mode5 = 0; label_34384:; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { return __return_main; } else { check__tmp = 0; __return_34402 = check__tmp; main__c1 = __return_34402; __tmp_33331_0 = main____CPAchecker_TMP_0; goto label_33331; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; __tmp_36186_0 = main____CPAchecker_TMP_0; goto label_36186; } else { goto label_34636; } } } else { send5 = node5__m5; mode5 = 0; goto label_34384; } } else { mode5 = 0; goto label_34384; } } else { return __return_main; } } } else { goto label_34363; } } } else { send4 = node4__m4; mode4 = 0; goto label_33524; } } else { mode4 = 0; goto label_33524; } } else { return __return_main; } } } else { if (((int)node3__m3) == ((int)id3)) { st3 = 1; mode3 = 0; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { node4__m4 = p3_old; p3_old = nomsg; if (((int)node4__m4) != ((int)nomsg)) { if (!(alive4 == 0)) { if (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_36216:; mode4 = 0; label_35515:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_35803:; mode5 = 0; label_35527:; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { return __return_main; } else { check__tmp = 0; __return_35545 = check__tmp; main__c1 = __return_35545; __tmp_33331_0 = main____CPAchecker_TMP_0; goto label_33331; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; __tmp_36186_0 = main____CPAchecker_TMP_0; goto label_36186; } else { goto label_35803; } } } else { send5 = node5__m5; mode5 = 0; goto label_35527; } } else { mode5 = 0; goto label_35527; } } else { return __return_main; } } } else { if (((int)node4__m4) == ((int)id4)) { st4 = 1; mode4 = 0; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_36464:; label_36465:; mode5 = 0; label_36235:; __tmp_36186_0 = main____CPAchecker_TMP_0; goto label_36186; } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; goto label_36464; } else { goto label_36464; } } } else { send5 = node5__m5; goto label_36465; } } else { mode5 = 0; goto label_36235; } } else { return __return_main; } } } else { goto label_36216; } } } else { send4 = node4__m4; mode4 = 0; goto label_35515; } } else { mode4 = 0; goto label_35515; } } else { return __return_main; } } } else { goto label_35494; } } } else { send3 = node3__m3; mode3 = 0; goto label_33512; } } else { mode3 = 0; goto label_33512; } } else { return __return_main; } } } else { goto label_33491; } } } else { send2 = node2__m2; mode2 = 0; goto label_33174; } } else { mode2 = 0; goto label_33174; } } else { return __return_main; } } } else { if (((int)node1__m1) == ((int)id1)) { st1 = 1; mode1 = 0; { msg_t node2__m2; node2__m2 = nomsg; if (!(mode2 == 0)) { node2__m2 = p1_old; p1_old = nomsg; if (((int)node2__m2) != ((int)nomsg)) { if (!(alive2 == 0)) { if (((int)node2__m2) > ((int)id2)) { send2 = node2__m2; label_33669:; mode2 = 0; label_33598:; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { node3__m3 = p2_old; p2_old = nomsg; if (((int)node3__m3) != ((int)nomsg)) { if (!(alive3 == 0)) { if (((int)node3__m3) > ((int)id3)) { send3 = node3__m3; label_35558:; mode3 = 0; label_33610:; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { node4__m4 = p3_old; p3_old = nomsg; if (((int)node4__m4) != ((int)nomsg)) { if (!(alive4 == 0)) { if (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_34415:; mode4 = 0; label_33622:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_33935:; mode5 = 0; label_33634:; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_33654 = check__tmp; main__c1 = __return_33654; { _Bool __tmp_8; __tmp_8 = main__c1; _Bool assert__arg; assert__arg = __tmp_8; if (assert__arg == 0) { {reach_error();} return __return_main; } else { __tmp_33337_0 = main____CPAchecker_TMP_0; goto label_33337; } } } else { return __return_main; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { return __return_main; } else { check__tmp = 0; __return_33962 = check__tmp; main__c1 = __return_33962; __tmp_33331_0 = main____CPAchecker_TMP_0; goto label_33331; } } } else { goto label_33935; } } } else { send5 = node5__m5; mode5 = 0; goto label_33634; } } else { mode5 = 0; goto label_33634; } } else { return __return_main; } } } else { if (((int)node4__m4) == ((int)id4)) { st4 = 1; mode4 = 0; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_34658:; mode5 = 0; label_34436:; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { return __return_main; } else { check__tmp = 0; __return_34454 = check__tmp; main__c1 = __return_34454; __tmp_33331_0 = main____CPAchecker_TMP_0; goto label_33331; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; __tmp_36186_0 = main____CPAchecker_TMP_0; goto label_36186; } else { goto label_34658; } } } else { send5 = node5__m5; mode5 = 0; goto label_34436; } } else { mode5 = 0; goto label_34436; } } else { return __return_main; } } } else { goto label_34415; } } } else { send4 = node4__m4; mode4 = 0; goto label_33622; } } else { mode4 = 0; goto label_33622; } } else { return __return_main; } } } else { if (((int)node3__m3) == ((int)id3)) { st3 = 1; mode3 = 0; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { node4__m4 = p3_old; p3_old = nomsg; if (((int)node4__m4) != ((int)nomsg)) { if (!(alive4 == 0)) { if (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_36250:; mode4 = 0; label_35579:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_35825:; mode5 = 0; label_35591:; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { return __return_main; } else { check__tmp = 0; __return_35609 = check__tmp; main__c1 = __return_35609; __tmp_33331_0 = main____CPAchecker_TMP_0; goto label_33331; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; __tmp_36186_0 = main____CPAchecker_TMP_0; goto label_36186; } else { goto label_35825; } } } else { send5 = node5__m5; mode5 = 0; goto label_35591; } } else { mode5 = 0; goto label_35591; } } else { return __return_main; } } } else { if (((int)node4__m4) == ((int)id4)) { st4 = 1; mode4 = 0; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_36476:; label_36477:; mode5 = 0; label_36269:; __tmp_36186_0 = main____CPAchecker_TMP_0; goto label_36186; } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; goto label_36476; } else { goto label_36476; } } } else { send5 = node5__m5; goto label_36477; } } else { mode5 = 0; goto label_36269; } } else { return __return_main; } } } else { goto label_36250; } } } else { send4 = node4__m4; mode4 = 0; goto label_35579; } } else { mode4 = 0; goto label_35579; } } else { return __return_main; } } } else { goto label_35558; } } } else { send3 = node3__m3; mode3 = 0; goto label_33610; } } else { mode3 = 0; goto label_33610; } } else { return __return_main; } } } else { if (((int)node2__m2) == ((int)id2)) { st2 = 1; mode2 = 0; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { node3__m3 = p2_old; p2_old = nomsg; if (((int)node3__m3) != ((int)nomsg)) { if (!(alive3 == 0)) { if (((int)node3__m3) > ((int)id3)) { send3 = node3__m3; label_35622:; mode3 = 0; label_33690:; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { node4__m4 = p3_old; p3_old = nomsg; if (((int)node4__m4) != ((int)nomsg)) { if (!(alive4 == 0)) { if (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_34467:; mode4 = 0; label_33702:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_33975:; mode5 = 0; label_33714:; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { return __return_main; } else { check__tmp = 0; __return_33732 = check__tmp; main__c1 = __return_33732; __tmp_33331_0 = main____CPAchecker_TMP_0; goto label_33331; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; __tmp_36186_0 = main____CPAchecker_TMP_0; goto label_36186; } else { goto label_33975; } } } else { send5 = node5__m5; mode5 = 0; goto label_33714; } } else { mode5 = 0; goto label_33714; } } else { return __return_main; } } } else { if (((int)node4__m4) == ((int)id4)) { st4 = 1; mode4 = 0; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_34680:; label_34681:; mode5 = 0; label_34487:; __tmp_36186_0 = main____CPAchecker_TMP_0; goto label_36186; } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; goto label_34680; } else { goto label_34680; } } } else { send5 = node5__m5; goto label_34681; } } else { mode5 = 0; goto label_34487; } } else { return __return_main; } } } else { goto label_34467; } } } else { send4 = node4__m4; mode4 = 0; goto label_33702; } } else { mode4 = 0; goto label_33702; } } else { return __return_main; } } } else { if (((int)node3__m3) == ((int)id3)) { st3 = 1; mode3 = 0; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { node4__m4 = p3_old; p3_old = nomsg; if (((int)node4__m4) != ((int)nomsg)) { if (!(alive4 == 0)) { if (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_36284:; mode4 = 0; label_35643:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (!(alive5 == 0)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_35847:; label_35848:; mode5 = 0; label_35654:; __tmp_36186_0 = main____CPAchecker_TMP_0; goto label_36186; } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; goto label_35847; } else { goto label_35847; } } } else { send5 = node5__m5; goto label_35848; } } else { mode5 = 0; goto label_35654; } } else { return __return_main; } } } else { if (((int)node4__m4) == ((int)id4)) { st4 = 1; mode4 = 0; __tmp_33298_0 = main____CPAchecker_TMP_0; goto label_33298; } else { goto label_36284; } } } else { send4 = node4__m4; mode4 = 0; goto label_35643; } } else { mode4 = 0; goto label_35643; } } else { return __return_main; } } } else { goto label_35622; } } } else { send3 = node3__m3; mode3 = 0; goto label_33690; } } else { mode3 = 0; goto label_33690; } } else { return __return_main; } } } else { goto label_33669; } } } else { send2 = node2__m2; mode2 = 0; goto label_33598; } } else { mode2 = 0; goto label_33598; } } else { return __return_main; } } } else { goto label_33576; } } } else { send1 = node1__m1; mode1 = 0; goto label_33161; } } else { mode1 = 0; goto label_33161; } } else { return __return_main; } } } else { return __return_main; } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_36401; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_36520:; p5_new = node5____CPAchecker_TMP_1; goto label_36403; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_36520; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36507 = check__tmp; main__c1 = __return_36507; { _Bool __tmp_9; __tmp_9 = main__c1; _Bool assert__arg; assert__arg = __tmp_9; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_36122:; p5_new = node5____CPAchecker_TMP_0; label_36124:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36147 = check__tmp; main__c1 = __return_36147; { _Bool __tmp_10; __tmp_10 = main__c1; _Bool assert__arg; assert__arg = __tmp_10; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_36122; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_36380:; p5_new = node5____CPAchecker_TMP_1; goto label_36124; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_36380; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36367 = check__tmp; main__c1 = __return_36367; { _Bool __tmp_11; __tmp_11 = main__c1; _Bool assert__arg; assert__arg = __tmp_11; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_36620:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_36637:; p5_new = node5____CPAchecker_TMP_0; label_36639:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36662 = check__tmp; main__c1 = __return_36662; { _Bool __tmp_12; __tmp_12 = main__c1; _Bool assert__arg; assert__arg = __tmp_12; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_36637; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_36711:; p5_new = node5____CPAchecker_TMP_1; goto label_36639; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_36711; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36698 = check__tmp; main__c1 = __return_36698; { _Bool __tmp_13; __tmp_13 = main__c1; _Bool assert__arg; assert__arg = __tmp_13; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_36620; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_36540:; p5_new = node5____CPAchecker_TMP_0; label_36542:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36565 = check__tmp; main__c1 = __return_36565; { _Bool __tmp_14; __tmp_14 = main__c1; _Bool assert__arg; assert__arg = __tmp_14; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_36540; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_36614:; p5_new = node5____CPAchecker_TMP_1; goto label_36542; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_36614; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36601 = check__tmp; main__c1 = __return_36601; { _Bool __tmp_15; __tmp_15 = main__c1; _Bool assert__arg; assert__arg = __tmp_15; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } else { return __return_main; } } else { node3____CPAchecker_TMP_0 = p3_new; p3_new = node3____CPAchecker_TMP_0; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_35721:; p5_new = node5____CPAchecker_TMP_0; label_35723:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_35746 = check__tmp; main__c1 = __return_35746; { _Bool __tmp_16; __tmp_16 = main__c1; _Bool assert__arg; assert__arg = __tmp_16; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_35721; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_35892:; p5_new = node5____CPAchecker_TMP_1; goto label_35723; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_35892; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_35879 = check__tmp; main__c1 = __return_35879; { _Bool __tmp_17; __tmp_17 = main__c1; _Bool assert__arg; assert__arg = __tmp_17; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_35378:; p5_new = node5____CPAchecker_TMP_0; label_35380:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_35403 = check__tmp; main__c1 = __return_35403; { _Bool __tmp_18; __tmp_18 = main__c1; _Bool assert__arg; assert__arg = __tmp_18; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_35378; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_35700:; p5_new = node5____CPAchecker_TMP_1; goto label_35380; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_35700; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_35687 = check__tmp; main__c1 = __return_35687; { _Bool __tmp_19; __tmp_19 = main__c1; _Bool assert__arg; assert__arg = __tmp_19; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_35992:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_36009:; p5_new = node5____CPAchecker_TMP_0; label_36011:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36034 = check__tmp; main__c1 = __return_36034; { _Bool __tmp_20; __tmp_20 = main__c1; _Bool assert__arg; assert__arg = __tmp_20; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_36009; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_36083:; p5_new = node5____CPAchecker_TMP_1; goto label_36011; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_36083; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36070 = check__tmp; main__c1 = __return_36070; { _Bool __tmp_21; __tmp_21 = main__c1; _Bool assert__arg; assert__arg = __tmp_21; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_35992; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_35912:; p5_new = node5____CPAchecker_TMP_0; label_35914:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_35937 = check__tmp; main__c1 = __return_35937; { _Bool __tmp_22; __tmp_22 = main__c1; _Bool assert__arg; assert__arg = __tmp_22; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_35912; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_35986:; p5_new = node5____CPAchecker_TMP_1; goto label_35914; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_35986; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_35973 = check__tmp; main__c1 = __return_35973; { _Bool __tmp_23; __tmp_23 = main__c1; _Bool assert__arg; assert__arg = __tmp_23; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } } else { if (((int)send3) != ((int)id3)) { int node3____CPAchecker_TMP_1; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_1 = send3; p3_new = node3____CPAchecker_TMP_1; goto label_36090; } else { return __return_main; } } else { node3____CPAchecker_TMP_1 = p3_new; p3_new = node3____CPAchecker_TMP_1; label_36717:; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_36844:; p5_new = node5____CPAchecker_TMP_0; label_36846:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36869 = check__tmp; main__c1 = __return_36869; { _Bool __tmp_24; __tmp_24 = main__c1; _Bool assert__arg; assert__arg = __tmp_24; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_36844; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_36918:; p5_new = node5____CPAchecker_TMP_1; goto label_36846; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_36918; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36905 = check__tmp; main__c1 = __return_36905; { _Bool __tmp_25; __tmp_25 = main__c1; _Bool assert__arg; assert__arg = __tmp_25; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_36749:; p5_new = node5____CPAchecker_TMP_0; label_36751:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36774 = check__tmp; main__c1 = __return_36774; { _Bool __tmp_26; __tmp_26 = main__c1; _Bool assert__arg; assert__arg = __tmp_26; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_36749; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_36823:; p5_new = node5____CPAchecker_TMP_1; goto label_36751; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_36823; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36810 = check__tmp; main__c1 = __return_36810; { _Bool __tmp_27; __tmp_27 = main__c1; _Bool assert__arg; assert__arg = __tmp_27; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_37018:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_37035:; p5_new = node5____CPAchecker_TMP_0; label_37037:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37060 = check__tmp; main__c1 = __return_37060; { _Bool __tmp_28; __tmp_28 = main__c1; _Bool assert__arg; assert__arg = __tmp_28; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_37035; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_37109:; p5_new = node5____CPAchecker_TMP_1; goto label_37037; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_37109; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37096 = check__tmp; main__c1 = __return_37096; { _Bool __tmp_29; __tmp_29 = main__c1; _Bool assert__arg; assert__arg = __tmp_29; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_37018; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_36938:; p5_new = node5____CPAchecker_TMP_0; label_36940:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36963 = check__tmp; main__c1 = __return_36963; { _Bool __tmp_30; __tmp_30 = main__c1; _Bool assert__arg; assert__arg = __tmp_30; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_36938; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_37012:; p5_new = node5____CPAchecker_TMP_1; goto label_36940; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_37012; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_36999 = check__tmp; main__c1 = __return_36999; { _Bool __tmp_31; __tmp_31 = main__c1; _Bool assert__arg; assert__arg = __tmp_31; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } } else { goto label_36717; } } } } } else { return __return_main; } } else { node2____CPAchecker_TMP_0 = p2_new; p2_new = node2____CPAchecker_TMP_0; mode2 = 1; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { return __return_main; } else { if (!(alive3 == 0)) { int node3____CPAchecker_TMP_0; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_0 = send3; p3_new = node3____CPAchecker_TMP_0; label_34227:; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_34554:; p5_new = node5____CPAchecker_TMP_0; label_34556:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34579 = check__tmp; main__c1 = __return_34579; { _Bool __tmp_32; __tmp_32 = main__c1; _Bool assert__arg; assert__arg = __tmp_32; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_34554; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_34725:; p5_new = node5____CPAchecker_TMP_1; goto label_34556; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_34725; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34712 = check__tmp; main__c1 = __return_34712; { _Bool __tmp_33; __tmp_33 = main__c1; _Bool assert__arg; assert__arg = __tmp_33; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_34259:; p5_new = node5____CPAchecker_TMP_0; label_34261:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34284 = check__tmp; main__c1 = __return_34284; { _Bool __tmp_34; __tmp_34 = main__c1; _Bool assert__arg; assert__arg = __tmp_34; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_34259; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_34533:; p5_new = node5____CPAchecker_TMP_1; goto label_34261; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_34533; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34520 = check__tmp; main__c1 = __return_34520; { _Bool __tmp_35; __tmp_35 = main__c1; _Bool assert__arg; assert__arg = __tmp_35; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_34825:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_34842:; p5_new = node5____CPAchecker_TMP_0; label_34844:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34867 = check__tmp; main__c1 = __return_34867; { _Bool __tmp_36; __tmp_36 = main__c1; _Bool assert__arg; assert__arg = __tmp_36; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_34842; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_34916:; p5_new = node5____CPAchecker_TMP_1; goto label_34844; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_34916; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34903 = check__tmp; main__c1 = __return_34903; { _Bool __tmp_37; __tmp_37 = main__c1; _Bool assert__arg; assert__arg = __tmp_37; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_34825; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_34745:; p5_new = node5____CPAchecker_TMP_0; label_34747:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34770 = check__tmp; main__c1 = __return_34770; { _Bool __tmp_38; __tmp_38 = main__c1; _Bool assert__arg; assert__arg = __tmp_38; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_34745; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_34819:; p5_new = node5____CPAchecker_TMP_1; goto label_34747; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_34819; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34806 = check__tmp; main__c1 = __return_34806; { _Bool __tmp_39; __tmp_39 = main__c1; _Bool assert__arg; assert__arg = __tmp_39; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } else { return __return_main; } } else { node3____CPAchecker_TMP_0 = p3_new; p3_new = node3____CPAchecker_TMP_0; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_33803:; p5_new = node5____CPAchecker_TMP_0; label_33805:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_33828 = check__tmp; main__c1 = __return_33828; { _Bool __tmp_40; __tmp_40 = main__c1; _Bool assert__arg; assert__arg = __tmp_40; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_33803; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_34029:; p5_new = node5____CPAchecker_TMP_1; goto label_33805; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_34029; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34016 = check__tmp; main__c1 = __return_34016; { _Bool __tmp_41; __tmp_41 = main__c1; _Bool assert__arg; assert__arg = __tmp_41; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_33112:; p5_new = node5____CPAchecker_TMP_0; label_33114:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_33137 = check__tmp; main__c1 = __return_33137; { _Bool __tmp_42; __tmp_42 = main__c1; _Bool assert__arg; assert__arg = __tmp_42; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_33112; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_33782:; p5_new = node5____CPAchecker_TMP_1; goto label_33114; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_33782; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_33769 = check__tmp; main__c1 = __return_33769; { _Bool __tmp_43; __tmp_43 = main__c1; _Bool assert__arg; assert__arg = __tmp_43; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_34129:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_34146:; p5_new = node5____CPAchecker_TMP_0; label_34148:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34171 = check__tmp; main__c1 = __return_34171; { _Bool __tmp_44; __tmp_44 = main__c1; _Bool assert__arg; assert__arg = __tmp_44; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_34146; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_34220:; p5_new = node5____CPAchecker_TMP_1; goto label_34148; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_34220; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34207 = check__tmp; main__c1 = __return_34207; { _Bool __tmp_45; __tmp_45 = main__c1; _Bool assert__arg; assert__arg = __tmp_45; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_34129; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_34049:; p5_new = node5____CPAchecker_TMP_0; label_34051:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34074 = check__tmp; main__c1 = __return_34074; { _Bool __tmp_46; __tmp_46 = main__c1; _Bool assert__arg; assert__arg = __tmp_46; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_34049; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_34123:; p5_new = node5____CPAchecker_TMP_1; goto label_34051; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_34123; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34110 = check__tmp; main__c1 = __return_34110; { _Bool __tmp_47; __tmp_47 = main__c1; _Bool assert__arg; assert__arg = __tmp_47; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } } else { if (((int)send3) != ((int)id3)) { int node3____CPAchecker_TMP_1; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_1 = send3; p3_new = node3____CPAchecker_TMP_1; goto label_34227; } else { return __return_main; } } else { node3____CPAchecker_TMP_1 = p3_new; p3_new = node3____CPAchecker_TMP_1; label_34922:; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_35049:; p5_new = node5____CPAchecker_TMP_0; label_35051:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_35074 = check__tmp; main__c1 = __return_35074; { _Bool __tmp_48; __tmp_48 = main__c1; _Bool assert__arg; assert__arg = __tmp_48; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_35049; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_35123:; p5_new = node5____CPAchecker_TMP_1; goto label_35051; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_35123; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_35110 = check__tmp; main__c1 = __return_35110; { _Bool __tmp_49; __tmp_49 = main__c1; _Bool assert__arg; assert__arg = __tmp_49; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_34954:; p5_new = node5____CPAchecker_TMP_0; label_34956:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_34979 = check__tmp; main__c1 = __return_34979; { _Bool __tmp_50; __tmp_50 = main__c1; _Bool assert__arg; assert__arg = __tmp_50; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_34954; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_35028:; p5_new = node5____CPAchecker_TMP_1; goto label_34956; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_35028; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_35015 = check__tmp; main__c1 = __return_35015; { _Bool __tmp_51; __tmp_51 = main__c1; _Bool assert__arg; assert__arg = __tmp_51; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_35223:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_35240:; p5_new = node5____CPAchecker_TMP_0; label_35242:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_35265 = check__tmp; main__c1 = __return_35265; { _Bool __tmp_52; __tmp_52 = main__c1; _Bool assert__arg; assert__arg = __tmp_52; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_35240; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_35314:; p5_new = node5____CPAchecker_TMP_1; goto label_35242; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_35314; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_35301 = check__tmp; main__c1 = __return_35301; { _Bool __tmp_53; __tmp_53 = main__c1; _Bool assert__arg; assert__arg = __tmp_53; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_35223; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_35143:; p5_new = node5____CPAchecker_TMP_0; label_35145:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_35168 = check__tmp; main__c1 = __return_35168; { _Bool __tmp_54; __tmp_54 = main__c1; _Bool assert__arg; assert__arg = __tmp_54; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_35143; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_35217:; p5_new = node5____CPAchecker_TMP_1; goto label_35145; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_35217; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_35204 = check__tmp; main__c1 = __return_35204; { _Bool __tmp_55; __tmp_55 = main__c1; _Bool assert__arg; assert__arg = __tmp_55; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } } else { goto label_34922; } } } } } } else { if (((int)send2) != ((int)id2)) { int node2____CPAchecker_TMP_1; if (send2 != nomsg) { if (p2_new == nomsg) { node2____CPAchecker_TMP_1 = send2; p2_new = node2____CPAchecker_TMP_1; goto label_35329; } else { return __return_main; } } else { node2____CPAchecker_TMP_1 = p2_new; p2_new = node2____CPAchecker_TMP_1; label_37123:; mode2 = 1; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { return __return_main; } else { if (!(alive3 == 0)) { int node3____CPAchecker_TMP_0; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_0 = send3; p3_new = node3____CPAchecker_TMP_0; label_37539:; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_37666:; p5_new = node5____CPAchecker_TMP_0; label_37668:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37691 = check__tmp; main__c1 = __return_37691; { _Bool __tmp_56; __tmp_56 = main__c1; _Bool assert__arg; assert__arg = __tmp_56; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_37666; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_37740:; p5_new = node5____CPAchecker_TMP_1; goto label_37668; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_37740; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37727 = check__tmp; main__c1 = __return_37727; { _Bool __tmp_57; __tmp_57 = main__c1; _Bool assert__arg; assert__arg = __tmp_57; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_37571:; p5_new = node5____CPAchecker_TMP_0; label_37573:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37596 = check__tmp; main__c1 = __return_37596; { _Bool __tmp_58; __tmp_58 = main__c1; _Bool assert__arg; assert__arg = __tmp_58; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_37571; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_37645:; p5_new = node5____CPAchecker_TMP_1; goto label_37573; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_37645; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37632 = check__tmp; main__c1 = __return_37632; { _Bool __tmp_59; __tmp_59 = main__c1; _Bool assert__arg; assert__arg = __tmp_59; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_37840:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_37857:; p5_new = node5____CPAchecker_TMP_0; label_37859:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37882 = check__tmp; main__c1 = __return_37882; { _Bool __tmp_60; __tmp_60 = main__c1; _Bool assert__arg; assert__arg = __tmp_60; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_37857; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_37931:; p5_new = node5____CPAchecker_TMP_1; goto label_37859; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_37931; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37918 = check__tmp; main__c1 = __return_37918; { _Bool __tmp_61; __tmp_61 = main__c1; _Bool assert__arg; assert__arg = __tmp_61; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_37840; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_37760:; p5_new = node5____CPAchecker_TMP_0; label_37762:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37785 = check__tmp; main__c1 = __return_37785; { _Bool __tmp_62; __tmp_62 = main__c1; _Bool assert__arg; assert__arg = __tmp_62; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_37760; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_37834:; p5_new = node5____CPAchecker_TMP_1; goto label_37762; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_37834; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37821 = check__tmp; main__c1 = __return_37821; { _Bool __tmp_63; __tmp_63 = main__c1; _Bool assert__arg; assert__arg = __tmp_63; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } else { return __return_main; } } else { node3____CPAchecker_TMP_0 = p3_new; p3_new = node3____CPAchecker_TMP_0; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_37267:; p5_new = node5____CPAchecker_TMP_0; label_37269:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37292 = check__tmp; main__c1 = __return_37292; { _Bool __tmp_64; __tmp_64 = main__c1; _Bool assert__arg; assert__arg = __tmp_64; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_37267; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_37341:; p5_new = node5____CPAchecker_TMP_1; goto label_37269; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_37341; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37328 = check__tmp; main__c1 = __return_37328; { _Bool __tmp_65; __tmp_65 = main__c1; _Bool assert__arg; assert__arg = __tmp_65; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_37172:; p5_new = node5____CPAchecker_TMP_0; label_37174:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37197 = check__tmp; main__c1 = __return_37197; { _Bool __tmp_66; __tmp_66 = main__c1; _Bool assert__arg; assert__arg = __tmp_66; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_37172; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_37246:; p5_new = node5____CPAchecker_TMP_1; goto label_37174; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_37246; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37233 = check__tmp; main__c1 = __return_37233; { _Bool __tmp_67; __tmp_67 = main__c1; _Bool assert__arg; assert__arg = __tmp_67; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_37441:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_37458:; p5_new = node5____CPAchecker_TMP_0; label_37460:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37483 = check__tmp; main__c1 = __return_37483; { _Bool __tmp_68; __tmp_68 = main__c1; _Bool assert__arg; assert__arg = __tmp_68; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_37458; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_37532:; p5_new = node5____CPAchecker_TMP_1; goto label_37460; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_37532; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37519 = check__tmp; main__c1 = __return_37519; { _Bool __tmp_69; __tmp_69 = main__c1; _Bool assert__arg; assert__arg = __tmp_69; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_37441; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_37361:; p5_new = node5____CPAchecker_TMP_0; label_37363:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37386 = check__tmp; main__c1 = __return_37386; { _Bool __tmp_70; __tmp_70 = main__c1; _Bool assert__arg; assert__arg = __tmp_70; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_37361; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_37435:; p5_new = node5____CPAchecker_TMP_1; goto label_37363; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_37435; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37422 = check__tmp; main__c1 = __return_37422; { _Bool __tmp_71; __tmp_71 = main__c1; _Bool assert__arg; assert__arg = __tmp_71; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } } else { if (((int)send3) != ((int)id3)) { int node3____CPAchecker_TMP_1; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_1 = send3; p3_new = node3____CPAchecker_TMP_1; goto label_37539; } else { return __return_main; } } else { node3____CPAchecker_TMP_1 = p3_new; p3_new = node3____CPAchecker_TMP_1; label_37937:; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_38064:; p5_new = node5____CPAchecker_TMP_0; label_38066:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38089 = check__tmp; main__c1 = __return_38089; { _Bool __tmp_72; __tmp_72 = main__c1; _Bool assert__arg; assert__arg = __tmp_72; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_38064; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_38138:; p5_new = node5____CPAchecker_TMP_1; goto label_38066; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_38138; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38125 = check__tmp; main__c1 = __return_38125; { _Bool __tmp_73; __tmp_73 = main__c1; _Bool assert__arg; assert__arg = __tmp_73; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_37969:; p5_new = node5____CPAchecker_TMP_0; label_37971:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_37994 = check__tmp; main__c1 = __return_37994; { _Bool __tmp_74; __tmp_74 = main__c1; _Bool assert__arg; assert__arg = __tmp_74; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_37969; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_38043:; p5_new = node5____CPAchecker_TMP_1; goto label_37971; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_38043; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38030 = check__tmp; main__c1 = __return_38030; { _Bool __tmp_75; __tmp_75 = main__c1; _Bool assert__arg; assert__arg = __tmp_75; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_38238:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_38255:; p5_new = node5____CPAchecker_TMP_0; label_38257:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38280 = check__tmp; main__c1 = __return_38280; { _Bool __tmp_76; __tmp_76 = main__c1; _Bool assert__arg; assert__arg = __tmp_76; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_38255; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_38329:; p5_new = node5____CPAchecker_TMP_1; goto label_38257; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_38329; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38316 = check__tmp; main__c1 = __return_38316; { _Bool __tmp_77; __tmp_77 = main__c1; _Bool assert__arg; assert__arg = __tmp_77; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_38238; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_38158:; p5_new = node5____CPAchecker_TMP_0; label_38160:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38183 = check__tmp; main__c1 = __return_38183; { _Bool __tmp_78; __tmp_78 = main__c1; _Bool assert__arg; assert__arg = __tmp_78; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_38158; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_38232:; p5_new = node5____CPAchecker_TMP_1; goto label_38160; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_38232; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38219 = check__tmp; main__c1 = __return_38219; { _Bool __tmp_79; __tmp_79 = main__c1; _Bool assert__arg; assert__arg = __tmp_79; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } } else { goto label_37937; } } } } } } else { goto label_37123; } } } } } else { return __return_main; } } else { node1____CPAchecker_TMP_0 = p1_new; goto label_33044; } } else { mode1 = 1; { msg_t node2__m2; node2__m2 = nomsg; if (!(mode2 == 0)) { return __return_main; } else { if (!(alive2 == 0)) { int node2____CPAchecker_TMP_0; if (send2 != nomsg) { if (p2_new == nomsg) { node2____CPAchecker_TMP_0 = send2; p2_new = node2____CPAchecker_TMP_0; label_39587:; mode2 = 1; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { return __return_main; } else { if (!(alive3 == 0)) { int node3____CPAchecker_TMP_0; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_0 = send3; p3_new = node3____CPAchecker_TMP_0; label_40003:; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_40130:; p5_new = node5____CPAchecker_TMP_0; label_40132:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40155 = check__tmp; main__c1 = __return_40155; { _Bool __tmp_80; __tmp_80 = main__c1; _Bool assert__arg; assert__arg = __tmp_80; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_40130; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_40204:; p5_new = node5____CPAchecker_TMP_1; goto label_40132; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_40204; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40191 = check__tmp; main__c1 = __return_40191; { _Bool __tmp_81; __tmp_81 = main__c1; _Bool assert__arg; assert__arg = __tmp_81; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_40035:; p5_new = node5____CPAchecker_TMP_0; label_40037:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40060 = check__tmp; main__c1 = __return_40060; { _Bool __tmp_82; __tmp_82 = main__c1; _Bool assert__arg; assert__arg = __tmp_82; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_40035; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_40109:; p5_new = node5____CPAchecker_TMP_1; goto label_40037; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_40109; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40096 = check__tmp; main__c1 = __return_40096; { _Bool __tmp_83; __tmp_83 = main__c1; _Bool assert__arg; assert__arg = __tmp_83; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_40304:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_40321:; p5_new = node5____CPAchecker_TMP_0; label_40323:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40346 = check__tmp; main__c1 = __return_40346; { _Bool __tmp_84; __tmp_84 = main__c1; _Bool assert__arg; assert__arg = __tmp_84; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_40321; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_40395:; p5_new = node5____CPAchecker_TMP_1; goto label_40323; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_40395; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40382 = check__tmp; main__c1 = __return_40382; { _Bool __tmp_85; __tmp_85 = main__c1; _Bool assert__arg; assert__arg = __tmp_85; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_40304; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_40224:; p5_new = node5____CPAchecker_TMP_0; label_40226:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40249 = check__tmp; main__c1 = __return_40249; { _Bool __tmp_86; __tmp_86 = main__c1; _Bool assert__arg; assert__arg = __tmp_86; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_40224; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_40298:; p5_new = node5____CPAchecker_TMP_1; goto label_40226; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_40298; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40285 = check__tmp; main__c1 = __return_40285; { _Bool __tmp_87; __tmp_87 = main__c1; _Bool assert__arg; assert__arg = __tmp_87; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } else { return __return_main; } } else { node3____CPAchecker_TMP_0 = p3_new; p3_new = node3____CPAchecker_TMP_0; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_39731:; p5_new = node5____CPAchecker_TMP_0; label_39733:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39756 = check__tmp; main__c1 = __return_39756; { _Bool __tmp_88; __tmp_88 = main__c1; _Bool assert__arg; assert__arg = __tmp_88; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_39731; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_39805:; p5_new = node5____CPAchecker_TMP_1; goto label_39733; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_39805; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39792 = check__tmp; main__c1 = __return_39792; { _Bool __tmp_89; __tmp_89 = main__c1; _Bool assert__arg; assert__arg = __tmp_89; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_39636:; p5_new = node5____CPAchecker_TMP_0; label_39638:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39661 = check__tmp; main__c1 = __return_39661; { _Bool __tmp_90; __tmp_90 = main__c1; _Bool assert__arg; assert__arg = __tmp_90; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_39636; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_39710:; p5_new = node5____CPAchecker_TMP_1; goto label_39638; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_39710; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39697 = check__tmp; main__c1 = __return_39697; { _Bool __tmp_91; __tmp_91 = main__c1; _Bool assert__arg; assert__arg = __tmp_91; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_39905:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_39922:; p5_new = node5____CPAchecker_TMP_0; label_39924:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39947 = check__tmp; main__c1 = __return_39947; { _Bool __tmp_92; __tmp_92 = main__c1; _Bool assert__arg; assert__arg = __tmp_92; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_39922; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_39996:; p5_new = node5____CPAchecker_TMP_1; goto label_39924; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_39996; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39983 = check__tmp; main__c1 = __return_39983; { _Bool __tmp_93; __tmp_93 = main__c1; _Bool assert__arg; assert__arg = __tmp_93; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_39905; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_39825:; p5_new = node5____CPAchecker_TMP_0; label_39827:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39850 = check__tmp; main__c1 = __return_39850; { _Bool __tmp_94; __tmp_94 = main__c1; _Bool assert__arg; assert__arg = __tmp_94; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_39825; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_39899:; p5_new = node5____CPAchecker_TMP_1; goto label_39827; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_39899; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39886 = check__tmp; main__c1 = __return_39886; { _Bool __tmp_95; __tmp_95 = main__c1; _Bool assert__arg; assert__arg = __tmp_95; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } } else { if (((int)send3) != ((int)id3)) { int node3____CPAchecker_TMP_1; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_1 = send3; p3_new = node3____CPAchecker_TMP_1; goto label_40003; } else { return __return_main; } } else { node3____CPAchecker_TMP_1 = p3_new; p3_new = node3____CPAchecker_TMP_1; label_40401:; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_40528:; p5_new = node5____CPAchecker_TMP_0; label_40530:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40553 = check__tmp; main__c1 = __return_40553; { _Bool __tmp_96; __tmp_96 = main__c1; _Bool assert__arg; assert__arg = __tmp_96; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_40528; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_40602:; p5_new = node5____CPAchecker_TMP_1; goto label_40530; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_40602; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40589 = check__tmp; main__c1 = __return_40589; { _Bool __tmp_97; __tmp_97 = main__c1; _Bool assert__arg; assert__arg = __tmp_97; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_40433:; p5_new = node5____CPAchecker_TMP_0; label_40435:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40458 = check__tmp; main__c1 = __return_40458; { _Bool __tmp_98; __tmp_98 = main__c1; _Bool assert__arg; assert__arg = __tmp_98; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_40433; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_40507:; p5_new = node5____CPAchecker_TMP_1; goto label_40435; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_40507; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40494 = check__tmp; main__c1 = __return_40494; { _Bool __tmp_99; __tmp_99 = main__c1; _Bool assert__arg; assert__arg = __tmp_99; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_40702:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_40719:; p5_new = node5____CPAchecker_TMP_0; label_40721:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40744 = check__tmp; main__c1 = __return_40744; { _Bool __tmp_100; __tmp_100 = main__c1; _Bool assert__arg; assert__arg = __tmp_100; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_40719; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_40793:; p5_new = node5____CPAchecker_TMP_1; goto label_40721; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_40793; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40780 = check__tmp; main__c1 = __return_40780; { _Bool __tmp_101; __tmp_101 = main__c1; _Bool assert__arg; assert__arg = __tmp_101; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_40702; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_40622:; p5_new = node5____CPAchecker_TMP_0; label_40624:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40647 = check__tmp; main__c1 = __return_40647; { _Bool __tmp_102; __tmp_102 = main__c1; _Bool assert__arg; assert__arg = __tmp_102; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_40622; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_40696:; p5_new = node5____CPAchecker_TMP_1; goto label_40624; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_40696; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40683 = check__tmp; main__c1 = __return_40683; { _Bool __tmp_103; __tmp_103 = main__c1; _Bool assert__arg; assert__arg = __tmp_103; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } } else { goto label_40401; } } } } } else { return __return_main; } } else { node2____CPAchecker_TMP_0 = p2_new; p2_new = node2____CPAchecker_TMP_0; mode2 = 1; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { return __return_main; } else { if (!(alive3 == 0)) { int node3____CPAchecker_TMP_0; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_0 = send3; p3_new = node3____CPAchecker_TMP_0; label_38782:; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_38909:; p5_new = node5____CPAchecker_TMP_0; label_38911:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38934 = check__tmp; main__c1 = __return_38934; { _Bool __tmp_104; __tmp_104 = main__c1; _Bool assert__arg; assert__arg = __tmp_104; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_38909; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_38983:; p5_new = node5____CPAchecker_TMP_1; goto label_38911; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_38983; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38970 = check__tmp; main__c1 = __return_38970; { _Bool __tmp_105; __tmp_105 = main__c1; _Bool assert__arg; assert__arg = __tmp_105; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_38814:; p5_new = node5____CPAchecker_TMP_0; label_38816:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38839 = check__tmp; main__c1 = __return_38839; { _Bool __tmp_106; __tmp_106 = main__c1; _Bool assert__arg; assert__arg = __tmp_106; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_38814; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_38888:; p5_new = node5____CPAchecker_TMP_1; goto label_38816; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_38888; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38875 = check__tmp; main__c1 = __return_38875; { _Bool __tmp_107; __tmp_107 = main__c1; _Bool assert__arg; assert__arg = __tmp_107; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_39083:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_39100:; p5_new = node5____CPAchecker_TMP_0; label_39102:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39125 = check__tmp; main__c1 = __return_39125; { _Bool __tmp_108; __tmp_108 = main__c1; _Bool assert__arg; assert__arg = __tmp_108; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_39100; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_39174:; p5_new = node5____CPAchecker_TMP_1; goto label_39102; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_39174; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39161 = check__tmp; main__c1 = __return_39161; { _Bool __tmp_109; __tmp_109 = main__c1; _Bool assert__arg; assert__arg = __tmp_109; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_39083; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_39003:; p5_new = node5____CPAchecker_TMP_0; label_39005:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39028 = check__tmp; main__c1 = __return_39028; { _Bool __tmp_110; __tmp_110 = main__c1; _Bool assert__arg; assert__arg = __tmp_110; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_39003; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_39077:; p5_new = node5____CPAchecker_TMP_1; goto label_39005; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_39077; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39064 = check__tmp; main__c1 = __return_39064; { _Bool __tmp_111; __tmp_111 = main__c1; _Bool assert__arg; assert__arg = __tmp_111; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } else { return __return_main; } } else { node3____CPAchecker_TMP_0 = p3_new; p3_new = node3____CPAchecker_TMP_0; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_38510:; p5_new = node5____CPAchecker_TMP_0; label_38512:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38535 = check__tmp; main__c1 = __return_38535; { _Bool __tmp_112; __tmp_112 = main__c1; _Bool assert__arg; assert__arg = __tmp_112; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_38510; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_38584:; p5_new = node5____CPAchecker_TMP_1; goto label_38512; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_38584; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38571 = check__tmp; main__c1 = __return_38571; { _Bool __tmp_113; __tmp_113 = main__c1; _Bool assert__arg; assert__arg = __tmp_113; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_38415:; p5_new = node5____CPAchecker_TMP_0; label_38417:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38440 = check__tmp; main__c1 = __return_38440; { _Bool __tmp_114; __tmp_114 = main__c1; _Bool assert__arg; assert__arg = __tmp_114; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_38415; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_38489:; p5_new = node5____CPAchecker_TMP_1; goto label_38417; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_38489; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38476 = check__tmp; main__c1 = __return_38476; { _Bool __tmp_115; __tmp_115 = main__c1; _Bool assert__arg; assert__arg = __tmp_115; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_38684:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_38701:; p5_new = node5____CPAchecker_TMP_0; label_38703:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38726 = check__tmp; main__c1 = __return_38726; { _Bool __tmp_116; __tmp_116 = main__c1; _Bool assert__arg; assert__arg = __tmp_116; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_38701; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_38775:; p5_new = node5____CPAchecker_TMP_1; goto label_38703; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_38775; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38762 = check__tmp; main__c1 = __return_38762; { _Bool __tmp_117; __tmp_117 = main__c1; _Bool assert__arg; assert__arg = __tmp_117; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_38684; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_38604:; p5_new = node5____CPAchecker_TMP_0; label_38606:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38629 = check__tmp; main__c1 = __return_38629; { _Bool __tmp_118; __tmp_118 = main__c1; _Bool assert__arg; assert__arg = __tmp_118; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_38604; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_38678:; p5_new = node5____CPAchecker_TMP_1; goto label_38606; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_38678; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_38665 = check__tmp; main__c1 = __return_38665; { _Bool __tmp_119; __tmp_119 = main__c1; _Bool assert__arg; assert__arg = __tmp_119; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } } else { if (((int)send3) != ((int)id3)) { int node3____CPAchecker_TMP_1; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_1 = send3; p3_new = node3____CPAchecker_TMP_1; goto label_38782; } else { return __return_main; } } else { node3____CPAchecker_TMP_1 = p3_new; p3_new = node3____CPAchecker_TMP_1; label_39180:; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_39307:; p5_new = node5____CPAchecker_TMP_0; label_39309:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39332 = check__tmp; main__c1 = __return_39332; { _Bool __tmp_120; __tmp_120 = main__c1; _Bool assert__arg; assert__arg = __tmp_120; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_39307; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_39381:; p5_new = node5____CPAchecker_TMP_1; goto label_39309; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_39381; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39368 = check__tmp; main__c1 = __return_39368; { _Bool __tmp_121; __tmp_121 = main__c1; _Bool assert__arg; assert__arg = __tmp_121; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_39212:; p5_new = node5____CPAchecker_TMP_0; label_39214:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39237 = check__tmp; main__c1 = __return_39237; { _Bool __tmp_122; __tmp_122 = main__c1; _Bool assert__arg; assert__arg = __tmp_122; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_39212; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_39286:; p5_new = node5____CPAchecker_TMP_1; goto label_39214; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_39286; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39273 = check__tmp; main__c1 = __return_39273; { _Bool __tmp_123; __tmp_123 = main__c1; _Bool assert__arg; assert__arg = __tmp_123; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_39481:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_39498:; p5_new = node5____CPAchecker_TMP_0; label_39500:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39523 = check__tmp; main__c1 = __return_39523; { _Bool __tmp_124; __tmp_124 = main__c1; _Bool assert__arg; assert__arg = __tmp_124; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_39498; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_39572:; p5_new = node5____CPAchecker_TMP_1; goto label_39500; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_39572; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39559 = check__tmp; main__c1 = __return_39559; { _Bool __tmp_125; __tmp_125 = main__c1; _Bool assert__arg; assert__arg = __tmp_125; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_39481; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_39401:; p5_new = node5____CPAchecker_TMP_0; label_39403:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39426 = check__tmp; main__c1 = __return_39426; { _Bool __tmp_126; __tmp_126 = main__c1; _Bool assert__arg; assert__arg = __tmp_126; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_39401; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_39475:; p5_new = node5____CPAchecker_TMP_1; goto label_39403; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_39475; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_39462 = check__tmp; main__c1 = __return_39462; { _Bool __tmp_127; __tmp_127 = main__c1; _Bool assert__arg; assert__arg = __tmp_127; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } } else { goto label_39180; } } } } } } else { if (((int)send2) != ((int)id2)) { int node2____CPAchecker_TMP_1; if (send2 != nomsg) { if (p2_new == nomsg) { node2____CPAchecker_TMP_1 = send2; p2_new = node2____CPAchecker_TMP_1; goto label_39587; } else { return __return_main; } } else { node2____CPAchecker_TMP_1 = p2_new; p2_new = node2____CPAchecker_TMP_1; label_40807:; mode2 = 1; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { return __return_main; } else { if (!(alive3 == 0)) { int node3____CPAchecker_TMP_0; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_0 = send3; p3_new = node3____CPAchecker_TMP_0; label_41223:; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_41350:; p5_new = node5____CPAchecker_TMP_0; label_41352:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41375 = check__tmp; main__c1 = __return_41375; { _Bool __tmp_128; __tmp_128 = main__c1; _Bool assert__arg; assert__arg = __tmp_128; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_41350; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_41424:; p5_new = node5____CPAchecker_TMP_1; goto label_41352; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_41424; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41411 = check__tmp; main__c1 = __return_41411; { _Bool __tmp_129; __tmp_129 = main__c1; _Bool assert__arg; assert__arg = __tmp_129; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_41255:; p5_new = node5____CPAchecker_TMP_0; label_41257:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41280 = check__tmp; main__c1 = __return_41280; { _Bool __tmp_130; __tmp_130 = main__c1; _Bool assert__arg; assert__arg = __tmp_130; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_41255; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_41329:; p5_new = node5____CPAchecker_TMP_1; goto label_41257; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_41329; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41316 = check__tmp; main__c1 = __return_41316; { _Bool __tmp_131; __tmp_131 = main__c1; _Bool assert__arg; assert__arg = __tmp_131; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_41524:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_41541:; p5_new = node5____CPAchecker_TMP_0; label_41543:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41566 = check__tmp; main__c1 = __return_41566; { _Bool __tmp_132; __tmp_132 = main__c1; _Bool assert__arg; assert__arg = __tmp_132; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_41541; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_41615:; p5_new = node5____CPAchecker_TMP_1; goto label_41543; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_41615; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41602 = check__tmp; main__c1 = __return_41602; { _Bool __tmp_133; __tmp_133 = main__c1; _Bool assert__arg; assert__arg = __tmp_133; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_41524; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_41444:; p5_new = node5____CPAchecker_TMP_0; label_41446:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41469 = check__tmp; main__c1 = __return_41469; { _Bool __tmp_134; __tmp_134 = main__c1; _Bool assert__arg; assert__arg = __tmp_134; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_41444; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_41518:; p5_new = node5____CPAchecker_TMP_1; goto label_41446; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_41518; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41505 = check__tmp; main__c1 = __return_41505; { _Bool __tmp_135; __tmp_135 = main__c1; _Bool assert__arg; assert__arg = __tmp_135; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } else { return __return_main; } } else { node3____CPAchecker_TMP_0 = p3_new; p3_new = node3____CPAchecker_TMP_0; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_40951:; p5_new = node5____CPAchecker_TMP_0; label_40953:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40976 = check__tmp; main__c1 = __return_40976; { _Bool __tmp_136; __tmp_136 = main__c1; _Bool assert__arg; assert__arg = __tmp_136; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_40951; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_41025:; p5_new = node5____CPAchecker_TMP_1; goto label_40953; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_41025; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41012 = check__tmp; main__c1 = __return_41012; { _Bool __tmp_137; __tmp_137 = main__c1; _Bool assert__arg; assert__arg = __tmp_137; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_40856:; p5_new = node5____CPAchecker_TMP_0; label_40858:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40881 = check__tmp; main__c1 = __return_40881; { _Bool __tmp_138; __tmp_138 = main__c1; _Bool assert__arg; assert__arg = __tmp_138; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_40856; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_40930:; p5_new = node5____CPAchecker_TMP_1; goto label_40858; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_40930; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_40917 = check__tmp; main__c1 = __return_40917; { _Bool __tmp_139; __tmp_139 = main__c1; _Bool assert__arg; assert__arg = __tmp_139; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_41125:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_41142:; p5_new = node5____CPAchecker_TMP_0; label_41144:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41167 = check__tmp; main__c1 = __return_41167; { _Bool __tmp_140; __tmp_140 = main__c1; _Bool assert__arg; assert__arg = __tmp_140; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_41142; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_41216:; p5_new = node5____CPAchecker_TMP_1; goto label_41144; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_41216; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41203 = check__tmp; main__c1 = __return_41203; { _Bool __tmp_141; __tmp_141 = main__c1; _Bool assert__arg; assert__arg = __tmp_141; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_41125; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_41045:; p5_new = node5____CPAchecker_TMP_0; label_41047:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41070 = check__tmp; main__c1 = __return_41070; { _Bool __tmp_142; __tmp_142 = main__c1; _Bool assert__arg; assert__arg = __tmp_142; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_41045; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_41119:; p5_new = node5____CPAchecker_TMP_1; goto label_41047; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_41119; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41106 = check__tmp; main__c1 = __return_41106; { _Bool __tmp_143; __tmp_143 = main__c1; _Bool assert__arg; assert__arg = __tmp_143; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } } else { if (((int)send3) != ((int)id3)) { int node3____CPAchecker_TMP_1; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_1 = send3; p3_new = node3____CPAchecker_TMP_1; goto label_41223; } else { return __return_main; } } else { node3____CPAchecker_TMP_1 = p3_new; p3_new = node3____CPAchecker_TMP_1; label_41621:; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { if (!(alive4 == 0)) { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_41748:; p5_new = node5____CPAchecker_TMP_0; label_41750:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41773 = check__tmp; main__c1 = __return_41773; { _Bool __tmp_144; __tmp_144 = main__c1; _Bool assert__arg; assert__arg = __tmp_144; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_41748; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_41822:; p5_new = node5____CPAchecker_TMP_1; goto label_41750; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_41822; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41809 = check__tmp; main__c1 = __return_41809; { _Bool __tmp_145; __tmp_145 = main__c1; _Bool assert__arg; assert__arg = __tmp_145; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_0 = p4_new; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_41653:; p5_new = node5____CPAchecker_TMP_0; label_41655:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41678 = check__tmp; main__c1 = __return_41678; { _Bool __tmp_146; __tmp_146 = main__c1; _Bool assert__arg; assert__arg = __tmp_146; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_41653; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_41727:; p5_new = node5____CPAchecker_TMP_1; goto label_41655; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_41727; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41714 = check__tmp; main__c1 = __return_41714; { _Bool __tmp_147; __tmp_147 = main__c1; _Bool assert__arg; assert__arg = __tmp_147; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } else { if (((int)send4) != ((int)id4)) { int node4____CPAchecker_TMP_1; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_1 = send4; label_41922:; p4_new = node4____CPAchecker_TMP_1; mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_41939:; p5_new = node5____CPAchecker_TMP_0; label_41941:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41964 = check__tmp; main__c1 = __return_41964; { _Bool __tmp_148; __tmp_148 = main__c1; _Bool assert__arg; assert__arg = __tmp_148; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_41939; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_42013:; p5_new = node5____CPAchecker_TMP_1; goto label_41941; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_42013; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_42000 = check__tmp; main__c1 = __return_42000; { _Bool __tmp_149; __tmp_149 = main__c1; _Bool assert__arg; assert__arg = __tmp_149; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } else { return __return_main; } } else { node4____CPAchecker_TMP_1 = p4_new; goto label_41922; } } else { mode4 = 1; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { return __return_main; } else { if (!(alive5 == 0)) { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_41842:; p5_new = node5____CPAchecker_TMP_0; label_41844:; mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41867 = check__tmp; main__c1 = __return_41867; { _Bool __tmp_150; __tmp_150 = main__c1; _Bool assert__arg; assert__arg = __tmp_150; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; goto label_41842; } } else { if (((int)send5) != ((int)id5)) { int node5____CPAchecker_TMP_1; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_1 = send5; label_41916:; p5_new = node5____CPAchecker_TMP_1; goto label_41844; } else { return __return_main; } } else { node5____CPAchecker_TMP_1 = p5_new; goto label_41916; } } else { mode5 = 1; p1_old = p1_new; p1_new = nomsg; p2_old = p2_new; p2_new = nomsg; p3_old = p3_new; p3_new = nomsg; p4_old = p4_new; p4_new = nomsg; p5_old = p5_new; p5_new = nomsg; { int check__tmp; if (((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) <= 1) { if (((int)r1) < 5) { check__tmp = 1; __return_41903 = check__tmp; main__c1 = __return_41903; { _Bool __tmp_151; __tmp_151 = main__c1; _Bool assert__arg; assert__arg = __tmp_151; if (assert__arg == 0) { return __return_main; } else { int main____CPAchecker_TMP_0 = main__i2; main__i2 = main__i2 + 1; __tmp_33147_0 = main____CPAchecker_TMP_0; goto label_33147; } } } else { return __return_main; } } else { return __return_main; } } } } } } } } } } } } else { goto label_41621; } } } } } } else { goto label_40807; } } } } } } } } else { 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; } } }