// 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.6.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c", 4, "reach_error"); } _Bool __VERIFIER_nondet_bool(); char __VERIFIER_nondet_char(); unsigned char __VERIFIER_nondet_uchar(); 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; unsigned 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; 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; 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; 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; 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; port_t p6 = 0; char p6_old = '\x0'; char p6_new = '\x0'; char id6 = '\x0'; char st6 = '\x0'; msg_t send6 = '\x0'; _Bool mode6 = 0; void node1(); void node2(); void node3(); void node4(); void node5(); void node6(); void (*nodes[6])() = { &node1, &node2, &node3, &node4, &node5, &node6 }; int init(); int check(); int main(); int __return_13205; int __return_19489; int __return_13439; int __return_13554; int __return_13888; int __return_14089; int __return_14273; int __return_14494; int __return_14690; int __return_14882; int __return_15060; int __return_15279; int __return_15487; int __return_15679; int __return_15857; int __return_16047; int __return_16237; int __return_16401; int __return_16772; int __return_16990; int __return_17180; int __return_17356; int __return_17558; int __return_17746; int __return_17922; int __return_18290; int __return_18490; int __return_18666; int __return_19008; int __return_13793; int __return_13966; int __return_14179; int __return_14353; int __return_14596; int __return_14770; int __return_14974; int __return_15393; int __return_15567; int __return_15771; int __return_16151; int __return_16898; int __return_17068; int __return_17270; int __return_17660; int __return_18404; int __return_19439; int __return_19361; int __return_19285; int __return_19207; int __return_19143; int __return_19041; int __return_18945; int __return_18853; int __return_18789; int __return_18699; int __return_18615; int __return_18523; int __return_18451; int __return_18329; int __return_18215; int __return_18109; int __return_18045; int __return_17955; int __return_17871; int __return_17779; int __return_17707; int __return_17597; int __return_17495; int __return_17389; int __return_17317; int __return_17219; int __return_17129; int __return_17029; int __return_16951; int __return_16811; int __return_16682; int __return_16564; int __return_16512; int __return_16434; int __return_16350; int __return_16270; int __return_16198; int __return_16088; int __return_15984; int __return_15890; int __return_15818; int __return_15720; int __return_15628; int __return_15528; int __return_15448; int __return_15318; int __return_15201; int __return_15093; int __return_15021; int __return_14923; int __return_14831; int __return_14731; int __return_14651; int __return_14533; int __return_14428; int __return_14314; int __return_14234; int __return_14128; int __return_14035; int __return_13927; int __return_13846; int __return_13690; int __return_13332; int main() { int main__c1; int main__i2; main__c1 = 0; r1 = __VERIFIER_nondet_uchar(); id1 = __VERIFIER_nondet_char(); st1 = __VERIFIER_nondet_char(); send1 = __VERIFIER_nondet_char(); mode1 = __VERIFIER_nondet_bool(); id2 = __VERIFIER_nondet_char(); st2 = __VERIFIER_nondet_char(); send2 = __VERIFIER_nondet_char(); mode2 = __VERIFIER_nondet_bool(); id3 = __VERIFIER_nondet_char(); st3 = __VERIFIER_nondet_char(); send3 = __VERIFIER_nondet_char(); mode3 = __VERIFIER_nondet_bool(); id4 = __VERIFIER_nondet_char(); st4 = __VERIFIER_nondet_char(); send4 = __VERIFIER_nondet_char(); mode4 = __VERIFIER_nondet_bool(); id5 = __VERIFIER_nondet_char(); st5 = __VERIFIER_nondet_char(); send5 = __VERIFIER_nondet_char(); mode5 = __VERIFIER_nondet_bool(); id6 = __VERIFIER_nondet_char(); st6 = __VERIFIER_nondet_char(); send6 = __VERIFIER_nondet_char(); mode6 = __VERIFIER_nondet_bool(); { int init__tmp; if (((int)r1) == 0) { 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)id6) >= 0) { if (((int)st6) == 0) { if (((int)send6) == ((int)id6)) { if (((int)mode6) == 0) { if (((int)id1) != ((int)id2)) { if (((int)id1) != ((int)id3)) { if (((int)id1) != ((int)id4)) { if (((int)id1) != ((int)id5)) { if (((int)id1) != ((int)id6)) { if (((int)id2) != ((int)id3)) { if (((int)id2) != ((int)id4)) { if (((int)id2) != ((int)id5)) { if (((int)id2) != ((int)id6)) { if (((int)id3) != ((int)id4)) { if (((int)id3) != ((int)id5)) { if (((int)id3) != ((int)id6)) { if (((int)id4) != ((int)id5)) { if (((int)id4) != ((int)id6)) { if (((int)id5) != ((int)id6)) { init__tmp = 1; __return_13205 = init__tmp; main__i2 = __return_13205; 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; p6_old = nomsg; p6_new = nomsg; main__i2 = 0; { msg_t node1__m1; node1__m1 = nomsg; if (!(mode1 == 0)) { return __return_main; } else { int node1____CPAchecker_TMP_0; if (send1 != nomsg) { if (p1_new == nomsg) { node1____CPAchecker_TMP_0 = send1; p1_new = node1____CPAchecker_TMP_0; mode1 = 1; { msg_t node2__m2; node2__m2 = nomsg; if (!(mode2 == 0)) { return __return_main; } else { int node2____CPAchecker_TMP_0; if (send2 != nomsg) { if (p2_new == nomsg) { node2____CPAchecker_TMP_0 = send2; p2_new = node2____CPAchecker_TMP_0; mode2 = 1; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { return __return_main; } else { int node3____CPAchecker_TMP_0; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_0 = send3; p3_new = node3____CPAchecker_TMP_0; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_19489 = check__tmp; main__c1 = __return_19489; { _Bool __tmp_1; __tmp_1 = main__c1; _Bool assert__arg; assert__arg = __tmp_1; if (assert__arg == 0) { return __return_main; } else { label_13339:; { msg_t node1__m1; node1__m1 = nomsg; if (!(mode1 == 0)) { if (r1 == 255) { return __return_main; } else { r1 = r1 + 1; node1__m1 = p6_old; p6_old = nomsg; if (((int)node1__m1) != ((int)nomsg)) { if (((int)node1__m1) > ((int)id1)) { send1 = node1__m1; label_13703:; mode1 = 0; label_13353:; { msg_t node2__m2; node2__m2 = nomsg; if (!(mode2 == 0)) { node2__m2 = p1_old; p1_old = nomsg; if (((int)node2__m2) != ((int)nomsg)) { if (((int)node2__m2) > ((int)id2)) { send2 = node2__m2; label_16694:; mode2 = 0; label_13365:; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { node3__m3 = p2_old; p2_old = nomsg; if (((int)node3__m3) != ((int)nomsg)) { if (((int)node3__m3) > ((int)id3)) { send3 = node3__m3; label_15213:; mode3 = 0; label_13377:; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { node4__m4 = p3_old; p3_old = nomsg; if (((int)node4__m4) != ((int)nomsg)) { if (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_14440:; mode4 = 0; label_13389:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_14047:; mode5 = 0; label_13401:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_13858:; mode6 = 0; label_13413:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_13439 = check__tmp; main__c1 = __return_13439; { _Bool __tmp_2; __tmp_2 = main__c1; _Bool assert__arg; assert__arg = __tmp_2; if (assert__arg == 0) { return __return_main; } else { label_13446:; { msg_t node1__m1; node1__m1 = nomsg; if (!(mode1 == 0)) { if (r1 == 255) { r1 = 5; label_13455:; r1 = r1 + 1; node1__m1 = p6_old; p6_old = nomsg; if (((int)node1__m1) != ((int)nomsg)) { if (((int)node1__m1) > ((int)id1)) { send1 = node1__m1; label_13460:; mode1 = 0; label_13462:; { msg_t node2__m2; node2__m2 = nomsg; if (!(mode2 == 0)) { node2__m2 = p1_old; p1_old = nomsg; if (((int)node2__m2) != ((int)nomsg)) { if (((int)node2__m2) > ((int)id2)) { send2 = node2__m2; label_13474:; mode2 = 0; label_13476:; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { node3__m3 = p2_old; p2_old = nomsg; if (((int)node3__m3) != ((int)nomsg)) { if (((int)node3__m3) > ((int)id3)) { send3 = node3__m3; label_13488:; mode3 = 0; label_13490:; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { node4__m4 = p3_old; p3_old = nomsg; if (((int)node4__m4) != ((int)nomsg)) { if (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_13502:; mode4 = 0; label_13504:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_13516:; mode5 = 0; label_13518:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_13530:; mode6 = 0; label_13532:; label_13534:; 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; p6_old = p6_new; p6_new = nomsg; label_13546:; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { label_13570:; if (((int)r1) < 6) { check__tmp = 1; label_13576:; label_13569:; label_13553:; __return_13554 = check__tmp; main__c1 = __return_13554; label_13555:; { _Bool __tmp_3; __tmp_3 = main__c1; _Bool assert__arg; assert__arg = __tmp_3; if (assert__arg == 0) { {reach_error();} return __return_main; } else { label_13561:; goto label_13446; } } } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 1) { check__tmp = 1; goto label_13576; } else { check__tmp = 0; goto label_13576; } } } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { goto label_13570; } else { check__tmp = 0; goto label_13569; } } } else { check__tmp = 0; goto label_13553; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; goto label_13530; } else { goto label_13530; } } } else { goto label_13530; } } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; label_13588:; p6_new = node6____CPAchecker_TMP_0; mode6 = 1; goto label_13532; } else { label_13587:; node6____CPAchecker_TMP_0 = p6_new; goto label_13588; } } else { goto label_13587; } } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; goto label_13516; } else { goto label_13516; } } } else { goto label_13516; } } else { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; label_13601:; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; goto label_13518; } else { label_13600:; node5____CPAchecker_TMP_0 = p5_new; goto label_13601; } } else { goto label_13600; } } } } else { if (((int)node4__m4) == ((int)id4)) { st4 = 1; goto label_13502; } else { goto label_13502; } } } else { goto label_13502; } } else { int node4____CPAchecker_TMP_0; if (send4 != nomsg) { if (p4_new == nomsg) { node4____CPAchecker_TMP_0 = send4; label_13614:; p4_new = node4____CPAchecker_TMP_0; mode4 = 1; goto label_13504; } else { label_13613:; node4____CPAchecker_TMP_0 = p4_new; goto label_13614; } } else { goto label_13613; } } } } else { if (((int)node3__m3) == ((int)id3)) { st3 = 1; goto label_13488; } else { goto label_13488; } } } else { goto label_13488; } } else { int node3____CPAchecker_TMP_0; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_0 = send3; label_13627:; p3_new = node3____CPAchecker_TMP_0; mode3 = 1; goto label_13490; } else { label_13626:; node3____CPAchecker_TMP_0 = p3_new; goto label_13627; } } else { goto label_13626; } } } } else { if (((int)node2__m2) == ((int)id2)) { st2 = 1; goto label_13474; } else { goto label_13474; } } } else { goto label_13474; } } else { int node2____CPAchecker_TMP_0; if (send2 != nomsg) { if (p2_new == nomsg) { node2____CPAchecker_TMP_0 = send2; label_13640:; p2_new = node2____CPAchecker_TMP_0; mode2 = 1; goto label_13476; } else { label_13639:; node2____CPAchecker_TMP_0 = p2_new; goto label_13640; } } else { goto label_13639; } } } } else { if (((int)node1__m1) == ((int)id1)) { st1 = 1; goto label_13460; } else { send1 = node1__m1; goto label_13460; } } } else { goto label_13460; } } else { goto label_13455; } } else { int node1____CPAchecker_TMP_0; if (send1 != nomsg) { if (p1_new == nomsg) { node1____CPAchecker_TMP_0 = send1; label_13655:; p1_new = node1____CPAchecker_TMP_0; mode1 = 1; goto label_13462; } else { label_13654:; node1____CPAchecker_TMP_0 = p1_new; goto label_13655; } } else { goto label_13654; } } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { return __return_main; } else { check__tmp = 0; __return_13888 = check__tmp; main__c1 = __return_13888; { _Bool __tmp_4; __tmp_4 = main__c1; _Bool assert__arg; assert__arg = __tmp_4; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { return __return_main; } } } else { goto label_13858; } } } else { mode6 = 0; goto label_13413; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_14246:; mode6 = 0; label_14066:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { return __return_main; } else { check__tmp = 0; __return_14089 = check__tmp; main__c1 = __return_14089; { _Bool __tmp_5; __tmp_5 = main__c1; _Bool assert__arg; assert__arg = __tmp_5; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { return __return_main; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_14273 = check__tmp; main__c1 = __return_14273; { _Bool __tmp_6; __tmp_6 = main__c1; _Bool assert__arg; assert__arg = __tmp_6; if (assert__arg == 0) { {reach_error();} return __return_main; } else { goto label_13561; } } } } } else { goto label_14246; } } } else { mode6 = 0; goto label_14066; } } else { return __return_main; } } } else { goto label_14047; } } } else { mode5 = 0; goto label_13401; } } 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 (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_14843:; mode5 = 0; label_14459:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_14663:; mode6 = 0; label_14471:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { return __return_main; } else { check__tmp = 0; __return_14494 = check__tmp; main__c1 = __return_14494; { _Bool __tmp_7; __tmp_7 = main__c1; _Bool assert__arg; assert__arg = __tmp_7; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { return __return_main; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_14690 = check__tmp; main__c1 = __return_14690; { _Bool __tmp_8; __tmp_8 = main__c1; _Bool assert__arg; assert__arg = __tmp_8; if (assert__arg == 0) { {reach_error();} return __return_main; } else { goto label_13561; } } } } } else { goto label_14663; } } } else { mode6 = 0; goto label_14471; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_15033:; mode6 = 0; label_14862:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_14882 = check__tmp; main__c1 = __return_14882; { _Bool __tmp_9; __tmp_9 = main__c1; _Bool assert__arg; assert__arg = __tmp_9; if (assert__arg == 0) { {reach_error();} return __return_main; } else { goto label_13561; } } } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_15060 = check__tmp; main__c1 = __return_15060; goto label_13555; } } } else { goto label_15033; } } } else { mode6 = 0; goto label_14862; } } else { return __return_main; } } } else { goto label_14843; } } } else { mode5 = 0; goto label_14459; } } else { return __return_main; } } } else { goto label_14440; } } } else { mode4 = 0; goto label_13389; } } 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 (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_15996:; mode4 = 0; label_15232:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_15640:; mode5 = 0; label_15244:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_15460:; mode6 = 0; label_15256:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { return __return_main; } else { check__tmp = 0; __return_15279 = check__tmp; main__c1 = __return_15279; { _Bool __tmp_10; __tmp_10 = main__c1; _Bool assert__arg; assert__arg = __tmp_10; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { return __return_main; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_15487 = check__tmp; main__c1 = __return_15487; { _Bool __tmp_11; __tmp_11 = main__c1; _Bool assert__arg; assert__arg = __tmp_11; if (assert__arg == 0) { {reach_error();} return __return_main; } else { goto label_13561; } } } } } else { goto label_15460; } } } else { mode6 = 0; goto label_15256; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_15830:; mode6 = 0; label_15659:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_15679 = check__tmp; main__c1 = __return_15679; { _Bool __tmp_12; __tmp_12 = main__c1; _Bool assert__arg; assert__arg = __tmp_12; if (assert__arg == 0) { {reach_error();} return __return_main; } else { goto label_13561; } } } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_15857 = check__tmp; main__c1 = __return_15857; goto label_13555; } } } else { goto label_15830; } } } else { mode6 = 0; goto label_15659; } } else { return __return_main; } } } else { goto label_15640; } } } else { mode5 = 0; goto label_15244; } } 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 (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_16362:; mode5 = 0; label_16015:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_16210:; mode6 = 0; label_16027:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_16047 = check__tmp; main__c1 = __return_16047; { _Bool __tmp_13; __tmp_13 = main__c1; _Bool assert__arg; assert__arg = __tmp_13; if (assert__arg == 0) { {reach_error();} return __return_main; } else { goto label_13561; } } } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_16237 = check__tmp; main__c1 = __return_16237; goto label_13555; } } } else { goto label_16210; } } } else { mode6 = 0; goto label_16027; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_16524:; mode6 = 0; label_16381:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_16401 = check__tmp; main__c1 = __return_16401; goto label_13555; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 0; goto label_13534; } else { goto label_16524; } } } else { mode6 = 0; goto label_16381; } } else { return __return_main; } } } else { goto label_16362; } } } else { mode5 = 0; goto label_16015; } } else { return __return_main; } } } else { goto label_15996; } } } else { mode4 = 0; goto label_15232; } } else { return __return_main; } } } else { goto label_15213; } } } else { mode3 = 0; goto label_13377; } } 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 (((int)node3__m3) > ((int)id3)) { send3 = node3__m3; label_18227:; mode3 = 0; label_16713:; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { node4__m4 = p3_old; p3_old = nomsg; if (((int)node4__m4) != ((int)nomsg)) { if (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_17507:; mode4 = 0; label_16725:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_17141:; mode5 = 0; label_16737:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_16963:; mode6 = 0; label_16749:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { return __return_main; } else { check__tmp = 0; __return_16772 = check__tmp; main__c1 = __return_16772; { _Bool __tmp_14; __tmp_14 = main__c1; _Bool assert__arg; assert__arg = __tmp_14; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { return __return_main; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_16990 = check__tmp; main__c1 = __return_16990; { _Bool __tmp_15; __tmp_15 = main__c1; _Bool assert__arg; assert__arg = __tmp_15; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { goto label_16963; } } } else { mode6 = 0; goto label_16749; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_17329:; mode6 = 0; label_17160:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_17180 = check__tmp; main__c1 = __return_17180; { _Bool __tmp_16; __tmp_16 = main__c1; _Bool assert__arg; assert__arg = __tmp_16; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_17356 = check__tmp; main__c1 = __return_17356; goto label_13555; } } } else { goto label_17329; } } } else { mode6 = 0; goto label_17160; } } else { return __return_main; } } } else { goto label_17141; } } } else { mode5 = 0; goto label_16737; } } 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 (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_17883:; mode5 = 0; label_17526:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_17719:; mode6 = 0; label_17538:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_17558 = check__tmp; main__c1 = __return_17558; { _Bool __tmp_17; __tmp_17 = main__c1; _Bool assert__arg; assert__arg = __tmp_17; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_17746 = check__tmp; main__c1 = __return_17746; goto label_13555; } } } else { goto label_17719; } } } else { mode6 = 0; goto label_17538; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_18057:; mode6 = 0; label_17902:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_17922 = check__tmp; main__c1 = __return_17922; goto label_13555; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; goto label_13546; } else { goto label_18057; } } } else { mode6 = 0; goto label_17902; } } else { return __return_main; } } } else { goto label_17883; } } } else { mode5 = 0; goto label_17526; } } else { return __return_main; } } } else { goto label_17507; } } } else { mode4 = 0; goto label_16725; } } 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 (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_18957:; mode4 = 0; label_18246:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_18627:; mode5 = 0; label_18258:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_18463:; mode6 = 0; label_18270:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_18290 = check__tmp; main__c1 = __return_18290; { _Bool __tmp_18; __tmp_18 = main__c1; _Bool assert__arg; assert__arg = __tmp_18; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_18490 = check__tmp; main__c1 = __return_18490; goto label_13555; } } } else { goto label_18463; } } } else { mode6 = 0; goto label_18270; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_18801:; mode6 = 0; label_18646:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_18666 = check__tmp; main__c1 = __return_18666; goto label_13555; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; goto label_13546; } else { goto label_18801; } } } else { mode6 = 0; goto label_18646; } } else { return __return_main; } } } else { goto label_18627; } } } else { mode5 = 0; goto label_18258; } } 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 (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_19297:; mode5 = 0; label_18976:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_19155:; mode6 = 0; label_18988:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_19008 = check__tmp; main__c1 = __return_19008; goto label_13555; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; goto label_13546; } else { goto label_19155; } } } else { mode6 = 0; goto label_18988; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_19451:; mode6 = 0; label_19452:; goto label_13534; } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 0; goto label_19452; } else { goto label_19451; } } } else { mode6 = 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; p6_old = p6_new; p6_new = nomsg; goto label_13546; } } else { return __return_main; } } } else { goto label_19297; } } } else { mode5 = 0; goto label_18976; } } else { return __return_main; } } } else { goto label_18957; } } } else { mode4 = 0; goto label_18246; } } else { return __return_main; } } } else { goto label_18227; } } } else { mode3 = 0; goto label_16713; } } else { return __return_main; } } } else { goto label_16694; } } } else { mode2 = 0; goto label_13365; } } 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 (((int)node2__m2) > ((int)id2)) { send2 = node2__m2; label_16823:; mode2 = 0; label_13722:; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { node3__m3 = p2_old; p2_old = nomsg; if (((int)node3__m3) != ((int)nomsg)) { if (((int)node3__m3) > ((int)id3)) { send3 = node3__m3; label_15330:; mode3 = 0; label_13734:; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { node4__m4 = p3_old; p3_old = nomsg; if (((int)node4__m4) != ((int)nomsg)) { if (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_14545:; mode4 = 0; label_13746:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_14140:; mode5 = 0; label_13758:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_13939:; mode6 = 0; label_13770:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { return __return_main; } else { check__tmp = 0; __return_13793 = check__tmp; main__c1 = __return_13793; { _Bool __tmp_19; __tmp_19 = main__c1; _Bool assert__arg; assert__arg = __tmp_19; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { return __return_main; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_13966 = check__tmp; main__c1 = __return_13966; { _Bool __tmp_20; __tmp_20 = main__c1; _Bool assert__arg; assert__arg = __tmp_20; if (assert__arg == 0) { {reach_error();} return __return_main; } else { goto label_13561; } } } } } else { goto label_13939; } } } else { mode6 = 0; goto label_13770; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_14326:; mode6 = 0; label_14159:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_14179 = check__tmp; main__c1 = __return_14179; { _Bool __tmp_21; __tmp_21 = main__c1; _Bool assert__arg; assert__arg = __tmp_21; if (assert__arg == 0) { {reach_error();} return __return_main; } else { goto label_13561; } } } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_14353 = check__tmp; main__c1 = __return_14353; goto label_13555; } } } else { goto label_14326; } } } else { mode6 = 0; goto label_14159; } } else { return __return_main; } } } else { goto label_14140; } } } else { mode5 = 0; goto label_13758; } } 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 (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_14935:; mode5 = 0; label_14564:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_14743:; mode6 = 0; label_14576:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_14596 = check__tmp; main__c1 = __return_14596; { _Bool __tmp_22; __tmp_22 = main__c1; _Bool assert__arg; assert__arg = __tmp_22; if (assert__arg == 0) { {reach_error();} return __return_main; } else { goto label_13561; } } } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_14770 = check__tmp; main__c1 = __return_14770; goto label_13555; } } } else { goto label_14743; } } } else { mode6 = 0; goto label_14576; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_15105:; mode6 = 0; label_14954:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_14974 = check__tmp; main__c1 = __return_14974; goto label_13555; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 0; goto label_13534; } else { goto label_15105; } } } else { mode6 = 0; goto label_14954; } } else { return __return_main; } } } else { goto label_14935; } } } else { mode5 = 0; goto label_14564; } } else { return __return_main; } } } else { goto label_14545; } } } else { mode4 = 0; goto label_13746; } } 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 (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_16100:; mode4 = 0; label_15349:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_15732:; mode5 = 0; label_15361:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_15540:; mode6 = 0; label_15373:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_15393 = check__tmp; main__c1 = __return_15393; { _Bool __tmp_23; __tmp_23 = main__c1; _Bool assert__arg; assert__arg = __tmp_23; if (assert__arg == 0) { {reach_error();} return __return_main; } else { goto label_13561; } } } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_15567 = check__tmp; main__c1 = __return_15567; goto label_13555; } } } else { goto label_15540; } } } else { mode6 = 0; goto label_15373; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_15902:; mode6 = 0; label_15751:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_15771 = check__tmp; main__c1 = __return_15771; goto label_13555; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 0; goto label_13534; } else { goto label_15902; } } } else { mode6 = 0; goto label_15751; } } else { return __return_main; } } } else { goto label_15732; } } } else { mode5 = 0; goto label_15361; } } 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 (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_16446:; mode5 = 0; label_16119:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_16282:; mode6 = 0; label_16131:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_16151 = check__tmp; main__c1 = __return_16151; goto label_13555; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 0; goto label_13534; } else { goto label_16282; } } } else { mode6 = 0; goto label_16131; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_16576:; mode6 = 0; label_16465:; goto label_13534; } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; goto label_16576; } else { goto label_16576; } } } else { mode6 = 0; goto label_16465; } } else { return __return_main; } } } else { goto label_16446; } } } else { mode5 = 0; goto label_16119; } } else { return __return_main; } } } else { goto label_16100; } } } else { mode4 = 0; goto label_15349; } } else { return __return_main; } } } else { goto label_15330; } } } else { mode3 = 0; goto label_13734; } } 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 (((int)node3__m3) > ((int)id3)) { send3 = node3__m3; label_18341:; mode3 = 0; label_16842:; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { node4__m4 = p3_old; p3_old = nomsg; if (((int)node4__m4) != ((int)nomsg)) { if (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_17609:; mode4 = 0; label_16854:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_17231:; mode5 = 0; label_16866:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_17041:; mode6 = 0; label_16878:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_16898 = check__tmp; main__c1 = __return_16898; { _Bool __tmp_24; __tmp_24 = main__c1; _Bool assert__arg; assert__arg = __tmp_24; if (assert__arg == 0) { {reach_error();} return __return_main; } else { return __return_main; } } } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_17068 = check__tmp; main__c1 = __return_17068; goto label_13555; } } } else { goto label_17041; } } } else { mode6 = 0; goto label_16878; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_17401:; mode6 = 0; label_17250:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_17270 = check__tmp; main__c1 = __return_17270; goto label_13555; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; goto label_13546; } else { goto label_17401; } } } else { mode6 = 0; goto label_17250; } } else { return __return_main; } } } else { goto label_17231; } } } else { mode5 = 0; goto label_16866; } } 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 (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_17967:; mode5 = 0; label_17628:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_17791:; mode6 = 0; label_17640:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_17660 = check__tmp; main__c1 = __return_17660; goto label_13555; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; goto label_13546; } else { goto label_17791; } } } else { mode6 = 0; goto label_17640; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_18121:; mode6 = 0; label_18122:; goto label_13534; } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 0; goto label_18122; } else { goto label_18121; } } } else { mode6 = 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; p6_old = p6_new; p6_new = nomsg; goto label_13546; } } else { return __return_main; } } } else { goto label_17967; } } } else { mode5 = 0; goto label_17628; } } else { return __return_main; } } } else { goto label_17609; } } } else { mode4 = 0; goto label_16854; } } 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 (((int)node4__m4) > ((int)id4)) { send4 = node4__m4; label_19053:; mode4 = 0; label_18360:; { msg_t node5__m5; node5__m5 = nomsg; if (!(mode5 == 0)) { node5__m5 = p4_old; p4_old = nomsg; if (((int)node5__m5) != ((int)nomsg)) { if (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_18711:; mode5 = 0; label_18372:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_18535:; mode6 = 0; label_18384:; 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { return __return_main; } else { check__tmp = 0; __return_18404 = check__tmp; main__c1 = __return_18404; goto label_13555; } } } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 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; p6_old = p6_new; p6_new = nomsg; goto label_13546; } else { goto label_18535; } } } else { mode6 = 0; goto label_18384; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_18865:; mode6 = 0; label_18866:; goto label_13534; } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 0; goto label_18866; } else { goto label_18865; } } } else { mode6 = 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; p6_old = p6_new; p6_new = nomsg; goto label_13546; } } else { return __return_main; } } } else { goto label_18711; } } } else { mode5 = 0; goto label_18372; } } 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 (((int)node5__m5) > ((int)id5)) { send5 = node5__m5; label_19373:; mode5 = 0; label_19072:; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_19219:; mode6 = 0; label_19220:; goto label_13534; } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; mode6 = 0; goto label_19220; } else { goto label_19219; } } } else { mode6 = 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; p6_old = p6_new; p6_new = nomsg; goto label_13546; } } else { return __return_main; } } } else { if (((int)node5__m5) == ((int)id5)) { st5 = 1; mode5 = 0; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { node6__m6 = p5_old; p5_old = nomsg; if (((int)node6__m6) != ((int)nomsg)) { if (((int)node6__m6) > ((int)id6)) { send6 = node6__m6; label_19389:; mode6 = 0; goto label_13534; } else { if (((int)node6__m6) == ((int)id6)) { st6 = 1; goto label_19389; } else { goto label_19389; } } } else { goto label_19389; } } else { return __return_main; } } } else { goto label_19373; } } } else { mode5 = 0; goto label_19072; } } else { return __return_main; } } } else { goto label_19053; } } } else { mode4 = 0; goto label_18360; } } else { return __return_main; } } } else { goto label_18341; } } } else { mode3 = 0; goto label_16842; } } else { return __return_main; } } } else { goto label_16823; } } } else { mode2 = 0; goto label_13722; } } else { return __return_main; } } } else { send1 = node1__m1; goto label_13703; } } } else { mode1 = 0; goto label_13353; } } } else { return __return_main; } } } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_19439 = check__tmp; main__c1 = __return_19439; { _Bool __tmp_25; __tmp_25 = main__c1; _Bool assert__arg; assert__arg = __tmp_25; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_19361 = check__tmp; main__c1 = __return_19361; { _Bool __tmp_26; __tmp_26 = main__c1; _Bool assert__arg; assert__arg = __tmp_26; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_19285 = check__tmp; main__c1 = __return_19285; { _Bool __tmp_27; __tmp_27 = main__c1; _Bool assert__arg; assert__arg = __tmp_27; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_19207 = check__tmp; main__c1 = __return_19207; { _Bool __tmp_28; __tmp_28 = main__c1; _Bool assert__arg; assert__arg = __tmp_28; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_19143 = check__tmp; main__c1 = __return_19143; { _Bool __tmp_29; __tmp_29 = main__c1; _Bool assert__arg; assert__arg = __tmp_29; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_19041 = check__tmp; main__c1 = __return_19041; { _Bool __tmp_30; __tmp_30 = main__c1; _Bool assert__arg; assert__arg = __tmp_30; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_18945 = check__tmp; main__c1 = __return_18945; { _Bool __tmp_31; __tmp_31 = main__c1; _Bool assert__arg; assert__arg = __tmp_31; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } 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 { 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_18853 = check__tmp; main__c1 = __return_18853; { _Bool __tmp_32; __tmp_32 = main__c1; _Bool assert__arg; assert__arg = __tmp_32; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_18789 = check__tmp; main__c1 = __return_18789; { _Bool __tmp_33; __tmp_33 = main__c1; _Bool assert__arg; assert__arg = __tmp_33; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_18699 = check__tmp; main__c1 = __return_18699; { _Bool __tmp_34; __tmp_34 = main__c1; _Bool assert__arg; assert__arg = __tmp_34; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_18615 = check__tmp; main__c1 = __return_18615; { _Bool __tmp_35; __tmp_35 = main__c1; _Bool assert__arg; assert__arg = __tmp_35; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_18523 = check__tmp; main__c1 = __return_18523; { _Bool __tmp_36; __tmp_36 = main__c1; _Bool assert__arg; assert__arg = __tmp_36; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_18451 = check__tmp; main__c1 = __return_18451; { _Bool __tmp_37; __tmp_37 = main__c1; _Bool assert__arg; assert__arg = __tmp_37; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_18329 = check__tmp; main__c1 = __return_18329; { _Bool __tmp_38; __tmp_38 = main__c1; _Bool assert__arg; assert__arg = __tmp_38; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_18215 = check__tmp; main__c1 = __return_18215; { _Bool __tmp_39; __tmp_39 = main__c1; _Bool assert__arg; assert__arg = __tmp_39; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } } } } } } } } } } 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 { int node3____CPAchecker_TMP_0; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_0 = send3; p3_new = node3____CPAchecker_TMP_0; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_18109 = check__tmp; main__c1 = __return_18109; { _Bool __tmp_40; __tmp_40 = main__c1; _Bool assert__arg; assert__arg = __tmp_40; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_18045 = check__tmp; main__c1 = __return_18045; { _Bool __tmp_41; __tmp_41 = main__c1; _Bool assert__arg; assert__arg = __tmp_41; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_17955 = check__tmp; main__c1 = __return_17955; { _Bool __tmp_42; __tmp_42 = main__c1; _Bool assert__arg; assert__arg = __tmp_42; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_17871 = check__tmp; main__c1 = __return_17871; { _Bool __tmp_43; __tmp_43 = main__c1; _Bool assert__arg; assert__arg = __tmp_43; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_17779 = check__tmp; main__c1 = __return_17779; { _Bool __tmp_44; __tmp_44 = main__c1; _Bool assert__arg; assert__arg = __tmp_44; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_17707 = check__tmp; main__c1 = __return_17707; { _Bool __tmp_45; __tmp_45 = main__c1; _Bool assert__arg; assert__arg = __tmp_45; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_17597 = check__tmp; main__c1 = __return_17597; { _Bool __tmp_46; __tmp_46 = main__c1; _Bool assert__arg; assert__arg = __tmp_46; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_17495 = check__tmp; main__c1 = __return_17495; { _Bool __tmp_47; __tmp_47 = main__c1; _Bool assert__arg; assert__arg = __tmp_47; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } 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 { 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_17389 = check__tmp; main__c1 = __return_17389; { _Bool __tmp_48; __tmp_48 = main__c1; _Bool assert__arg; assert__arg = __tmp_48; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_17317 = check__tmp; main__c1 = __return_17317; { _Bool __tmp_49; __tmp_49 = main__c1; _Bool assert__arg; assert__arg = __tmp_49; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_17219 = check__tmp; main__c1 = __return_17219; { _Bool __tmp_50; __tmp_50 = main__c1; _Bool assert__arg; assert__arg = __tmp_50; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_17129 = check__tmp; main__c1 = __return_17129; { _Bool __tmp_51; __tmp_51 = main__c1; _Bool assert__arg; assert__arg = __tmp_51; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_17029 = check__tmp; main__c1 = __return_17029; { _Bool __tmp_52; __tmp_52 = main__c1; _Bool assert__arg; assert__arg = __tmp_52; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_16951 = check__tmp; main__c1 = __return_16951; { _Bool __tmp_53; __tmp_53 = main__c1; _Bool assert__arg; assert__arg = __tmp_53; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_16811 = check__tmp; main__c1 = __return_16811; { _Bool __tmp_54; __tmp_54 = main__c1; _Bool assert__arg; assert__arg = __tmp_54; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_16682 = check__tmp; main__c1 = __return_16682; { _Bool __tmp_55; __tmp_55 = main__c1; _Bool assert__arg; assert__arg = __tmp_55; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } } } } } } } } } } } } } else { return __return_main; } } else { node1____CPAchecker_TMP_0 = p1_new; p1_new = node1____CPAchecker_TMP_0; mode1 = 1; { msg_t node2__m2; node2__m2 = nomsg; if (!(mode2 == 0)) { return __return_main; } else { int node2____CPAchecker_TMP_0; if (send2 != nomsg) { if (p2_new == nomsg) { node2____CPAchecker_TMP_0 = send2; p2_new = node2____CPAchecker_TMP_0; mode2 = 1; { msg_t node3__m3; node3__m3 = nomsg; if (!(mode3 == 0)) { return __return_main; } else { int node3____CPAchecker_TMP_0; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_0 = send3; p3_new = node3____CPAchecker_TMP_0; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_16564 = check__tmp; main__c1 = __return_16564; { _Bool __tmp_56; __tmp_56 = main__c1; _Bool assert__arg; assert__arg = __tmp_56; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_16512 = check__tmp; main__c1 = __return_16512; { _Bool __tmp_57; __tmp_57 = main__c1; _Bool assert__arg; assert__arg = __tmp_57; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_16434 = check__tmp; main__c1 = __return_16434; { _Bool __tmp_58; __tmp_58 = main__c1; _Bool assert__arg; assert__arg = __tmp_58; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_16350 = check__tmp; main__c1 = __return_16350; { _Bool __tmp_59; __tmp_59 = main__c1; _Bool assert__arg; assert__arg = __tmp_59; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_16270 = check__tmp; main__c1 = __return_16270; { _Bool __tmp_60; __tmp_60 = main__c1; _Bool assert__arg; assert__arg = __tmp_60; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_16198 = check__tmp; main__c1 = __return_16198; { _Bool __tmp_61; __tmp_61 = main__c1; _Bool assert__arg; assert__arg = __tmp_61; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_16088 = check__tmp; main__c1 = __return_16088; { _Bool __tmp_62; __tmp_62 = main__c1; _Bool assert__arg; assert__arg = __tmp_62; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_15984 = check__tmp; main__c1 = __return_15984; { _Bool __tmp_63; __tmp_63 = main__c1; _Bool assert__arg; assert__arg = __tmp_63; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } 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 { 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_15890 = check__tmp; main__c1 = __return_15890; { _Bool __tmp_64; __tmp_64 = main__c1; _Bool assert__arg; assert__arg = __tmp_64; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_15818 = check__tmp; main__c1 = __return_15818; { _Bool __tmp_65; __tmp_65 = main__c1; _Bool assert__arg; assert__arg = __tmp_65; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_15720 = check__tmp; main__c1 = __return_15720; { _Bool __tmp_66; __tmp_66 = main__c1; _Bool assert__arg; assert__arg = __tmp_66; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_15628 = check__tmp; main__c1 = __return_15628; { _Bool __tmp_67; __tmp_67 = main__c1; _Bool assert__arg; assert__arg = __tmp_67; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_15528 = check__tmp; main__c1 = __return_15528; { _Bool __tmp_68; __tmp_68 = main__c1; _Bool assert__arg; assert__arg = __tmp_68; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_15448 = check__tmp; main__c1 = __return_15448; { _Bool __tmp_69; __tmp_69 = main__c1; _Bool assert__arg; assert__arg = __tmp_69; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_15318 = check__tmp; main__c1 = __return_15318; { _Bool __tmp_70; __tmp_70 = main__c1; _Bool assert__arg; assert__arg = __tmp_70; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_15201 = check__tmp; main__c1 = __return_15201; { _Bool __tmp_71; __tmp_71 = main__c1; _Bool assert__arg; assert__arg = __tmp_71; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } } } } } } } } } } 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 { int node3____CPAchecker_TMP_0; if (send3 != nomsg) { if (p3_new == nomsg) { node3____CPAchecker_TMP_0 = send3; p3_new = node3____CPAchecker_TMP_0; mode3 = 1; { msg_t node4__m4; node4__m4 = nomsg; if (!(mode4 == 0)) { return __return_main; } else { 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_15093 = check__tmp; main__c1 = __return_15093; { _Bool __tmp_72; __tmp_72 = main__c1; _Bool assert__arg; assert__arg = __tmp_72; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_15021 = check__tmp; main__c1 = __return_15021; { _Bool __tmp_73; __tmp_73 = main__c1; _Bool assert__arg; assert__arg = __tmp_73; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_14923 = check__tmp; main__c1 = __return_14923; { _Bool __tmp_74; __tmp_74 = main__c1; _Bool assert__arg; assert__arg = __tmp_74; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_14831 = check__tmp; main__c1 = __return_14831; { _Bool __tmp_75; __tmp_75 = main__c1; _Bool assert__arg; assert__arg = __tmp_75; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_14731 = check__tmp; main__c1 = __return_14731; { _Bool __tmp_76; __tmp_76 = main__c1; _Bool assert__arg; assert__arg = __tmp_76; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_14651 = check__tmp; main__c1 = __return_14651; { _Bool __tmp_77; __tmp_77 = main__c1; _Bool assert__arg; assert__arg = __tmp_77; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_14533 = check__tmp; main__c1 = __return_14533; { _Bool __tmp_78; __tmp_78 = main__c1; _Bool assert__arg; assert__arg = __tmp_78; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_14428 = check__tmp; main__c1 = __return_14428; { _Bool __tmp_79; __tmp_79 = main__c1; _Bool assert__arg; assert__arg = __tmp_79; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } 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 { 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_14314 = check__tmp; main__c1 = __return_14314; { _Bool __tmp_80; __tmp_80 = main__c1; _Bool assert__arg; assert__arg = __tmp_80; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_14234 = check__tmp; main__c1 = __return_14234; { _Bool __tmp_81; __tmp_81 = main__c1; _Bool assert__arg; assert__arg = __tmp_81; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_14128 = check__tmp; main__c1 = __return_14128; { _Bool __tmp_82; __tmp_82 = main__c1; _Bool assert__arg; assert__arg = __tmp_82; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_14035 = check__tmp; main__c1 = __return_14035; { _Bool __tmp_83; __tmp_83 = main__c1; _Bool assert__arg; assert__arg = __tmp_83; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } 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 { int node5____CPAchecker_TMP_0; if (send5 != nomsg) { if (p5_new == nomsg) { node5____CPAchecker_TMP_0 = send5; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_13927 = check__tmp; main__c1 = __return_13927; { _Bool __tmp_84; __tmp_84 = main__c1; _Bool assert__arg; assert__arg = __tmp_84; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_13846 = check__tmp; main__c1 = __return_13846; { _Bool __tmp_85; __tmp_85 = main__c1; _Bool assert__arg; assert__arg = __tmp_85; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } else { return __return_main; } } else { node5____CPAchecker_TMP_0 = p5_new; p5_new = node5____CPAchecker_TMP_0; mode5 = 1; { msg_t node6__m6; node6__m6 = nomsg; if (!(mode6 == 0)) { return __return_main; } else { int node6____CPAchecker_TMP_0; if (send6 != nomsg) { if (p6_new == nomsg) { node6____CPAchecker_TMP_0 = send6; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_13690 = check__tmp; main__c1 = __return_13690; { _Bool __tmp_86; __tmp_86 = main__c1; _Bool assert__arg; assert__arg = __tmp_86; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } else { return __return_main; } } else { node6____CPAchecker_TMP_0 = p6_new; p6_new = node6____CPAchecker_TMP_0; mode6 = 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; p6_old = p6_new; p6_new = nomsg; { int check__tmp; if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) <= 1) { if (((int)r1) >= 6) { return __return_main; } else { if ((((((((int)st1) + ((int)st2)) + ((int)st3)) + ((int)st4)) + ((int)st5)) + ((int)st6)) == 0) { if (((int)r1) < 6) { check__tmp = 1; __return_13332 = check__tmp; main__c1 = __return_13332; { _Bool __tmp_87; __tmp_87 = main__c1; _Bool assert__arg; assert__arg = __tmp_87; if (assert__arg == 0) { return __return_main; } else { goto label_13339; } } } else { return __return_main; } } else { return __return_main; } } } else { return __return_main; } } } } } } } } } } } } } } } } } } } } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } else { return __return_main; } } }