extern void __VERIFIER_error() __attribute__ ((__noreturn__)); /********************************************************************** Copyright (c) 2013 Carnegie Mellon University. All Rights Reserved. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following acknowledgments and disclaimers. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The names "Carnegie Mellon University," "SEI" and/or "Software Engineering Institute" shall not be used to endorse or promote products derived from this software without prior written permission. For written permission, please contact permission@sei.cmu.edu. 4. Products derived from this software may not be called "SEI" nor may "SEI" appear in their names without prior written permission of permission@sei.cmu.edu. 5. Redistributions of any form whatsoever must retain the following acknowledgment: This material is based upon work funded and supported by the Department of Defense under Contract No. FA8721-05-C-0003 with Carnegie Mellon University for the operation of the Software Engineering Institute, a federally funded research and development center. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the United States Department of Defense. NO WARRANTY. THIS CARNEGIE MELLON UNIVERSITY AND SOFTWARE ENGINEERING INSTITUTE MATERIAL IS FURNISHEDON AN "AS-IS" BASIS. CARNEGIE MELLON UNIVERSITY MAKES NO WARRANTIES OF ANY KIND, EITHER EXPRESSED OR IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF FITNESS FOR PURPOSE OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT, TRADEMARK, OR COPYRIGHT INFRINGEMENT. This material has been approved for public release and unlimited distribution. DM-0000575 **********************************************************************/ /* Generated by CIL v. 1.6.0 */ /* print_CIL_Input is true */ char __VERIFIER_nondet_char(void) ; unsigned char __VERIFIER_nondet_uchar(void) ; _Bool __VERIFIER_nondet_bool(void) ; void assert(_Bool arg ) ; void __VERIFIER_assume(int arg ) ; 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 ; unsigned char r1 ; char st1 ; char nl1 ; char m1 ; char max1 ; _Bool mode1 ; _Bool newmax1 ; char id2 ; unsigned char r2 ; char st2 ; char nl2 ; char m2 ; char max2 ; _Bool mode2 ; _Bool newmax2 ; char id3 ; unsigned char r3 ; char st3 ; char nl3 ; char m3 ; char max3 ; _Bool mode3 ; _Bool newmax3 ; char id4 ; unsigned char r4 ; char st4 ; char nl4 ; char m4 ; char max4 ; _Bool mode4 ; _Bool newmax4 ; char id5 ; unsigned char r5 ; char st5 ; char nl5 ; char m5 ; char max5 ; _Bool mode5 ; _Bool newmax5 ; void node1(void) { _Bool newmax ; { newmax = (_Bool)0; if (mode1) { if (r1 == 255) { r1 = 4; } r1 = r1 + 1; if (ep21) { m1 = p21_old; p21_old = nomsg; if ((int )m1 > (int )max1) { max1 = m1; newmax = (_Bool)1; } } if (ep31) { m1 = p31_old; p31_old = nomsg; if ((int )m1 > (int )max1) { max1 = m1; newmax = (_Bool)1; } } if (ep41) { m1 = p41_old; p41_old = nomsg; if ((int )m1 > (int )max1) { max1 = m1; newmax = (_Bool)1; } } if (ep51) { m1 = p51_old; p51_old = nomsg; if ((int )m1 > (int )max1) { max1 = m1; newmax = (_Bool)1; } } newmax1 = newmax; if ((int )r1 == 4) { if ((int )max1 == (int )id1) { st1 = (char)1; } else { nl1 = (char)1; } } mode1 = (_Bool)0; } else { if ((int )r1 < 4) { if (ep12) { if (newmax1) { p12_new = max1 != nomsg && p12_new == nomsg ? max1 : p12_new; } } if (ep13) { if (newmax1) { p13_new = max1 != nomsg && p13_new == nomsg ? max1 : p13_new; } } if (ep14) { if (newmax1) { p14_new = max1 != nomsg && p14_new == nomsg ? max1 : p14_new; } } if (ep15) { if (newmax1) { p15_new = max1 != nomsg && p15_new == nomsg ? max1 : p15_new; } } } mode1 = (_Bool)1; } return; } } void node2(void) { _Bool newmax ; { newmax = (_Bool)0; if (mode2) { if (r2 == 255) { r2 = 4; } r2 = r2 + 1; if (ep12) { m2 = p12_old; p12_old = nomsg; if ((int )m2 > (int )max2) { max2 = m2; newmax = (_Bool)1; } } if (ep32) { m2 = p32_old; p32_old = nomsg; if ((int )m2 > (int )max2) { max2 = m2; newmax = (_Bool)1; } } if (ep42) { m2 = p42_old; p42_old = nomsg; if ((int )m2 > (int )max2) { max2 = m2; newmax = (_Bool)1; } } if (ep52) { m2 = p52_old; p52_old = nomsg; if ((int )m2 > (int )max2) { max2 = m2; newmax = (_Bool)1; } } newmax2 = newmax; 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) { if (newmax2) { p21_new = max2 != nomsg && p21_new == nomsg ? max2 : p21_new; } } if (ep23) { if (newmax2) { p23_new = max2 != nomsg && p23_new == nomsg ? max2 : p23_new; } } if (ep24) { if (newmax2) { p24_new = max2 != nomsg && p24_new == nomsg ? max2 : p24_new; } } if (ep25) { if (newmax2) { p25_new = max2 != nomsg && p25_new == nomsg ? max2 : p25_new; } } } mode2 = (_Bool)1; } return; } } void node3(void) { _Bool newmax ; { newmax = (_Bool)0; if (mode3) { if (r3 == 255) { r3 = 4; } r3 = r3 + 1; if (ep13) { m3 = p13_old; p13_old = nomsg; if ((int )m3 > (int )max3) { max3 = m3; newmax = (_Bool)1; } } if (ep23) { m3 = p23_old; p23_old = nomsg; if ((int )m3 > (int )max3) { max3 = m3; newmax = (_Bool)1; } } if (ep43) { m3 = p43_old; p43_old = nomsg; if ((int )m3 > (int )max3) { max3 = m3; newmax = (_Bool)1; } } if (ep53) { m3 = p53_old; p53_old = nomsg; if ((int )m3 > (int )max3) { max3 = m3; newmax = (_Bool)1; } } newmax3 = newmax; 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) { if (newmax3) { p31_new = max3 != nomsg && p31_new == nomsg ? max3 : p31_new; } } if (ep32) { if (newmax3) { p32_new = max3 != nomsg && p32_new == nomsg ? max3 : p32_new; } } if (ep34) { if (newmax3) { p34_new = max3 != nomsg && p34_new == nomsg ? max3 : p34_new; } } if (ep35) { if (newmax3) { p35_new = max3 != nomsg && p35_new == nomsg ? max3 : p35_new; } } } mode3 = (_Bool)1; } return; } } void node4(void) { _Bool newmax ; { newmax = (_Bool)0; if (mode4) { if (r4 == 255) { r4 = 4; } r4 = r4 + 1; if (ep14) { m4 = p14_old; p14_old = nomsg; if ((int )m4 > (int )max4) { max4 = m4; newmax = (_Bool)1; } } if (ep24) { m4 = p24_old; p24_old = nomsg; if ((int )m4 > (int )max4) { max4 = m4; newmax = (_Bool)1; } } if (ep34) { m4 = p34_old; p34_old = nomsg; if ((int )m4 > (int )max4) { max4 = m4; newmax = (_Bool)1; } } if (ep54) { m4 = p54_old; p54_old = nomsg; if ((int )m4 > (int )max4) { max4 = m4; newmax = (_Bool)1; } } newmax4 = newmax; 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) { if (newmax4) { p41_new = max4 != nomsg && p41_new == nomsg ? max4 : p41_new; } } if (ep42) { if (newmax4) { p42_new = max4 != nomsg && p42_new == nomsg ? max4 : p42_new; } } if (ep43) { if (newmax4) { p43_new = max4 != nomsg && p43_new == nomsg ? max4 : p43_new; } } if (ep45) { if (newmax4) { p45_new = max4 != nomsg && p45_new == nomsg ? max4 : p45_new; } } } mode4 = (_Bool)1; } return; } } void node5(void) { _Bool newmax ; { newmax = (_Bool)0; if (mode5) { if (r5 == 255) { r5 = 4; } r5 = r5 + 1; if (ep15) { m5 = p15_old; p15_old = nomsg; if ((int )m5 > (int )max5) { max5 = m5; newmax = (_Bool)1; } } if (ep25) { m5 = p25_old; p25_old = nomsg; if ((int )m5 > (int )max5) { max5 = m5; newmax = (_Bool)1; } } if (ep35) { m5 = p35_old; p35_old = nomsg; if ((int )m5 > (int )max5) { max5 = m5; newmax = (_Bool)1; } } if (ep45) { m5 = p45_old; p45_old = nomsg; if ((int )m5 > (int )max5) { max5 = m5; newmax = (_Bool)1; } } newmax5 = newmax; 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) { if (newmax5) { p51_new = max5 != nomsg && p51_new == nomsg ? max5 : p51_new; } } if (ep52) { if (newmax5) { p52_new = max5 != nomsg && p52_new == nomsg ? max5 : p52_new; } } if (ep53) { if (newmax5) { p53_new = max5 != nomsg && p53_new == nomsg ? max5 : p53_new; } } if (ep54) { if (newmax5) { p54_new = max5 != nomsg && p54_new == nomsg ? max5 : p54_new; } } } mode5 = (_Bool)1; } return; } } void (*nodes[5])(void) = { & node1, & node2, & node3, & node4, & node5}; 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) { if (newmax1) { if (newmax2) { if (newmax3) { if (newmax4) { if (newmax5) { 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; } } 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_uchar(); st1 = __VERIFIER_nondet_char(); nl1 = __VERIFIER_nondet_char(); m1 = __VERIFIER_nondet_char(); max1 = __VERIFIER_nondet_char(); mode1 = __VERIFIER_nondet_bool(); newmax1 = __VERIFIER_nondet_bool(); id2 = __VERIFIER_nondet_char(); r2 = __VERIFIER_nondet_uchar(); st2 = __VERIFIER_nondet_char(); nl2 = __VERIFIER_nondet_char(); m2 = __VERIFIER_nondet_char(); max2 = __VERIFIER_nondet_char(); mode2 = __VERIFIER_nondet_bool(); newmax2 = __VERIFIER_nondet_bool(); id3 = __VERIFIER_nondet_char(); r3 = __VERIFIER_nondet_uchar(); st3 = __VERIFIER_nondet_char(); nl3 = __VERIFIER_nondet_char(); m3 = __VERIFIER_nondet_char(); max3 = __VERIFIER_nondet_char(); mode3 = __VERIFIER_nondet_bool(); newmax3 = __VERIFIER_nondet_bool(); id4 = __VERIFIER_nondet_char(); r4 = __VERIFIER_nondet_uchar(); st4 = __VERIFIER_nondet_char(); nl4 = __VERIFIER_nondet_char(); m4 = __VERIFIER_nondet_char(); max4 = __VERIFIER_nondet_char(); mode4 = __VERIFIER_nondet_bool(); newmax4 = __VERIFIER_nondet_bool(); id5 = __VERIFIER_nondet_char(); r5 = __VERIFIER_nondet_uchar(); st5 = __VERIFIER_nondet_char(); nl5 = __VERIFIER_nondet_char(); m5 = __VERIFIER_nondet_char(); max5 = __VERIFIER_nondet_char(); mode5 = __VERIFIER_nondet_bool(); newmax5 = __VERIFIER_nondet_bool(); i2 = init(); __VERIFIER_assume(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 (1) { { 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); } } } return 0; } void assert(_Bool arg ) { { if (! arg) { { ERROR: __VERIFIER_error(); } } } }