diff --git a/include/klee/ADT/Incremental.h b/include/klee/ADT/Incremental.h index b2e8417350..6f16fd0867 100644 --- a/include/klee/ADT/Incremental.h +++ b/include/klee/ADT/Incremental.h @@ -28,6 +28,11 @@ void extend(std::vector<_Tp, _Alloc> &ths, ths.insert(ths.end(), other.begin(), other.end()); } +template +void takeAfterv(std::vector<_Tp, _Alloc> &ths, size_t n) { + std::vector<_Tp, _Alloc>(ths.begin() + n, ths.end()).swap(ths); +} + template > class inc_vector { public: @@ -131,12 +136,9 @@ class inc_vector { size_t frames_count, frame_index; take(n, frames_count, frame_index); result = *this; - std::vector<_Tp, _Alloc>(result.v.begin() + n, result.v.end()) - .swap(result.v); - std::vector(result.frame_sizes.begin() + frame_index, - result.frame_sizes.end()) - .swap(result.frame_sizes); - if (frames_count) + takeAfterv(result.v, n); + takeAfterv(result.frame_sizes, frame_index); + if (frames_count && !result.frame_sizes.empty()) result.frame_sizes[0] -= frames_count; } diff --git a/test/Solver/pals_floodmax.5.2.ufo.BOUNDED-10.pals.c b/test/Solver/pals_floodmax.5.2.ufo.BOUNDED-10.pals.c new file mode 100644 index 0000000000..4dd74f1d3c --- /dev/null +++ b/test/Solver/pals_floodmax.5.2.ufo.BOUNDED-10.pals.c @@ -0,0 +1,2775 @@ +// REQUIRES: z3 +// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false --solver-backend=z3-tree --max-solvers-approx-tree-inc=16 -max-memory=6008 --optimize --skip-not-lazy-initialized -output-source=false --output-stats=false --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --function-call-reproduce=reach_error -dump-states-on-halt=true -exit-on-error-type=Assert --search=dfs -max-instructions=6000 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false %t1.bc 2>&1 | FileCheck -check-prefix=CHECK-VERDICT %s +// CHECK-VERDICT: KLEE: done: total instructions = 6000 +#include "klee-test-comp.c" + +extern void abort(void); +extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__((__nothrow__, __leaf__)) __attribute__((__noreturn__)); +void reach_error() { __assert_fail("0", "pals_floodmax.5.2.ufo.BOUNDED-10.pals.c", 3, "reach_error"); } + +// This file is part of the SV-Benchmarks collection of verification tasks: +// https://github.com/sosy-lab/sv-benchmarks +// +// SPDX-FileCopyrightText: 2013 Carnegie Mellon University +// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community +// +// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU + +/* Generated by CIL v. 1.6.0 */ +/* print_CIL_Input is true */ + +char __VERIFIER_nondet_char(void); +_Bool __VERIFIER_nondet_bool(void); +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; +extern void read(port_t p, msg_t m); +extern void write(port_t p, msg_t m); +msg_t nomsg = (msg_t)-1; +port_t p12; +char p12_old; +char p12_new; +_Bool ep12; +port_t p13; +char p13_old; +char p13_new; +_Bool ep13; +port_t p14; +char p14_old; +char p14_new; +_Bool ep14; +port_t p15; +char p15_old; +char p15_new; +_Bool ep15; +port_t p21; +char p21_old; +char p21_new; +_Bool ep21; +port_t p23; +char p23_old; +char p23_new; +_Bool ep23; +port_t p24; +char p24_old; +char p24_new; +_Bool ep24; +port_t p25; +char p25_old; +char p25_new; +_Bool ep25; +port_t p31; +char p31_old; +char p31_new; +_Bool ep31; +port_t p32; +char p32_old; +char p32_new; +_Bool ep32; +port_t p34; +char p34_old; +char p34_new; +_Bool ep34; +port_t p35; +char p35_old; +char p35_new; +_Bool ep35; +port_t p41; +char p41_old; +char p41_new; +_Bool ep41; +port_t p42; +char p42_old; +char p42_new; +_Bool ep42; +port_t p43; +char p43_old; +char p43_new; +_Bool ep43; +port_t p45; +char p45_old; +char p45_new; +_Bool ep45; +port_t p51; +char p51_old; +char p51_new; +_Bool ep51; +port_t p52; +char p52_old; +char p52_new; +_Bool ep52; +port_t p53; +char p53_old; +char p53_new; +_Bool ep53; +port_t p54; +char p54_old; +char p54_new; +_Bool ep54; +char id1; +char r1; +char st1; +char nl1; +char m1; +char max1; +_Bool mode1; +char id2; +char r2; +char st2; +char nl2; +char m2; +char max2; +_Bool mode2; +char id3; +char r3; +char st3; +char nl3; +char m3; +char max3; +_Bool mode3; +char id4; +char r4; +char st4; +char nl4; +char m4; +char max4; +_Bool mode4; +char id5; +char r5; +char st5; +char nl5; +char m5; +char max5; +_Bool mode5; +void node1(void) { + + { + if (mode1) { + r1 = (char)((int)r1 + 1); + if (ep21) { + m1 = p21_old; + p21_old = nomsg; + if ((int)m1 > (int)max1) { + max1 = m1; + } + } + if (ep31) { + m1 = p31_old; + p31_old = nomsg; + if ((int)m1 > (int)max1) { + max1 = m1; + } + } + if (ep41) { + m1 = p41_old; + p41_old = nomsg; + if ((int)m1 > (int)max1) { + max1 = m1; + } + } + if (ep51) { + m1 = p51_old; + p51_old = nomsg; + if ((int)m1 > (int)max1) { + max1 = m1; + } + } + if ((int)r1 == 3) { + if ((int)max1 == (int)id1) { + st1 = (char)1; + } else { + nl1 = (char)1; + } + } + mode1 = (_Bool)0; + } else { + if ((int)r1 < 4) { + if (ep12) { + p12_new = max1 != nomsg && p12_new == nomsg ? max1 : p12_new; + } + if (ep13) { + p13_new = max1 != nomsg && p13_new == nomsg ? max1 : p13_new; + } + if (ep14) { + p14_new = max1 != nomsg && p14_new == nomsg ? max1 : p14_new; + } + if (ep15) { + p15_new = max1 != nomsg && p15_new == nomsg ? max1 : p15_new; + } + } + mode1 = (_Bool)1; + } + return; + } +} +void node2(void) { + + { + if (mode2) { + r2 = (char)((int)r2 + 1); + if (ep12) { + m2 = p12_old; + p12_old = nomsg; + if ((int)m2 > (int)max2) { + max2 = m2; + } + } + if (ep32) { + m2 = p32_old; + p32_old = nomsg; + if ((int)m2 > (int)max2) { + max2 = m2; + } + } + if (ep42) { + m2 = p42_old; + p42_old = nomsg; + if ((int)m2 > (int)max2) { + max2 = m2; + } + } + if (ep52) { + m2 = p52_old; + p52_old = nomsg; + if ((int)m2 > (int)max2) { + max2 = m2; + } + } + if ((int)r2 == 4) { + if ((int)max2 == (int)id2) { + st2 = (char)1; + } else { + nl2 = (char)1; + } + } + mode2 = (_Bool)0; + } else { + if ((int)r2 < 4) { + if (ep21) { + p21_new = max2 != nomsg && p21_new == nomsg ? max2 : p21_new; + } + if (ep23) { + p23_new = max2 != nomsg && p23_new == nomsg ? max2 : p23_new; + } + if (ep24) { + p24_new = max2 != nomsg && p24_new == nomsg ? max2 : p24_new; + } + if (ep25) { + p25_new = max2 != nomsg && p25_new == nomsg ? max2 : p25_new; + } + } + mode2 = (_Bool)1; + } + return; + } +} +void node3(void) { + + { + if (mode3) { + r3 = (char)((int)r3 + 1); + if (ep13) { + m3 = p13_old; + p13_old = nomsg; + if ((int)m3 > (int)max3) { + max3 = m3; + } + } + if (ep23) { + m3 = p23_old; + p23_old = nomsg; + if ((int)m3 > (int)max3) { + max3 = m3; + } + } + if (ep43) { + m3 = p43_old; + p43_old = nomsg; + if ((int)m3 > (int)max3) { + max3 = m3; + } + } + if (ep53) { + m3 = p53_old; + p53_old = nomsg; + if ((int)m3 > (int)max3) { + max3 = m3; + } + } + if ((int)r3 == 4) { + if ((int)max3 == (int)id3) { + st3 = (char)1; + } else { + nl3 = (char)1; + } + } + mode3 = (_Bool)0; + } else { + if ((int)r3 < 4) { + if (ep31) { + p31_new = max3 != nomsg && p31_new == nomsg ? max3 : p31_new; + } + if (ep32) { + p32_new = max3 != nomsg && p32_new == nomsg ? max3 : p32_new; + } + if (ep34) { + p34_new = max3 != nomsg && p34_new == nomsg ? max3 : p34_new; + } + if (ep35) { + p35_new = max3 != nomsg && p35_new == nomsg ? max3 : p35_new; + } + } + mode3 = (_Bool)1; + } + return; + } +} +void node4(void) { + + { + if (mode4) { + r4 = (char)((int)r4 + 1); + if (ep14) { + m4 = p14_old; + p14_old = nomsg; + if ((int)m4 > (int)max4) { + max4 = m4; + } + } + if (ep24) { + m4 = p24_old; + p24_old = nomsg; + if ((int)m4 > (int)max4) { + max4 = m4; + } + } + if (ep34) { + m4 = p34_old; + p34_old = nomsg; + if ((int)m4 > (int)max4) { + max4 = m4; + } + } + if (ep54) { + m4 = p54_old; + p54_old = nomsg; + if ((int)m4 > (int)max4) { + max4 = m4; + } + } + if ((int)r4 == 4) { + if ((int)max4 == (int)id4) { + st4 = (char)1; + } else { + nl4 = (char)1; + } + } + mode4 = (_Bool)0; + } else { + if ((int)r4 < 4) { + if (ep41) { + p41_new = max4 != nomsg && p41_new == nomsg ? max4 : p41_new; + } + if (ep42) { + p42_new = max4 != nomsg && p42_new == nomsg ? max4 : p42_new; + } + if (ep43) { + p43_new = max4 != nomsg && p43_new == nomsg ? max4 : p43_new; + } + if (ep45) { + p45_new = max4 != nomsg && p45_new == nomsg ? max4 : p45_new; + } + } + mode4 = (_Bool)1; + } + return; + } +} +void node5(void) { + + { + if (mode5) { + r5 = (char)((int)r5 + 1); + if (ep15) { + m5 = p15_old; + p15_old = nomsg; + if ((int)m5 > (int)max5) { + max5 = m5; + } + } + if (ep25) { + m5 = p25_old; + p25_old = nomsg; + if ((int)m5 > (int)max5) { + max5 = m5; + } + } + if (ep35) { + m5 = p35_old; + p35_old = nomsg; + if ((int)m5 > (int)max5) { + max5 = m5; + } + } + if (ep45) { + m5 = p45_old; + p45_old = nomsg; + if ((int)m5 > (int)max5) { + max5 = m5; + } + } + if ((int)r5 == 4) { + if ((int)max5 == (int)id5) { + st5 = (char)1; + } else { + nl5 = (char)1; + } + } + mode5 = (_Bool)0; + } else { + if ((int)r5 < 4) { + if (ep51) { + p51_new = max5 != nomsg && p51_new == nomsg ? max5 : p51_new; + } + if (ep52) { + p52_new = max5 != nomsg && p52_new == nomsg ? max5 : p52_new; + } + if (ep53) { + p53_new = max5 != nomsg && p53_new == nomsg ? max5 : p53_new; + } + if (ep54) { + p54_new = max5 != nomsg && p54_new == nomsg ? max5 : p54_new; + } + } + mode5 = (_Bool)1; + } + return; + } +} +int init(void) { + _Bool r121; + _Bool r131; + _Bool r141; + _Bool r151; + _Bool r211; + _Bool r231; + _Bool r241; + _Bool r251; + _Bool r311; + _Bool r321; + _Bool r341; + _Bool r351; + _Bool r411; + _Bool r421; + _Bool r431; + _Bool r451; + _Bool r511; + _Bool r521; + _Bool r531; + _Bool r541; + _Bool r122; + int tmp; + _Bool r132; + int tmp___0; + _Bool r142; + int tmp___1; + _Bool r152; + int tmp___2; + _Bool r212; + int tmp___3; + _Bool r232; + int tmp___4; + _Bool r242; + int tmp___5; + _Bool r252; + int tmp___6; + _Bool r312; + int tmp___7; + _Bool r322; + int tmp___8; + _Bool r342; + int tmp___9; + _Bool r352; + int tmp___10; + _Bool r412; + int tmp___11; + _Bool r422; + int tmp___12; + _Bool r432; + int tmp___13; + _Bool r452; + int tmp___14; + _Bool r512; + int tmp___15; + _Bool r522; + int tmp___16; + _Bool r532; + int tmp___17; + _Bool r542; + int tmp___18; + _Bool r123; + int tmp___19; + _Bool r133; + int tmp___20; + _Bool r143; + int tmp___21; + _Bool r153; + int tmp___22; + _Bool r213; + int tmp___23; + _Bool r233; + int tmp___24; + _Bool r243; + int tmp___25; + _Bool r253; + int tmp___26; + _Bool r313; + int tmp___27; + _Bool r323; + int tmp___28; + _Bool r343; + int tmp___29; + _Bool r353; + int tmp___30; + _Bool r413; + int tmp___31; + _Bool r423; + int tmp___32; + _Bool r433; + int tmp___33; + _Bool r453; + int tmp___34; + _Bool r513; + int tmp___35; + _Bool r523; + int tmp___36; + _Bool r533; + int tmp___37; + _Bool r543; + int tmp___38; + _Bool r124; + int tmp___39; + _Bool r134; + int tmp___40; + _Bool r144; + int tmp___41; + _Bool r154; + int tmp___42; + _Bool r214; + int tmp___43; + _Bool r234; + int tmp___44; + _Bool r244; + int tmp___45; + _Bool r254; + int tmp___46; + _Bool r314; + int tmp___47; + _Bool r324; + int tmp___48; + _Bool r344; + int tmp___49; + _Bool r354; + int tmp___50; + _Bool r414; + int tmp___51; + _Bool r424; + int tmp___52; + _Bool r434; + int tmp___53; + _Bool r454; + int tmp___54; + _Bool r514; + int tmp___55; + _Bool r524; + int tmp___56; + _Bool r534; + int tmp___57; + _Bool r544; + int tmp___58; + int tmp___59; + + { + r121 = ep12; + r131 = ep13; + r141 = ep14; + r151 = ep15; + r211 = ep21; + r231 = ep23; + r241 = ep24; + r251 = ep25; + r311 = ep31; + r321 = ep32; + r341 = ep34; + r351 = ep35; + r411 = ep41; + r421 = ep42; + r431 = ep43; + r451 = ep45; + r511 = ep51; + r521 = ep52; + r531 = ep53; + r541 = ep54; + if (r121) { + tmp = 1; + } else if (r131) { + if (ep32) { + tmp = 1; + } else { + goto _L___0; + } + } else + _L___0: /* CIL Label */ + if (r141) { + if (ep42) { + tmp = 1; + } else { + goto _L; + } + } else + _L: /* CIL Label */ + if (r151) { + if (ep52) { + tmp = 1; + } else { + tmp = 0; + } + } else { + tmp = 0; + } + r122 = (_Bool)tmp; + if (r131) { + tmp___0 = 1; + } else if (r121) { + if (ep23) { + tmp___0 = 1; + } else { + goto _L___2; + } + } else + _L___2: /* CIL Label */ + if (r141) { + if (ep43) { + tmp___0 = 1; + } else { + goto _L___1; + } + } else + _L___1: /* CIL Label */ + if (r151) { + if (ep53) { + tmp___0 = 1; + } else { + tmp___0 = 0; + } + } else { + tmp___0 = 0; + } + r132 = (_Bool)tmp___0; + if (r141) { + tmp___1 = 1; + } else if (r121) { + if (ep24) { + tmp___1 = 1; + } else { + goto _L___4; + } + } else + _L___4: /* CIL Label */ + if (r131) { + if (ep34) { + tmp___1 = 1; + } else { + goto _L___3; + } + } else + _L___3: /* CIL Label */ + if (r151) { + if (ep54) { + tmp___1 = 1; + } else { + tmp___1 = 0; + } + } else { + tmp___1 = 0; + } + r142 = (_Bool)tmp___1; + if (r151) { + tmp___2 = 1; + } else if (r121) { + if (ep25) { + tmp___2 = 1; + } else { + goto _L___6; + } + } else + _L___6: /* CIL Label */ + if (r131) { + if (ep35) { + tmp___2 = 1; + } else { + goto _L___5; + } + } else + _L___5: /* CIL Label */ + if (r141) { + if (ep45) { + tmp___2 = 1; + } else { + tmp___2 = 0; + } + } else { + tmp___2 = 0; + } + r152 = (_Bool)tmp___2; + if (r211) { + tmp___3 = 1; + } else if (r231) { + if (ep31) { + tmp___3 = 1; + } else { + goto _L___8; + } + } else + _L___8: /* CIL Label */ + if (r241) { + if (ep41) { + tmp___3 = 1; + } else { + goto _L___7; + } + } else + _L___7: /* CIL Label */ + if (r251) { + if (ep51) { + tmp___3 = 1; + } else { + tmp___3 = 0; + } + } else { + tmp___3 = 0; + } + r212 = (_Bool)tmp___3; + if (r231) { + tmp___4 = 1; + } else if (r211) { + if (ep13) { + tmp___4 = 1; + } else { + goto _L___10; + } + } else + _L___10: /* CIL Label */ + if (r241) { + if (ep43) { + tmp___4 = 1; + } else { + goto _L___9; + } + } else + _L___9: /* CIL Label */ + if (r251) { + if (ep53) { + tmp___4 = 1; + } else { + tmp___4 = 0; + } + } else { + tmp___4 = 0; + } + r232 = (_Bool)tmp___4; + if (r241) { + tmp___5 = 1; + } else if (r211) { + if (ep14) { + tmp___5 = 1; + } else { + goto _L___12; + } + } else + _L___12: /* CIL Label */ + if (r231) { + if (ep34) { + tmp___5 = 1; + } else { + goto _L___11; + } + } else + _L___11: /* CIL Label */ + if (r251) { + if (ep54) { + tmp___5 = 1; + } else { + tmp___5 = 0; + } + } else { + tmp___5 = 0; + } + r242 = (_Bool)tmp___5; + if (r251) { + tmp___6 = 1; + } else if (r211) { + if (ep15) { + tmp___6 = 1; + } else { + goto _L___14; + } + } else + _L___14: /* CIL Label */ + if (r231) { + if (ep35) { + tmp___6 = 1; + } else { + goto _L___13; + } + } else + _L___13: /* CIL Label */ + if (r241) { + if (ep45) { + tmp___6 = 1; + } else { + tmp___6 = 0; + } + } else { + tmp___6 = 0; + } + r252 = (_Bool)tmp___6; + if (r311) { + tmp___7 = 1; + } else if (r321) { + if (ep21) { + tmp___7 = 1; + } else { + goto _L___16; + } + } else + _L___16: /* CIL Label */ + if (r341) { + if (ep41) { + tmp___7 = 1; + } else { + goto _L___15; + } + } else + _L___15: /* CIL Label */ + if (r351) { + if (ep51) { + tmp___7 = 1; + } else { + tmp___7 = 0; + } + } else { + tmp___7 = 0; + } + r312 = (_Bool)tmp___7; + if (r321) { + tmp___8 = 1; + } else if (r311) { + if (ep12) { + tmp___8 = 1; + } else { + goto _L___18; + } + } else + _L___18: /* CIL Label */ + if (r341) { + if (ep42) { + tmp___8 = 1; + } else { + goto _L___17; + } + } else + _L___17: /* CIL Label */ + if (r351) { + if (ep52) { + tmp___8 = 1; + } else { + tmp___8 = 0; + } + } else { + tmp___8 = 0; + } + r322 = (_Bool)tmp___8; + if (r341) { + tmp___9 = 1; + } else if (r311) { + if (ep14) { + tmp___9 = 1; + } else { + goto _L___20; + } + } else + _L___20: /* CIL Label */ + if (r321) { + if (ep24) { + tmp___9 = 1; + } else { + goto _L___19; + } + } else + _L___19: /* CIL Label */ + if (r351) { + if (ep54) { + tmp___9 = 1; + } else { + tmp___9 = 0; + } + } else { + tmp___9 = 0; + } + r342 = (_Bool)tmp___9; + if (r351) { + tmp___10 = 1; + } else if (r311) { + if (ep15) { + tmp___10 = 1; + } else { + goto _L___22; + } + } else + _L___22: /* CIL Label */ + if (r321) { + if (ep25) { + tmp___10 = 1; + } else { + goto _L___21; + } + } else + _L___21: /* CIL Label */ + if (r341) { + if (ep45) { + tmp___10 = 1; + } else { + tmp___10 = 0; + } + } else { + tmp___10 = 0; + } + r352 = (_Bool)tmp___10; + if (r411) { + tmp___11 = 1; + } else if (r421) { + if (ep21) { + tmp___11 = 1; + } else { + goto _L___24; + } + } else + _L___24: /* CIL Label */ + if (r431) { + if (ep31) { + tmp___11 = 1; + } else { + goto _L___23; + } + } else + _L___23: /* CIL Label */ + if (r451) { + if (ep51) { + tmp___11 = 1; + } else { + tmp___11 = 0; + } + } else { + tmp___11 = 0; + } + r412 = (_Bool)tmp___11; + if (r421) { + tmp___12 = 1; + } else if (r411) { + if (ep12) { + tmp___12 = 1; + } else { + goto _L___26; + } + } else + _L___26: /* CIL Label */ + if (r431) { + if (ep32) { + tmp___12 = 1; + } else { + goto _L___25; + } + } else + _L___25: /* CIL Label */ + if (r451) { + if (ep52) { + tmp___12 = 1; + } else { + tmp___12 = 0; + } + } else { + tmp___12 = 0; + } + r422 = (_Bool)tmp___12; + if (r431) { + tmp___13 = 1; + } else if (r411) { + if (ep13) { + tmp___13 = 1; + } else { + goto _L___28; + } + } else + _L___28: /* CIL Label */ + if (r421) { + if (ep23) { + tmp___13 = 1; + } else { + goto _L___27; + } + } else + _L___27: /* CIL Label */ + if (r451) { + if (ep53) { + tmp___13 = 1; + } else { + tmp___13 = 0; + } + } else { + tmp___13 = 0; + } + r432 = (_Bool)tmp___13; + if (r451) { + tmp___14 = 1; + } else if (r411) { + if (ep15) { + tmp___14 = 1; + } else { + goto _L___30; + } + } else + _L___30: /* CIL Label */ + if (r421) { + if (ep25) { + tmp___14 = 1; + } else { + goto _L___29; + } + } else + _L___29: /* CIL Label */ + if (r431) { + if (ep35) { + tmp___14 = 1; + } else { + tmp___14 = 0; + } + } else { + tmp___14 = 0; + } + r452 = (_Bool)tmp___14; + if (r511) { + tmp___15 = 1; + } else if (r521) { + if (ep21) { + tmp___15 = 1; + } else { + goto _L___32; + } + } else + _L___32: /* CIL Label */ + if (r531) { + if (ep31) { + tmp___15 = 1; + } else { + goto _L___31; + } + } else + _L___31: /* CIL Label */ + if (r541) { + if (ep41) { + tmp___15 = 1; + } else { + tmp___15 = 0; + } + } else { + tmp___15 = 0; + } + r512 = (_Bool)tmp___15; + if (r521) { + tmp___16 = 1; + } else if (r511) { + if (ep12) { + tmp___16 = 1; + } else { + goto _L___34; + } + } else + _L___34: /* CIL Label */ + if (r531) { + if (ep32) { + tmp___16 = 1; + } else { + goto _L___33; + } + } else + _L___33: /* CIL Label */ + if (r541) { + if (ep42) { + tmp___16 = 1; + } else { + tmp___16 = 0; + } + } else { + tmp___16 = 0; + } + r522 = (_Bool)tmp___16; + if (r531) { + tmp___17 = 1; + } else if (r511) { + if (ep13) { + tmp___17 = 1; + } else { + goto _L___36; + } + } else + _L___36: /* CIL Label */ + if (r521) { + if (ep23) { + tmp___17 = 1; + } else { + goto _L___35; + } + } else + _L___35: /* CIL Label */ + if (r541) { + if (ep43) { + tmp___17 = 1; + } else { + tmp___17 = 0; + } + } else { + tmp___17 = 0; + } + r532 = (_Bool)tmp___17; + if (r541) { + tmp___18 = 1; + } else if (r511) { + if (ep14) { + tmp___18 = 1; + } else { + goto _L___38; + } + } else + _L___38: /* CIL Label */ + if (r521) { + if (ep24) { + tmp___18 = 1; + } else { + goto _L___37; + } + } else + _L___37: /* CIL Label */ + if (r531) { + if (ep34) { + tmp___18 = 1; + } else { + tmp___18 = 0; + } + } else { + tmp___18 = 0; + } + r542 = (_Bool)tmp___18; + if (r122) { + tmp___19 = 1; + } else if (r132) { + if (ep32) { + tmp___19 = 1; + } else { + goto _L___40; + } + } else + _L___40: /* CIL Label */ + if (r142) { + if (ep42) { + tmp___19 = 1; + } else { + goto _L___39; + } + } else + _L___39: /* CIL Label */ + if (r152) { + if (ep52) { + tmp___19 = 1; + } else { + tmp___19 = 0; + } + } else { + tmp___19 = 0; + } + r123 = (_Bool)tmp___19; + if (r132) { + tmp___20 = 1; + } else if (r122) { + if (ep23) { + tmp___20 = 1; + } else { + goto _L___42; + } + } else + _L___42: /* CIL Label */ + if (r142) { + if (ep43) { + tmp___20 = 1; + } else { + goto _L___41; + } + } else + _L___41: /* CIL Label */ + if (r152) { + if (ep53) { + tmp___20 = 1; + } else { + tmp___20 = 0; + } + } else { + tmp___20 = 0; + } + r133 = (_Bool)tmp___20; + if (r142) { + tmp___21 = 1; + } else if (r122) { + if (ep24) { + tmp___21 = 1; + } else { + goto _L___44; + } + } else + _L___44: /* CIL Label */ + if (r132) { + if (ep34) { + tmp___21 = 1; + } else { + goto _L___43; + } + } else + _L___43: /* CIL Label */ + if (r152) { + if (ep54) { + tmp___21 = 1; + } else { + tmp___21 = 0; + } + } else { + tmp___21 = 0; + } + r143 = (_Bool)tmp___21; + if (r152) { + tmp___22 = 1; + } else if (r122) { + if (ep25) { + tmp___22 = 1; + } else { + goto _L___46; + } + } else + _L___46: /* CIL Label */ + if (r132) { + if (ep35) { + tmp___22 = 1; + } else { + goto _L___45; + } + } else + _L___45: /* CIL Label */ + if (r142) { + if (ep45) { + tmp___22 = 1; + } else { + tmp___22 = 0; + } + } else { + tmp___22 = 0; + } + r153 = (_Bool)tmp___22; + if (r212) { + tmp___23 = 1; + } else if (r232) { + if (ep31) { + tmp___23 = 1; + } else { + goto _L___48; + } + } else + _L___48: /* CIL Label */ + if (r242) { + if (ep41) { + tmp___23 = 1; + } else { + goto _L___47; + } + } else + _L___47: /* CIL Label */ + if (r252) { + if (ep51) { + tmp___23 = 1; + } else { + tmp___23 = 0; + } + } else { + tmp___23 = 0; + } + r213 = (_Bool)tmp___23; + if (r232) { + tmp___24 = 1; + } else if (r212) { + if (ep13) { + tmp___24 = 1; + } else { + goto _L___50; + } + } else + _L___50: /* CIL Label */ + if (r242) { + if (ep43) { + tmp___24 = 1; + } else { + goto _L___49; + } + } else + _L___49: /* CIL Label */ + if (r252) { + if (ep53) { + tmp___24 = 1; + } else { + tmp___24 = 0; + } + } else { + tmp___24 = 0; + } + r233 = (_Bool)tmp___24; + if (r242) { + tmp___25 = 1; + } else if (r212) { + if (ep14) { + tmp___25 = 1; + } else { + goto _L___52; + } + } else + _L___52: /* CIL Label */ + if (r232) { + if (ep34) { + tmp___25 = 1; + } else { + goto _L___51; + } + } else + _L___51: /* CIL Label */ + if (r252) { + if (ep54) { + tmp___25 = 1; + } else { + tmp___25 = 0; + } + } else { + tmp___25 = 0; + } + r243 = (_Bool)tmp___25; + if (r252) { + tmp___26 = 1; + } else if (r212) { + if (ep15) { + tmp___26 = 1; + } else { + goto _L___54; + } + } else + _L___54: /* CIL Label */ + if (r232) { + if (ep35) { + tmp___26 = 1; + } else { + goto _L___53; + } + } else + _L___53: /* CIL Label */ + if (r242) { + if (ep45) { + tmp___26 = 1; + } else { + tmp___26 = 0; + } + } else { + tmp___26 = 0; + } + r253 = (_Bool)tmp___26; + if (r312) { + tmp___27 = 1; + } else if (r322) { + if (ep21) { + tmp___27 = 1; + } else { + goto _L___56; + } + } else + _L___56: /* CIL Label */ + if (r342) { + if (ep41) { + tmp___27 = 1; + } else { + goto _L___55; + } + } else + _L___55: /* CIL Label */ + if (r352) { + if (ep51) { + tmp___27 = 1; + } else { + tmp___27 = 0; + } + } else { + tmp___27 = 0; + } + r313 = (_Bool)tmp___27; + if (r322) { + tmp___28 = 1; + } else if (r312) { + if (ep12) { + tmp___28 = 1; + } else { + goto _L___58; + } + } else + _L___58: /* CIL Label */ + if (r342) { + if (ep42) { + tmp___28 = 1; + } else { + goto _L___57; + } + } else + _L___57: /* CIL Label */ + if (r352) { + if (ep52) { + tmp___28 = 1; + } else { + tmp___28 = 0; + } + } else { + tmp___28 = 0; + } + r323 = (_Bool)tmp___28; + if (r342) { + tmp___29 = 1; + } else if (r312) { + if (ep14) { + tmp___29 = 1; + } else { + goto _L___60; + } + } else + _L___60: /* CIL Label */ + if (r322) { + if (ep24) { + tmp___29 = 1; + } else { + goto _L___59; + } + } else + _L___59: /* CIL Label */ + if (r352) { + if (ep54) { + tmp___29 = 1; + } else { + tmp___29 = 0; + } + } else { + tmp___29 = 0; + } + r343 = (_Bool)tmp___29; + if (r352) { + tmp___30 = 1; + } else if (r312) { + if (ep15) { + tmp___30 = 1; + } else { + goto _L___62; + } + } else + _L___62: /* CIL Label */ + if (r322) { + if (ep25) { + tmp___30 = 1; + } else { + goto _L___61; + } + } else + _L___61: /* CIL Label */ + if (r342) { + if (ep45) { + tmp___30 = 1; + } else { + tmp___30 = 0; + } + } else { + tmp___30 = 0; + } + r353 = (_Bool)tmp___30; + if (r412) { + tmp___31 = 1; + } else if (r422) { + if (ep21) { + tmp___31 = 1; + } else { + goto _L___64; + } + } else + _L___64: /* CIL Label */ + if (r432) { + if (ep31) { + tmp___31 = 1; + } else { + goto _L___63; + } + } else + _L___63: /* CIL Label */ + if (r452) { + if (ep51) { + tmp___31 = 1; + } else { + tmp___31 = 0; + } + } else { + tmp___31 = 0; + } + r413 = (_Bool)tmp___31; + if (r422) { + tmp___32 = 1; + } else if (r412) { + if (ep12) { + tmp___32 = 1; + } else { + goto _L___66; + } + } else + _L___66: /* CIL Label */ + if (r432) { + if (ep32) { + tmp___32 = 1; + } else { + goto _L___65; + } + } else + _L___65: /* CIL Label */ + if (r452) { + if (ep52) { + tmp___32 = 1; + } else { + tmp___32 = 0; + } + } else { + tmp___32 = 0; + } + r423 = (_Bool)tmp___32; + if (r432) { + tmp___33 = 1; + } else if (r412) { + if (ep13) { + tmp___33 = 1; + } else { + goto _L___68; + } + } else + _L___68: /* CIL Label */ + if (r422) { + if (ep23) { + tmp___33 = 1; + } else { + goto _L___67; + } + } else + _L___67: /* CIL Label */ + if (r452) { + if (ep53) { + tmp___33 = 1; + } else { + tmp___33 = 0; + } + } else { + tmp___33 = 0; + } + r433 = (_Bool)tmp___33; + if (r452) { + tmp___34 = 1; + } else if (r412) { + if (ep15) { + tmp___34 = 1; + } else { + goto _L___70; + } + } else + _L___70: /* CIL Label */ + if (r422) { + if (ep25) { + tmp___34 = 1; + } else { + goto _L___69; + } + } else + _L___69: /* CIL Label */ + if (r432) { + if (ep35) { + tmp___34 = 1; + } else { + tmp___34 = 0; + } + } else { + tmp___34 = 0; + } + r453 = (_Bool)tmp___34; + if (r512) { + tmp___35 = 1; + } else if (r522) { + if (ep21) { + tmp___35 = 1; + } else { + goto _L___72; + } + } else + _L___72: /* CIL Label */ + if (r532) { + if (ep31) { + tmp___35 = 1; + } else { + goto _L___71; + } + } else + _L___71: /* CIL Label */ + if (r542) { + if (ep41) { + tmp___35 = 1; + } else { + tmp___35 = 0; + } + } else { + tmp___35 = 0; + } + r513 = (_Bool)tmp___35; + if (r522) { + tmp___36 = 1; + } else if (r512) { + if (ep12) { + tmp___36 = 1; + } else { + goto _L___74; + } + } else + _L___74: /* CIL Label */ + if (r532) { + if (ep32) { + tmp___36 = 1; + } else { + goto _L___73; + } + } else + _L___73: /* CIL Label */ + if (r542) { + if (ep42) { + tmp___36 = 1; + } else { + tmp___36 = 0; + } + } else { + tmp___36 = 0; + } + r523 = (_Bool)tmp___36; + if (r532) { + tmp___37 = 1; + } else if (r512) { + if (ep13) { + tmp___37 = 1; + } else { + goto _L___76; + } + } else + _L___76: /* CIL Label */ + if (r522) { + if (ep23) { + tmp___37 = 1; + } else { + goto _L___75; + } + } else + _L___75: /* CIL Label */ + if (r542) { + if (ep43) { + tmp___37 = 1; + } else { + tmp___37 = 0; + } + } else { + tmp___37 = 0; + } + r533 = (_Bool)tmp___37; + if (r542) { + tmp___38 = 1; + } else if (r512) { + if (ep14) { + tmp___38 = 1; + } else { + goto _L___78; + } + } else + _L___78: /* CIL Label */ + if (r522) { + if (ep24) { + tmp___38 = 1; + } else { + goto _L___77; + } + } else + _L___77: /* CIL Label */ + if (r532) { + if (ep34) { + tmp___38 = 1; + } else { + tmp___38 = 0; + } + } else { + tmp___38 = 0; + } + r543 = (_Bool)tmp___38; + if (r123) { + tmp___39 = 1; + } else if (r133) { + if (ep32) { + tmp___39 = 1; + } else { + goto _L___80; + } + } else + _L___80: /* CIL Label */ + if (r143) { + if (ep42) { + tmp___39 = 1; + } else { + goto _L___79; + } + } else + _L___79: /* CIL Label */ + if (r153) { + if (ep52) { + tmp___39 = 1; + } else { + tmp___39 = 0; + } + } else { + tmp___39 = 0; + } + r124 = (_Bool)tmp___39; + if (r133) { + tmp___40 = 1; + } else if (r123) { + if (ep23) { + tmp___40 = 1; + } else { + goto _L___82; + } + } else + _L___82: /* CIL Label */ + if (r143) { + if (ep43) { + tmp___40 = 1; + } else { + goto _L___81; + } + } else + _L___81: /* CIL Label */ + if (r153) { + if (ep53) { + tmp___40 = 1; + } else { + tmp___40 = 0; + } + } else { + tmp___40 = 0; + } + r134 = (_Bool)tmp___40; + if (r143) { + tmp___41 = 1; + } else if (r123) { + if (ep24) { + tmp___41 = 1; + } else { + goto _L___84; + } + } else + _L___84: /* CIL Label */ + if (r133) { + if (ep34) { + tmp___41 = 1; + } else { + goto _L___83; + } + } else + _L___83: /* CIL Label */ + if (r153) { + if (ep54) { + tmp___41 = 1; + } else { + tmp___41 = 0; + } + } else { + tmp___41 = 0; + } + r144 = (_Bool)tmp___41; + if (r153) { + tmp___42 = 1; + } else if (r123) { + if (ep25) { + tmp___42 = 1; + } else { + goto _L___86; + } + } else + _L___86: /* CIL Label */ + if (r133) { + if (ep35) { + tmp___42 = 1; + } else { + goto _L___85; + } + } else + _L___85: /* CIL Label */ + if (r143) { + if (ep45) { + tmp___42 = 1; + } else { + tmp___42 = 0; + } + } else { + tmp___42 = 0; + } + r154 = (_Bool)tmp___42; + if (r213) { + tmp___43 = 1; + } else if (r233) { + if (ep31) { + tmp___43 = 1; + } else { + goto _L___88; + } + } else + _L___88: /* CIL Label */ + if (r243) { + if (ep41) { + tmp___43 = 1; + } else { + goto _L___87; + } + } else + _L___87: /* CIL Label */ + if (r253) { + if (ep51) { + tmp___43 = 1; + } else { + tmp___43 = 0; + } + } else { + tmp___43 = 0; + } + r214 = (_Bool)tmp___43; + if (r233) { + tmp___44 = 1; + } else if (r213) { + if (ep13) { + tmp___44 = 1; + } else { + goto _L___90; + } + } else + _L___90: /* CIL Label */ + if (r243) { + if (ep43) { + tmp___44 = 1; + } else { + goto _L___89; + } + } else + _L___89: /* CIL Label */ + if (r253) { + if (ep53) { + tmp___44 = 1; + } else { + tmp___44 = 0; + } + } else { + tmp___44 = 0; + } + r234 = (_Bool)tmp___44; + if (r243) { + tmp___45 = 1; + } else if (r213) { + if (ep14) { + tmp___45 = 1; + } else { + goto _L___92; + } + } else + _L___92: /* CIL Label */ + if (r233) { + if (ep34) { + tmp___45 = 1; + } else { + goto _L___91; + } + } else + _L___91: /* CIL Label */ + if (r253) { + if (ep54) { + tmp___45 = 1; + } else { + tmp___45 = 0; + } + } else { + tmp___45 = 0; + } + r244 = (_Bool)tmp___45; + if (r253) { + tmp___46 = 1; + } else if (r213) { + if (ep15) { + tmp___46 = 1; + } else { + goto _L___94; + } + } else + _L___94: /* CIL Label */ + if (r233) { + if (ep35) { + tmp___46 = 1; + } else { + goto _L___93; + } + } else + _L___93: /* CIL Label */ + if (r243) { + if (ep45) { + tmp___46 = 1; + } else { + tmp___46 = 0; + } + } else { + tmp___46 = 0; + } + r254 = (_Bool)tmp___46; + if (r313) { + tmp___47 = 1; + } else if (r323) { + if (ep21) { + tmp___47 = 1; + } else { + goto _L___96; + } + } else + _L___96: /* CIL Label */ + if (r343) { + if (ep41) { + tmp___47 = 1; + } else { + goto _L___95; + } + } else + _L___95: /* CIL Label */ + if (r353) { + if (ep51) { + tmp___47 = 1; + } else { + tmp___47 = 0; + } + } else { + tmp___47 = 0; + } + r314 = (_Bool)tmp___47; + if (r323) { + tmp___48 = 1; + } else if (r313) { + if (ep12) { + tmp___48 = 1; + } else { + goto _L___98; + } + } else + _L___98: /* CIL Label */ + if (r343) { + if (ep42) { + tmp___48 = 1; + } else { + goto _L___97; + } + } else + _L___97: /* CIL Label */ + if (r353) { + if (ep52) { + tmp___48 = 1; + } else { + tmp___48 = 0; + } + } else { + tmp___48 = 0; + } + r324 = (_Bool)tmp___48; + if (r343) { + tmp___49 = 1; + } else if (r313) { + if (ep14) { + tmp___49 = 1; + } else { + goto _L___100; + } + } else + _L___100: /* CIL Label */ + if (r323) { + if (ep24) { + tmp___49 = 1; + } else { + goto _L___99; + } + } else + _L___99: /* CIL Label */ + if (r353) { + if (ep54) { + tmp___49 = 1; + } else { + tmp___49 = 0; + } + } else { + tmp___49 = 0; + } + r344 = (_Bool)tmp___49; + if (r353) { + tmp___50 = 1; + } else if (r313) { + if (ep15) { + tmp___50 = 1; + } else { + goto _L___102; + } + } else + _L___102: /* CIL Label */ + if (r323) { + if (ep25) { + tmp___50 = 1; + } else { + goto _L___101; + } + } else + _L___101: /* CIL Label */ + if (r343) { + if (ep45) { + tmp___50 = 1; + } else { + tmp___50 = 0; + } + } else { + tmp___50 = 0; + } + r354 = (_Bool)tmp___50; + if (r413) { + tmp___51 = 1; + } else if (r423) { + if (ep21) { + tmp___51 = 1; + } else { + goto _L___104; + } + } else + _L___104: /* CIL Label */ + if (r433) { + if (ep31) { + tmp___51 = 1; + } else { + goto _L___103; + } + } else + _L___103: /* CIL Label */ + if (r453) { + if (ep51) { + tmp___51 = 1; + } else { + tmp___51 = 0; + } + } else { + tmp___51 = 0; + } + r414 = (_Bool)tmp___51; + if (r423) { + tmp___52 = 1; + } else if (r413) { + if (ep12) { + tmp___52 = 1; + } else { + goto _L___106; + } + } else + _L___106: /* CIL Label */ + if (r433) { + if (ep32) { + tmp___52 = 1; + } else { + goto _L___105; + } + } else + _L___105: /* CIL Label */ + if (r453) { + if (ep52) { + tmp___52 = 1; + } else { + tmp___52 = 0; + } + } else { + tmp___52 = 0; + } + r424 = (_Bool)tmp___52; + if (r433) { + tmp___53 = 1; + } else if (r413) { + if (ep13) { + tmp___53 = 1; + } else { + goto _L___108; + } + } else + _L___108: /* CIL Label */ + if (r423) { + if (ep23) { + tmp___53 = 1; + } else { + goto _L___107; + } + } else + _L___107: /* CIL Label */ + if (r453) { + if (ep53) { + tmp___53 = 1; + } else { + tmp___53 = 0; + } + } else { + tmp___53 = 0; + } + r434 = (_Bool)tmp___53; + if (r453) { + tmp___54 = 1; + } else if (r413) { + if (ep15) { + tmp___54 = 1; + } else { + goto _L___110; + } + } else + _L___110: /* CIL Label */ + if (r423) { + if (ep25) { + tmp___54 = 1; + } else { + goto _L___109; + } + } else + _L___109: /* CIL Label */ + if (r433) { + if (ep35) { + tmp___54 = 1; + } else { + tmp___54 = 0; + } + } else { + tmp___54 = 0; + } + r454 = (_Bool)tmp___54; + if (r513) { + tmp___55 = 1; + } else if (r523) { + if (ep21) { + tmp___55 = 1; + } else { + goto _L___112; + } + } else + _L___112: /* CIL Label */ + if (r533) { + if (ep31) { + tmp___55 = 1; + } else { + goto _L___111; + } + } else + _L___111: /* CIL Label */ + if (r543) { + if (ep41) { + tmp___55 = 1; + } else { + tmp___55 = 0; + } + } else { + tmp___55 = 0; + } + r514 = (_Bool)tmp___55; + if (r523) { + tmp___56 = 1; + } else if (r513) { + if (ep12) { + tmp___56 = 1; + } else { + goto _L___114; + } + } else + _L___114: /* CIL Label */ + if (r533) { + if (ep32) { + tmp___56 = 1; + } else { + goto _L___113; + } + } else + _L___113: /* CIL Label */ + if (r543) { + if (ep42) { + tmp___56 = 1; + } else { + tmp___56 = 0; + } + } else { + tmp___56 = 0; + } + r524 = (_Bool)tmp___56; + if (r533) { + tmp___57 = 1; + } else if (r513) { + if (ep13) { + tmp___57 = 1; + } else { + goto _L___116; + } + } else + _L___116: /* CIL Label */ + if (r523) { + if (ep23) { + tmp___57 = 1; + } else { + goto _L___115; + } + } else + _L___115: /* CIL Label */ + if (r543) { + if (ep43) { + tmp___57 = 1; + } else { + tmp___57 = 0; + } + } else { + tmp___57 = 0; + } + r534 = (_Bool)tmp___57; + if (r543) { + tmp___58 = 1; + } else if (r513) { + if (ep14) { + tmp___58 = 1; + } else { + goto _L___118; + } + } else + _L___118: /* CIL Label */ + if (r523) { + if (ep24) { + tmp___58 = 1; + } else { + goto _L___117; + } + } else + _L___117: /* CIL Label */ + if (r533) { + if (ep34) { + tmp___58 = 1; + } else { + tmp___58 = 0; + } + } else { + tmp___58 = 0; + } + r544 = (_Bool)tmp___58; + if ((int)id1 != (int)id2) { + if ((int)id1 != (int)id3) { + if ((int)id1 != (int)id4) { + if ((int)id1 != (int)id5) { + if ((int)id2 != (int)id3) { + if ((int)id2 != (int)id4) { + if ((int)id2 != (int)id5) { + if ((int)id3 != (int)id4) { + if ((int)id3 != (int)id5) { + if ((int)id4 != (int)id5) { + if ((int)id1 >= 0) { + if ((int)id2 >= 0) { + if ((int)id3 >= 0) { + if ((int)id4 >= 0) { + if ((int)id5 >= 0) { + if ((int)r1 == 0) { + if ((int)r2 == 0) { + if ((int)r3 == 0) { + if ((int)r4 == 0) { + if ((int)r5 == 0) { + if (r124) { + if (r134) { + if (r144) { + if (r154) { + if (r214) { + if (r234) { + if (r244) { + if (r254) { + if (r314) { + if (r324) { + if (r344) { + if (r354) { + if (r414) { + if (r424) { + if (r434) { + if (r454) { + if (r514) { + if (r524) { + if (r534) { + if (r544) { + if ((int)max1 == (int)id1) { + if ((int)max2 == (int)id2) { + if ((int)max3 == (int)id3) { + if ((int)max4 == (int)id4) { + if ((int)max5 == (int)id5) { + if ((int)st1 == 0) { + if ((int)st2 == 0) { + if ((int)st3 == 0) { + if ((int)st4 == 0) { + if ((int)st5 == 0) { + if ((int)nl1 == 0) { + if ((int)nl2 == 0) { + if ((int)nl3 == 0) { + if ((int)nl4 == 0) { + if ((int)nl5 == 0) { + if ((int)mode1 == 0) { + if ((int)mode2 == 0) { + if ((int)mode3 == 0) { + if ((int)mode4 == 0) { + if ((int)mode5 == 0) { + tmp___59 = 1; + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + } else { + tmp___59 = 0; + } + return (tmp___59); + } +} +int check(void) { + int tmp; + + { + if (((((int)st1 + (int)st2) + (int)st3) + (int)st4) + (int)st5 <= 1) { + if ((int)st1 + (int)nl1 <= 1) { + if ((int)st2 + (int)nl2 <= 1) { + if ((int)st3 + (int)nl3 <= 1) { + if ((int)st4 + (int)nl4 <= 1) { + if ((int)st5 + (int)nl5 <= 1) { + if ((int)r1 >= 4) { + goto _L___1; + } else if (((((int)st1 + (int)st2) + (int)st3) + (int)st4) + (int)st5 == 0) { + _L___1: /* CIL Label */ + if ((int)r1 < 4) { + goto _L___0; + } else if (((((int)st1 + (int)st2) + (int)st3) + (int)st4) + (int)st5 == 1) { + _L___0: /* CIL Label */ + if ((int)r1 >= 4) { + goto _L; + } else if (((((int)nl1 + (int)nl2) + (int)nl3) + (int)nl4) + (int)nl5 == 0) { + _L: /* CIL Label */ + if ((int)r1 < 4) { + tmp = 1; + } else if (((((int)nl1 + (int)nl2) + (int)nl3) + (int)nl4) + (int)nl5 == 4) { + tmp = 1; + } else { + tmp = 0; + } + } else { + tmp = 0; + } + } else { + tmp = 0; + } + } else { + tmp = 0; + } + } else { + tmp = 0; + } + } else { + tmp = 0; + } + } else { + tmp = 0; + } + } else { + tmp = 0; + } + } else { + tmp = 0; + } + } else { + tmp = 0; + } + return (tmp); + } +} +int main(void) { + int c1; + int i2; + + { + c1 = 0; + ep12 = __VERIFIER_nondet_bool(); + ep13 = __VERIFIER_nondet_bool(); + ep14 = __VERIFIER_nondet_bool(); + ep15 = __VERIFIER_nondet_bool(); + ep21 = __VERIFIER_nondet_bool(); + ep23 = __VERIFIER_nondet_bool(); + ep24 = __VERIFIER_nondet_bool(); + ep25 = __VERIFIER_nondet_bool(); + ep31 = __VERIFIER_nondet_bool(); + ep32 = __VERIFIER_nondet_bool(); + ep34 = __VERIFIER_nondet_bool(); + ep35 = __VERIFIER_nondet_bool(); + ep41 = __VERIFIER_nondet_bool(); + ep42 = __VERIFIER_nondet_bool(); + ep43 = __VERIFIER_nondet_bool(); + ep45 = __VERIFIER_nondet_bool(); + ep51 = __VERIFIER_nondet_bool(); + ep52 = __VERIFIER_nondet_bool(); + ep53 = __VERIFIER_nondet_bool(); + ep54 = __VERIFIER_nondet_bool(); + id1 = __VERIFIER_nondet_char(); + r1 = __VERIFIER_nondet_char(); + st1 = __VERIFIER_nondet_char(); + nl1 = __VERIFIER_nondet_char(); + m1 = __VERIFIER_nondet_char(); + max1 = __VERIFIER_nondet_char(); + mode1 = __VERIFIER_nondet_bool(); + id2 = __VERIFIER_nondet_char(); + r2 = __VERIFIER_nondet_char(); + st2 = __VERIFIER_nondet_char(); + nl2 = __VERIFIER_nondet_char(); + m2 = __VERIFIER_nondet_char(); + max2 = __VERIFIER_nondet_char(); + mode2 = __VERIFIER_nondet_bool(); + id3 = __VERIFIER_nondet_char(); + r3 = __VERIFIER_nondet_char(); + st3 = __VERIFIER_nondet_char(); + nl3 = __VERIFIER_nondet_char(); + m3 = __VERIFIER_nondet_char(); + max3 = __VERIFIER_nondet_char(); + mode3 = __VERIFIER_nondet_bool(); + id4 = __VERIFIER_nondet_char(); + r4 = __VERIFIER_nondet_char(); + st4 = __VERIFIER_nondet_char(); + nl4 = __VERIFIER_nondet_char(); + m4 = __VERIFIER_nondet_char(); + max4 = __VERIFIER_nondet_char(); + mode4 = __VERIFIER_nondet_bool(); + id5 = __VERIFIER_nondet_char(); + r5 = __VERIFIER_nondet_char(); + st5 = __VERIFIER_nondet_char(); + nl5 = __VERIFIER_nondet_char(); + m5 = __VERIFIER_nondet_char(); + max5 = __VERIFIER_nondet_char(); + mode5 = __VERIFIER_nondet_bool(); + i2 = init(); + assume_abort_if_not(i2); + p12_old = nomsg; + p12_new = nomsg; + p13_old = nomsg; + p13_new = nomsg; + p14_old = nomsg; + p14_new = nomsg; + p15_old = nomsg; + p15_new = nomsg; + p21_old = nomsg; + p21_new = nomsg; + p23_old = nomsg; + p23_new = nomsg; + p24_old = nomsg; + p24_new = nomsg; + p25_old = nomsg; + p25_new = nomsg; + p31_old = nomsg; + p31_new = nomsg; + p32_old = nomsg; + p32_new = nomsg; + p34_old = nomsg; + p34_new = nomsg; + p35_old = nomsg; + p35_new = nomsg; + p41_old = nomsg; + p41_new = nomsg; + p42_old = nomsg; + p42_new = nomsg; + p43_old = nomsg; + p43_new = nomsg; + p45_old = nomsg; + p45_new = nomsg; + p51_old = nomsg; + p51_new = nomsg; + p52_old = nomsg; + p52_new = nomsg; + p53_old = nomsg; + p53_new = nomsg; + p54_old = nomsg; + p54_new = nomsg; + i2 = 0; + while (i2 < 10) { + { + node1(); + node2(); + node3(); + node4(); + node5(); + p12_old = p12_new; + p12_new = nomsg; + p13_old = p13_new; + p13_new = nomsg; + p14_old = p14_new; + p14_new = nomsg; + p15_old = p15_new; + p15_new = nomsg; + p21_old = p21_new; + p21_new = nomsg; + p23_old = p23_new; + p23_new = nomsg; + p24_old = p24_new; + p24_new = nomsg; + p25_old = p25_new; + p25_new = nomsg; + p31_old = p31_new; + p31_new = nomsg; + p32_old = p32_new; + p32_new = nomsg; + p34_old = p34_new; + p34_new = nomsg; + p35_old = p35_new; + p35_new = nomsg; + p41_old = p41_new; + p41_new = nomsg; + p42_old = p42_new; + p42_new = nomsg; + p43_old = p43_new; + p43_new = nomsg; + p45_old = p45_new; + p45_new = nomsg; + p51_old = p51_new; + p51_new = nomsg; + p52_old = p52_new; + p52_new = nomsg; + p53_old = p53_new; + p53_new = nomsg; + p54_old = p54_new; + p54_new = nomsg; + c1 = check(); + assert(c1); + i2++; + } + } + } + return 0; +} +void assert(_Bool arg) { + + { + if (!arg) { + { + ERROR : { + reach_error(); + abort(); + } + } + } + } +}