// This file is part of the SV-Benchmarks collection of verification tasks: // https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks // // SPDX-FileCopyrightText: 2022 Jana (Philipp) Berger // // SPDX-License-Identifier: GPL-3.0-or-later extern unsigned long __VERIFIER_nondet_ulong(); extern long __VERIFIER_nondet_long(); extern unsigned char __VERIFIER_nondet_uchar(); extern char __VERIFIER_nondet_char(); extern unsigned short __VERIFIER_nondet_ushort(); extern short __VERIFIER_nondet_short(); extern float __VERIFIER_nondet_float(); extern double __VERIFIER_nondet_double(); 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", "Req1_Prop1_Batch96PS_CN_500.c", 13, "reach_error"); } void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } return; } void assume_abort_if_not(int cond) { if(!cond) { abort(); } } unsigned char isInitial = 0; signed char var_1_1 = 16; unsigned char var_1_4 = 0; unsigned char var_1_6 = 1; signed char var_1_8 = -10; unsigned short int var_1_9 = 4; signed char var_1_10 = 8; unsigned short int var_1_12 = 64314; unsigned short int var_1_13 = 26169; signed char var_1_17 = 50; signed char var_1_18 = 16; signed char var_1_19 = 5; signed char var_1_20 = 0; signed char var_1_21 = 50; signed char var_1_22 = 16; unsigned char var_1_23 = 16; unsigned char var_1_24 = 1; unsigned char var_1_25 = 0; double var_1_27 = 0.25; double var_1_28 = 10.25; double var_1_29 = 1000.25; double var_1_30 = 9.5; float var_1_31 = 63.5; unsigned short int var_1_32 = 16; unsigned long int var_1_33 = 500; unsigned long int var_1_34 = 10; signed char var_1_35 = 1; unsigned char var_1_36 = 0; unsigned short int var_1_37 = 16; unsigned short int var_1_38 = 10; unsigned short int var_1_39 = 64; unsigned char var_1_40 = 1; signed char var_1_41 = 25; signed char var_1_42 = 32; unsigned char var_1_43 = 0; unsigned char var_1_44 = 1; unsigned char var_1_45 = 200; signed long int var_1_46 = -50; unsigned char var_1_47 = 25; signed short int var_1_48 = 0; unsigned short int var_1_49 = 50; unsigned long int var_1_50 = 16; unsigned long int var_1_51 = 3417354380; unsigned long int var_1_52 = 64; float var_1_53 = 9.5; float var_1_54 = 500.75; float var_1_55 = 3.1; float var_1_56 = 1.7; double var_1_57 = -0.5; unsigned long int var_1_58 = 16; double var_1_59 = 3.875; double var_1_60 = 128.75; float var_1_61 = 100000.475; unsigned char var_1_62 = 16; signed short int var_1_63 = -16; signed long int var_1_64 = 5; signed long int var_1_65 = 100; signed short int var_1_66 = 32; unsigned short int var_1_67 = 64; unsigned short int var_1_68 = 20270; unsigned short int var_1_69 = 26162; unsigned short int var_1_70 = 40886; signed short int var_1_71 = 256; float var_1_72 = 7.15; signed short int var_1_73 = 8; signed long int var_1_74 = -32; float var_1_75 = 0.625; double var_1_76 = 100.375; signed long int var_1_77 = -256; signed char var_1_78 = -1; signed char var_1_79 = 5; signed char var_1_80 = 1; signed char var_1_81 = -8; unsigned short int var_1_82 = 256; unsigned short int var_1_83 = 100; unsigned short int var_1_84 = 5; float var_1_85 = 1.5; signed short int var_1_86 = -500; signed char var_1_87 = -128; unsigned char var_1_88 = 0; float var_1_89 = 3.5; float var_1_90 = 25.25; float var_1_91 = 49.23; float var_1_92 = 64.4; signed short int var_1_93 = 10; signed short int var_1_94 = 0; double var_1_95 = 2.2; unsigned char var_1_96 = 16; double var_1_97 = 2.9; double var_1_98 = 0.0; double var_1_99 = 4.5; double var_1_100 = 127.6; unsigned short int var_1_101 = 100; unsigned char var_1_102 = 128; unsigned char var_1_103 = 128; unsigned char var_1_104 = 64; unsigned char var_1_105 = 64; unsigned char var_1_106 = 1; unsigned short int var_1_107 = 1; unsigned char var_1_108 = 0; unsigned char var_1_109 = 0; float var_1_110 = 64.5; unsigned char var_1_111 = 0; signed short int var_1_112 = 0; unsigned long int var_1_113 = 32; unsigned long int var_1_114 = 25; unsigned long int var_1_115 = 1789229886; double var_1_116 = 7.9; signed short int var_1_117 = -100; unsigned char var_1_118 = 0; signed long int var_1_119 = 256; signed short int var_1_120 = -10; signed short int var_1_121 = -2; float var_1_122 = 7.115; signed long int var_1_123 = -256; unsigned char var_1_124 = 1; unsigned char var_1_125 = 1; float var_1_126 = 25.5; unsigned long int var_1_127 = 128; signed char var_1_128 = 64; double var_1_129 = 4.2; float var_1_130 = 9.5; signed char var_1_131 = -16; unsigned short int var_1_132 = 4; unsigned short int var_1_133 = 128; unsigned short int var_1_134 = 32; double var_1_135 = 0.09999999999999998; double var_1_136 = 999.25; signed long int var_1_137 = 8; signed long int var_1_138 = -256; unsigned char var_1_139 = 1; float var_1_140 = 3.3; double var_1_141 = 99.5; unsigned char var_1_142 = 100; unsigned short int last_1_var_1_9 = 4; void initially(void) { } void step(void) { if ((var_1_34 <= var_1_33) || var_1_36) { if (((((5) < 0 ) ? -(5) : (5))) < var_1_34) { if (var_1_36) { var_1_32 = ((((((((var_1_37) < (var_1_38)) ? (var_1_37) : (var_1_38)))) > (var_1_39)) ? (((((var_1_37) < (var_1_38)) ? (var_1_37) : (var_1_38)))) : (var_1_39))); } } } if (((((4) < 0 ) ? -(4) : (4))) >= var_1_37) { if ((((((var_1_41) < 0 ) ? -(var_1_41) : (var_1_41))) % ((((var_1_35) < (var_1_42)) ? (var_1_35) : (var_1_42)))) <= (var_1_39 ^ var_1_37)) { if (((((((((var_1_41) < 0 ) ? -(var_1_41) : (var_1_41)))) < (var_1_42)) ? (((((var_1_41) < 0 ) ? -(var_1_41) : (var_1_41)))) : (var_1_42))) < var_1_38) { var_1_40 = var_1_43; } else { var_1_40 = (! (! var_1_44)); } } } if ((((((((var_1_39) < 0 ) ? -(var_1_39) : (var_1_39))) < 0 ) ? -((((var_1_39) < 0 ) ? -(var_1_39) : (var_1_39))) : ((((var_1_39) < 0 ) ? -(var_1_39) : (var_1_39))))) <= ((((var_1_41) < 0 ) ? -(var_1_41) : (var_1_41)))) { if ((~ var_1_46) > var_1_34) { var_1_45 = var_1_47; } } else { var_1_45 = var_1_47; } if (var_1_38 < (var_1_46 % var_1_49)) { if ((var_1_46 >> var_1_41) <= (((((((var_1_32) < 0 ) ? -(var_1_32) : (var_1_32))) < 0 ) ? -((((var_1_32) < 0 ) ? -(var_1_32) : (var_1_32))) : ((((var_1_32) < 0 ) ? -(var_1_32) : (var_1_32)))))) { var_1_48 = (((((((var_1_42) < (((((var_1_45) < 0 ) ? -(var_1_45) : (var_1_45))))) ? (var_1_42) : (((((var_1_45) < 0 ) ? -(var_1_45) : (var_1_45)))))) < 0 ) ? -((((var_1_42) < (((((var_1_45) < 0 ) ? -(var_1_45) : (var_1_45))))) ? (var_1_42) : (((((var_1_45) < 0 ) ? -(var_1_45) : (var_1_45)))))) : ((((var_1_42) < (((((var_1_45) < 0 ) ? -(var_1_45) : (var_1_45))))) ? (var_1_42) : (((((var_1_45) < 0 ) ? -(var_1_45) : (var_1_45)))))))); } } if ((~ (var_1_51 - var_1_52)) <= var_1_45) { if (var_1_32 < var_1_38) { var_1_50 = ((((var_1_52) < 0 ) ? -(var_1_52) : (var_1_52))); } else { var_1_50 = var_1_52; } } var_1_53 = ((((var_1_54) > (var_1_55)) ? (var_1_54) : (var_1_55))); if (var_1_44) { if (((((var_1_53) < 0 ) ? -(var_1_53) : (var_1_53))) < ((((var_1_54) < 0 ) ? -(var_1_54) : (var_1_54)))) { var_1_56 = ((((((((3.6f) > (((((var_1_55) < 0 ) ? -(var_1_55) : (var_1_55))))) ? (3.6f) : (((((var_1_55) < 0 ) ? -(var_1_55) : (var_1_55))))))) < (((((var_1_54) < 0 ) ? -(var_1_54) : (var_1_54))))) ? (((((3.6f) > (((((var_1_55) < 0 ) ? -(var_1_55) : (var_1_55))))) ? (3.6f) : (((((var_1_55) < 0 ) ? -(var_1_55) : (var_1_55))))))) : (((((var_1_54) < 0 ) ? -(var_1_54) : (var_1_54)))))); } else { var_1_56 = var_1_54; } } else { var_1_56 = ((((64.6f) > (((((var_1_55) < 0 ) ? -(var_1_55) : (var_1_55))))) ? (64.6f) : (((((var_1_55) < 0 ) ? -(var_1_55) : (var_1_55)))))); } if (((var_1_51 + var_1_46) / ((((var_1_49) < (var_1_58)) ? (var_1_49) : (var_1_58)))) <= var_1_52) { if (var_1_50 > ((var_1_49 % 256u) / (var_1_51 - 100u))) { var_1_57 = (var_1_59 + ((((var_1_60) < 0 ) ? -(var_1_60) : (var_1_60)))); } } if (var_1_43 || var_1_44) { if (var_1_46 >= (~ var_1_45)) { if (var_1_41 <= var_1_58) { var_1_61 = (((((((var_1_60 + var_1_59) < 0 ) ? -(var_1_60 + var_1_59) : (var_1_60 + var_1_59))) < 0 ) ? -((((var_1_60 + var_1_59) < 0 ) ? -(var_1_60 + var_1_59) : (var_1_60 + var_1_59))) : ((((var_1_60 + var_1_59) < 0 ) ? -(var_1_60 + var_1_59) : (var_1_60 + var_1_59))))); } else { var_1_61 = var_1_54; } } else { var_1_61 = var_1_60; } } else { if (var_1_47 > var_1_62) { var_1_61 = ((((var_1_55) < ((var_1_60 + 256.4f))) ? (var_1_55) : ((var_1_60 + 256.4f)))); } } if (var_1_46 <= var_1_34) { if (-256 < var_1_32) { var_1_63 = ((((100) < 0 ) ? -(100) : (100))); } } else { var_1_63 = ((((var_1_47) < 0 ) ? -(var_1_47) : (var_1_47))); } if (-16 >= (-1 | (2 / var_1_49))) { if ((var_1_53 + var_1_61) < (- var_1_54)) { var_1_64 = var_1_62; } else { var_1_64 = ((((((((var_1_38 - var_1_47) < 0 ) ? -(var_1_38 - var_1_47) : (var_1_38 - var_1_47)))) < (var_1_32)) ? (((((var_1_38 - var_1_47) < 0 ) ? -(var_1_38 - var_1_47) : (var_1_38 - var_1_47)))) : (var_1_32))); } } if (var_1_63 <= var_1_66) { var_1_65 = ((((var_1_39) < 0 ) ? -(var_1_39) : (var_1_39))); } if (var_1_43 || (((((var_1_61) < 0 ) ? -(var_1_61) : (var_1_61))) < var_1_53)) { if (var_1_47 <= var_1_33) { var_1_67 = ((var_1_68 + var_1_69) - var_1_47); } else { var_1_67 = var_1_45; } } else { var_1_67 = (var_1_70 - var_1_62); } if (var_1_45 <= var_1_58) { if (var_1_44) { var_1_71 = var_1_35; } } if (var_1_40 || (var_1_67 >= var_1_69)) { var_1_72 = ((((var_1_60) < 0 ) ? -(var_1_60) : (var_1_60))); } if (var_1_36) { if (! var_1_43) { var_1_73 = var_1_45; } } else { var_1_73 = var_1_62; } var_1_74 = ((((var_1_70) > (var_1_73)) ? (var_1_70) : (var_1_73))); if (var_1_60 <= (var_1_76 - 3.6)) { if (var_1_40) { var_1_75 = ((((((((((((var_1_60) < (var_1_54)) ? (var_1_60) : (var_1_54)))) > (25.5f)) ? (((((var_1_60) < (var_1_54)) ? (var_1_60) : (var_1_54)))) : (25.5f)))) > (var_1_59)) ? (((((((((var_1_60) < (var_1_54)) ? (var_1_60) : (var_1_54)))) > (25.5f)) ? (((((var_1_60) < (var_1_54)) ? (var_1_60) : (var_1_54)))) : (25.5f)))) : (var_1_59))); } } if ((var_1_52 | 64) != var_1_32) { var_1_77 = ((((((((var_1_66) < 0 ) ? -(var_1_66) : (var_1_66)))) > (var_1_49)) ? (((((var_1_66) < 0 ) ? -(var_1_66) : (var_1_66)))) : (var_1_49))); } else { var_1_77 = (((((((var_1_35) < 0 ) ? -(var_1_35) : (var_1_35))) < 0 ) ? -((((var_1_35) < 0 ) ? -(var_1_35) : (var_1_35))) : ((((var_1_35) < 0 ) ? -(var_1_35) : (var_1_35))))); } if (((var_1_32 ^ -5) > var_1_39) && var_1_40) { var_1_78 = (((((var_1_79 - var_1_80)) < (var_1_81)) ? ((var_1_79 - var_1_80)) : (var_1_81))); } if ((- var_1_54) >= var_1_72) { if (var_1_43) { var_1_82 = ((((1) < 0 ) ? -(1) : (1))); } else { if (var_1_36) { var_1_82 = var_1_38; } else { var_1_82 = (var_1_70 - (var_1_80 + var_1_45)); } } } if ((var_1_80 >> var_1_47) >= (-50 / var_1_35)) { if (! var_1_40) { var_1_83 = ((((var_1_84) > (((((var_1_39) < (var_1_47)) ? (var_1_39) : (var_1_47))))) ? (var_1_84) : (((((var_1_39) < (var_1_47)) ? (var_1_39) : (var_1_47)))))); } } else { if ((var_1_76 - var_1_85) > var_1_54) { var_1_83 = (((((200) < 0 ) ? -(200) : (200))) + var_1_80); } else { if (((((var_1_60) < ((var_1_76 - var_1_85))) ? (var_1_60) : ((var_1_76 - var_1_85)))) < (var_1_72 + (- var_1_61))) { if (var_1_52 >= var_1_68) { var_1_83 = (var_1_70 - var_1_45); } else { var_1_83 = (var_1_70 - 128); } } } } if ((- (var_1_67 * var_1_52)) > ((((var_1_65 % var_1_51) < 0 ) ? -(var_1_65 % var_1_51) : (var_1_65 % var_1_51)))) { var_1_86 = ((((var_1_81) < 0 ) ? -(var_1_81) : (var_1_81))); } if (var_1_37 <= var_1_52) { var_1_87 = ((((((((var_1_79) < 0 ) ? -(var_1_79) : (var_1_79)))) < (var_1_81)) ? (((((var_1_79) < 0 ) ? -(var_1_79) : (var_1_79)))) : (var_1_81))); } if (var_1_40) { if (var_1_44 || ((var_1_65 % var_1_68) < var_1_38)) { var_1_88 = ((((var_1_47) < 0 ) ? -(var_1_47) : (var_1_47))); } else { var_1_88 = 8; } } if (var_1_82 <= var_1_34) { var_1_89 = (((((var_1_90) < (var_1_91)) ? (var_1_90) : (var_1_91))) - var_1_92); } if (var_1_53 > 0.5f) { var_1_93 = (((((var_1_88) < 0 ) ? -(var_1_88) : (var_1_88))) + var_1_47); } if (var_1_48 > (var_1_80 & var_1_58)) { var_1_94 = ((((var_1_80) < 0 ) ? -(var_1_80) : (var_1_80))); } else { var_1_94 = ((((var_1_78) < (((((var_1_45 - var_1_47) < 0 ) ? -(var_1_45 - var_1_47) : (var_1_45 - var_1_47))))) ? (var_1_78) : (((((var_1_45 - var_1_47) < 0 ) ? -(var_1_45 - var_1_47) : (var_1_45 - var_1_47)))))); } if (var_1_67 == ((((- var_1_66) < 0 ) ? -(- var_1_66) : (- var_1_66)))) { if (var_1_60 < var_1_53) { var_1_95 = (2.375 + var_1_60); } else { var_1_95 = ((((var_1_90) < (var_1_91)) ? (var_1_90) : (var_1_91))); } } var_1_96 = var_1_80; if (var_1_44) { if ((- ((((var_1_50) < 0 ) ? -(var_1_50) : (var_1_50)))) <= var_1_52) { var_1_97 = ((((var_1_91) < 0 ) ? -(var_1_91) : (var_1_91))); } else { var_1_97 = (((((var_1_98 - var_1_99) - var_1_91) < 0 ) ? -((var_1_98 - var_1_99) - var_1_91) : ((var_1_98 - var_1_99) - var_1_91))); } } else { if ((128 ^ var_1_45) > (var_1_34 | var_1_80)) { var_1_97 = ((((var_1_54) < (var_1_92)) ? (var_1_54) : (var_1_92))); } else { if (var_1_36) { var_1_97 = (((((((var_1_59) < 0 ) ? -(var_1_59) : (var_1_59))) < 0 ) ? -((((var_1_59) < 0 ) ? -(var_1_59) : (var_1_59))) : ((((var_1_59) < 0 ) ? -(var_1_59) : (var_1_59))))); } else { var_1_97 = ((((var_1_100) < 0 ) ? -(var_1_100) : (var_1_100))); } } } if (var_1_42 != var_1_68) { if (var_1_48 >= var_1_52) { var_1_101 = 2; } } if (var_1_32 < var_1_34) { if (var_1_57 < var_1_72) { if (var_1_40) { if (((((2.5f) > (var_1_97)) ? (2.5f) : (var_1_97))) >= ((((var_1_61) < 0 ) ? -(var_1_61) : (var_1_61)))) { var_1_102 = ((((1) < (var_1_47)) ? (1) : (var_1_47))); } else { var_1_102 = (var_1_103 - (((((var_1_104) < (var_1_105)) ? (var_1_104) : (var_1_105))) - var_1_106)); } } else { var_1_102 = var_1_104; } } } else { if ((var_1_84 >> var_1_101) > var_1_45) { if (var_1_36) { var_1_102 = (var_1_105 + var_1_106); } } else { var_1_102 = (var_1_103 - ((((var_1_106) < 0 ) ? -(var_1_106) : (var_1_106)))); } } if ((~ var_1_70) < ((((var_1_106) < 0 ) ? -(var_1_106) : (var_1_106)))) { var_1_107 = ((((var_1_62) < (var_1_39)) ? (var_1_62) : (var_1_39))); } if (var_1_73 < var_1_46) { if ((((((((4) < 0 ) ? -(4) : (4))) < 0 ) ? -((((4) < 0 ) ? -(4) : (4))) : ((((4) < 0 ) ? -(4) : (4))))) < ((var_1_65 & var_1_81) + var_1_79)) { var_1_108 = (! var_1_44); } } else { if (var_1_40) { var_1_108 = ((var_1_56 > var_1_95) && var_1_109); } } if ((var_1_47 ^ var_1_73) >= var_1_67) { var_1_110 = ((((var_1_98) < 0 ) ? -(var_1_98) : (var_1_98))); } if (var_1_97 > (- 0.95)) { var_1_111 = (var_1_36 || var_1_43); } if (((var_1_65 / var_1_35) >> var_1_58) > (var_1_77 | var_1_50)) { var_1_112 = (((((var_1_102 - ((((var_1_105) < 0 ) ? -(var_1_105) : (var_1_105))))) > (var_1_106)) ? ((var_1_102 - ((((var_1_105) < 0 ) ? -(var_1_105) : (var_1_105))))) : (var_1_106))); } if (((((var_1_76) < 0 ) ? -(var_1_76) : (var_1_76))) <= var_1_61) { if ((~ var_1_73) <= 32) { var_1_113 = (var_1_114 + (var_1_115 - var_1_102)); } } if (! (7.2 > ((((var_1_72) < 0 ) ? -(var_1_72) : (var_1_72))))) { var_1_116 = var_1_59; } if (! var_1_111) { var_1_117 = ((((((var_1_104) < (var_1_96)) ? (var_1_104) : (var_1_96))) + ((((var_1_47) < (var_1_103)) ? (var_1_47) : (var_1_103)))) - var_1_106); } else { var_1_117 = (((((((var_1_88) < 0 ) ? -(var_1_88) : (var_1_88))) < 0 ) ? -((((var_1_88) < 0 ) ? -(var_1_88) : (var_1_88))) : ((((var_1_88) < 0 ) ? -(var_1_88) : (var_1_88))))); } if ((var_1_82 ^ var_1_41) <= (((((((var_1_119) > (5)) ? (var_1_119) : (5))) < 0 ) ? -((((var_1_119) > (5)) ? (var_1_119) : (5))) : ((((var_1_119) > (5)) ? (var_1_119) : (5)))))) { var_1_118 = (! (! var_1_109)); } else { var_1_118 = ((var_1_105 < var_1_69) || var_1_43); } if (((var_1_82 | var_1_47) >> var_1_58) >= var_1_117) { if (var_1_111) { var_1_120 = ((((((((var_1_62) > ((5 - var_1_80))) ? (var_1_62) : ((5 - var_1_80))))) > ((var_1_45 + ((((var_1_42) > (var_1_41)) ? (var_1_42) : (var_1_41)))))) ? (((((var_1_62) > ((5 - var_1_80))) ? (var_1_62) : ((5 - var_1_80))))) : ((var_1_45 + ((((var_1_42) > (var_1_41)) ? (var_1_42) : (var_1_41))))))); } } else { var_1_120 = var_1_80; } if (var_1_78 <= var_1_46) { if (var_1_108 && (var_1_74 > var_1_117)) { var_1_121 = ((((var_1_105) < 0 ) ? -(var_1_105) : (var_1_105))); } else { var_1_121 = ((((var_1_78) > ((var_1_62 - var_1_104))) ? (var_1_78) : ((var_1_62 - var_1_104)))); } } if (var_1_71 > var_1_42) { var_1_122 = var_1_54; } if (((((-2) > ((var_1_115 / 32))) ? (-2) : ((var_1_115 / 32)))) >= var_1_62) { var_1_123 = ((((var_1_32) < (((((((((var_1_67) < 0 ) ? -(var_1_67) : (var_1_67)))) < (((((var_1_68) < 0 ) ? -(var_1_68) : (var_1_68))))) ? (((((var_1_67) < 0 ) ? -(var_1_67) : (var_1_67)))) : (((((var_1_68) < 0 ) ? -(var_1_68) : (var_1_68)))))))) ? (var_1_32) : (((((((((var_1_67) < 0 ) ? -(var_1_67) : (var_1_67)))) < (((((var_1_68) < 0 ) ? -(var_1_68) : (var_1_68))))) ? (((((var_1_67) < 0 ) ? -(var_1_67) : (var_1_67)))) : (((((var_1_68) < 0 ) ? -(var_1_68) : (var_1_68))))))))); } else { var_1_123 = (((((var_1_80) > ((var_1_96 + var_1_120))) ? (var_1_80) : ((var_1_96 + var_1_120)))) + var_1_68); } if (! ((var_1_104 & var_1_52) >= var_1_62)) { if (var_1_108 || var_1_125) { var_1_124 = (var_1_36 || var_1_43); } else { var_1_124 = (! var_1_109); } } else { if (var_1_125) { var_1_124 = (var_1_44 || var_1_43); } } if (var_1_36) { if ((var_1_51 - ((((var_1_103) < (var_1_49)) ? (var_1_103) : (var_1_49)))) < var_1_127) { var_1_126 = ((((((((4.7f + var_1_99) < 0 ) ? -(4.7f + var_1_99) : (4.7f + var_1_99)))) > ((((((((var_1_90) < 0 ) ? -(var_1_90) : (var_1_90))) < 0 ) ? -((((var_1_90) < 0 ) ? -(var_1_90) : (var_1_90))) : ((((var_1_90) < 0 ) ? -(var_1_90) : (var_1_90))))))) ? (((((4.7f + var_1_99) < 0 ) ? -(4.7f + var_1_99) : (4.7f + var_1_99)))) : ((((((((var_1_90) < 0 ) ? -(var_1_90) : (var_1_90))) < 0 ) ? -((((var_1_90) < 0 ) ? -(var_1_90) : (var_1_90))) : ((((var_1_90) < 0 ) ? -(var_1_90) : (var_1_90)))))))); } } if (((((var_1_97) < (var_1_59)) ? (var_1_97) : (var_1_59))) <= var_1_129) { var_1_128 = var_1_106; } if (var_1_36) { var_1_130 = var_1_59; } else { var_1_130 = var_1_59; } var_1_131 = var_1_81; if (var_1_118) { var_1_132 = var_1_47; } else { var_1_132 = var_1_133; } if (var_1_43) { var_1_134 = var_1_38; } if (var_1_40) { var_1_135 = var_1_136; } else { var_1_135 = 63.8; } if (var_1_125) { var_1_137 = var_1_86; } else { var_1_137 = var_1_73; } if (var_1_36) { var_1_138 = var_1_120; } else { var_1_138 = var_1_132; } if (var_1_125) { var_1_139 = var_1_109; } if (var_1_111) { var_1_140 = var_1_54; } var_1_141 = 50.04; if ((~ -128) > var_1_101) { if (var_1_137 >= (~ (var_1_73 | var_1_62))) { if (var_1_65 > var_1_79) { var_1_142 = (((((((var_1_105) < 0 ) ? -(var_1_105) : (var_1_105))) < 0 ) ? -((((var_1_105) < 0 ) ? -(var_1_105) : (var_1_105))) : ((((var_1_105) < 0 ) ? -(var_1_105) : (var_1_105))))); } else { var_1_142 = var_1_103; } } } else { var_1_142 = var_1_80; } if ((- last_1_var_1_9) < (last_1_var_1_9 + -500)) { var_1_23 = var_1_20; } var_1_17 = (((((var_1_18) < (var_1_19)) ? (var_1_18) : (var_1_19))) - (var_1_20 + (var_1_21 - var_1_22))); if (var_1_4) { var_1_24 = (! var_1_25); } else { var_1_24 = (var_1_6 && ((var_1_10 >= var_1_17) && var_1_25)); } var_1_31 = var_1_30; if (var_1_23 < var_1_23) { if (var_1_24 && var_1_24) { if (var_1_24) { if (var_1_24 && (var_1_24 || var_1_24)) { var_1_1 = -5; } } } else { var_1_1 = var_1_8; } } else { var_1_1 = var_1_8; } signed char stepLocal_0 = var_1_1; if (stepLocal_0 < (-1 - var_1_10)) { if (var_1_24) { var_1_9 = (var_1_10 + ((((var_1_23) < 0 ) ? -(var_1_23) : (var_1_23)))); } else { var_1_9 = ((var_1_12 - var_1_10) - ((var_1_13 - var_1_23) - ((((var_1_23) < (var_1_23)) ? (var_1_23) : (var_1_23))))); } } else { var_1_9 = var_1_13; } if (var_1_9 < (var_1_21 + var_1_23)) { var_1_27 = ((var_1_28 + var_1_29) + var_1_30); } else { var_1_27 = var_1_28; } } void updateVariables() { var_1_4 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_4 >= 0); assume_abort_if_not(var_1_4 <= 1); var_1_6 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_6 >= 0); assume_abort_if_not(var_1_6 <= 1); var_1_8 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_8 >= -127); assume_abort_if_not(var_1_8 <= 126); var_1_10 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_10 >= 0); assume_abort_if_not(var_1_10 <= 127); var_1_12 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_12 >= 49150); assume_abort_if_not(var_1_12 <= 65534); var_1_13 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_13 >= 24575); assume_abort_if_not(var_1_13 <= 32767); var_1_18 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_18 >= -1); assume_abort_if_not(var_1_18 <= 126); var_1_19 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_19 >= -1); assume_abort_if_not(var_1_19 <= 126); var_1_20 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_20 >= 0); assume_abort_if_not(var_1_20 <= 63); var_1_21 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_21 >= 31); assume_abort_if_not(var_1_21 <= 63); var_1_22 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_22 >= 0); assume_abort_if_not(var_1_22 <= 31); var_1_25 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_25 >= 0); assume_abort_if_not(var_1_25 <= 0); var_1_28 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_28 >= -230584.3009213691390e+13F && var_1_28 <= -1.0e-20F) || (var_1_28 <= 2305843.009213691390e+12F && var_1_28 >= 1.0e-20F )); var_1_29 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_29 >= -230584.3009213691390e+13F && var_1_29 <= -1.0e-20F) || (var_1_29 <= 2305843.009213691390e+12F && var_1_29 >= 1.0e-20F )); var_1_30 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_30 >= -461168.6018427382800e+13F && var_1_30 <= -1.0e-20F) || (var_1_30 <= 4611686.018427382800e+12F && var_1_30 >= 1.0e-20F )); var_1_33 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_33 >= 0); assume_abort_if_not(var_1_33 <= 4294967295); var_1_34 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_34 >= 0); assume_abort_if_not(var_1_34 <= 4294967295); var_1_35 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_35 >= -128); assume_abort_if_not(var_1_35 <= 127); assume_abort_if_not(var_1_35 != 0); var_1_36 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_36 >= 0); assume_abort_if_not(var_1_36 <= 1); var_1_37 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_37 >= 0); assume_abort_if_not(var_1_37 <= 65534); var_1_38 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_38 >= 0); assume_abort_if_not(var_1_38 <= 65534); var_1_39 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_39 >= 0); assume_abort_if_not(var_1_39 <= 65534); var_1_41 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_41 >= -127); assume_abort_if_not(var_1_41 <= 127); var_1_42 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_42 >= -128); assume_abort_if_not(var_1_42 <= 127); assume_abort_if_not(var_1_42 != 0); var_1_43 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_43 >= 1); assume_abort_if_not(var_1_43 <= 1); var_1_44 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_44 >= 1); assume_abort_if_not(var_1_44 <= 1); var_1_46 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_46 >= -2147483648); assume_abort_if_not(var_1_46 <= 2147483647); var_1_47 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_47 >= 0); assume_abort_if_not(var_1_47 <= 254); var_1_49 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_49 >= 0); assume_abort_if_not(var_1_49 <= 65535); assume_abort_if_not(var_1_49 != 0); var_1_51 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_51 >= 2147483647); assume_abort_if_not(var_1_51 <= 4294967295); var_1_52 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_52 >= 0); assume_abort_if_not(var_1_52 <= 2147483647); var_1_54 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_54 >= -922337.2036854765600e+13F && var_1_54 <= -1.0e-20F) || (var_1_54 <= 9223372.036854765600e+12F && var_1_54 >= 1.0e-20F )); var_1_55 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_55 >= -922337.2036854765600e+13F && var_1_55 <= -1.0e-20F) || (var_1_55 <= 9223372.036854765600e+12F && var_1_55 >= 1.0e-20F )); var_1_58 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_58 >= 0); assume_abort_if_not(var_1_58 <= 4294967295); assume_abort_if_not(var_1_58 != 0); var_1_59 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_59 >= -461168.6018427382800e+13F && var_1_59 <= -1.0e-20F) || (var_1_59 <= 4611686.018427382800e+12F && var_1_59 >= 1.0e-20F )); var_1_60 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_60 >= -461168.6018427382800e+13F && var_1_60 <= -1.0e-20F) || (var_1_60 <= 4611686.018427382800e+12F && var_1_60 >= 1.0e-20F )); var_1_62 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_62 >= 0); assume_abort_if_not(var_1_62 <= 255); var_1_66 = __VERIFIER_nondet_short(); assume_abort_if_not(var_1_66 >= -32768); assume_abort_if_not(var_1_66 <= 32767); var_1_68 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_68 >= 16383); assume_abort_if_not(var_1_68 <= 32767); var_1_69 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_69 >= 16384); assume_abort_if_not(var_1_69 <= 32767); var_1_70 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_70 >= 32767); assume_abort_if_not(var_1_70 <= 65534); var_1_76 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_76 >= 0.0F && var_1_76 <= -1.0e-20F) || (var_1_76 <= 9223372.036854776000e+12F && var_1_76 >= 1.0e-20F )); var_1_79 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_79 >= -1); assume_abort_if_not(var_1_79 <= 126); var_1_80 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_80 >= 0); assume_abort_if_not(var_1_80 <= 126); var_1_81 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_81 >= -127); assume_abort_if_not(var_1_81 <= 126); var_1_84 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_84 >= 0); assume_abort_if_not(var_1_84 <= 65534); var_1_85 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_85 >= 0.0F && var_1_85 <= -1.0e-20F) || (var_1_85 <= 9223372.036854776000e+12F && var_1_85 >= 1.0e-20F )); var_1_90 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_90 >= 0.0F && var_1_90 <= -1.0e-20F) || (var_1_90 <= 9223372.036854765600e+12F && var_1_90 >= 1.0e-20F )); var_1_91 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_91 >= 0.0F && var_1_91 <= -1.0e-20F) || (var_1_91 <= 9223372.036854765600e+12F && var_1_91 >= 1.0e-20F )); var_1_92 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_92 >= 0.0F && var_1_92 <= -1.0e-20F) || (var_1_92 <= 9223372.036854765600e+12F && var_1_92 >= 1.0e-20F )); var_1_98 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_98 >= 4611686.018427382800e+12F && var_1_98 <= -1.0e-20F) || (var_1_98 <= 9223372.036854765600e+12F && var_1_98 >= 1.0e-20F )); var_1_99 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_99 >= 0.0F && var_1_99 <= -1.0e-20F) || (var_1_99 <= 4611686.018427382800e+12F && var_1_99 >= 1.0e-20F )); var_1_100 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_100 >= -922337.2036854765600e+13F && var_1_100 <= -1.0e-20F) || (var_1_100 <= 9223372.036854765600e+12F && var_1_100 >= 1.0e-20F )); var_1_103 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_103 >= 127); assume_abort_if_not(var_1_103 <= 254); var_1_104 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_104 >= 63); assume_abort_if_not(var_1_104 <= 127); var_1_105 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_105 >= 63); assume_abort_if_not(var_1_105 <= 127); var_1_106 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_106 >= 0); assume_abort_if_not(var_1_106 <= 63); var_1_109 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_109 >= 0); assume_abort_if_not(var_1_109 <= 0); var_1_114 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_114 >= 0); assume_abort_if_not(var_1_114 <= 2147483647); var_1_115 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_115 >= 1073741823); assume_abort_if_not(var_1_115 <= 2147483647); var_1_119 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_119 >= -2147483647); assume_abort_if_not(var_1_119 <= 2147483647); var_1_125 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_125 >= 0); assume_abort_if_not(var_1_125 <= 1); var_1_127 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_127 >= 0); assume_abort_if_not(var_1_127 <= 4294967295); var_1_129 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_129 >= -922337.2036854776000e+13F && var_1_129 <= -1.0e-20F) || (var_1_129 <= 9223372.036854776000e+12F && var_1_129 >= 1.0e-20F )); var_1_133 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_133 >= 0); assume_abort_if_not(var_1_133 <= 65534); var_1_136 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_136 >= -922337.2036854765600e+13F && var_1_136 <= -1.0e-20F) || (var_1_136 <= 9223372.036854765600e+12F && var_1_136 >= 1.0e-20F )); } void updateLastVariables() { last_1_var_1_9 = var_1_9; } int property() { return (((((((var_1_23 < var_1_23) ? ((var_1_24 && var_1_24) ? (var_1_24 ? ((var_1_24 && (var_1_24 || var_1_24)) ? (var_1_1 == ((signed char) -5)) : 1) : 1) : (var_1_1 == ((signed char) var_1_8))) : (var_1_1 == ((signed char) var_1_8))) && ((var_1_1 < (-1 - var_1_10)) ? (var_1_24 ? (var_1_9 == ((unsigned short int) (var_1_10 + ((((var_1_23) < 0 ) ? -(var_1_23) : (var_1_23)))))) : (var_1_9 == ((unsigned short int) ((var_1_12 - var_1_10) - ((var_1_13 - var_1_23) - ((((var_1_23) < (var_1_23)) ? (var_1_23) : (var_1_23)))))))) : (var_1_9 == ((unsigned short int) var_1_13)))) && (var_1_17 == ((signed char) (((((var_1_18) < (var_1_19)) ? (var_1_18) : (var_1_19))) - (var_1_20 + (var_1_21 - var_1_22)))))) && (((- last_1_var_1_9) < (last_1_var_1_9 + -500)) ? (var_1_23 == ((unsigned char) var_1_20)) : 1)) && (var_1_4 ? (var_1_24 == ((unsigned char) (! var_1_25))) : (var_1_24 == ((unsigned char) (var_1_6 && ((var_1_10 >= var_1_17) && var_1_25)))))) && ((var_1_9 < (var_1_21 + var_1_23)) ? (var_1_27 == ((double) ((var_1_28 + var_1_29) + var_1_30))) : (var_1_27 == ((double) var_1_28)))) && (var_1_31 == ((float) var_1_30)) ; } int main(void) { isInitial = 1; initially(); while (1) { updateLastVariables(); updateVariables(); step(); __VERIFIER_assert(property()); isInitial = 0; } return 0; }