// 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_Batch45Amount500.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; unsigned long int var_1_1 = 0; signed long int var_1_5 = 32; unsigned long int var_1_8 = 3974482504; unsigned long int var_1_9 = 4191564779; unsigned long int var_1_10 = 1942660812; unsigned long int var_1_11 = 1000000000; signed char var_1_12 = -128; signed char var_1_13 = 100; signed short int var_1_14 = -1; unsigned long int var_1_15 = 0; float var_1_19 = 32.975; unsigned char var_1_21 = 8; signed short int var_1_23 = -2; double var_1_24 = 255.8; double var_1_25 = 32.5; double var_1_26 = 7.6; double var_1_27 = 0.0; double var_1_28 = 0.5; unsigned char var_1_29 = 0; unsigned char var_1_30 = 0; unsigned char var_1_31 = 0; unsigned char var_1_32 = 8; unsigned char var_1_33 = 128; unsigned char var_1_34 = 32; unsigned char var_1_35 = 200; unsigned char var_1_36 = 8; unsigned char var_1_37 = 16; unsigned char var_1_38 = 50; signed char var_1_39 = 1; double var_1_40 = 99.5; unsigned char var_1_41 = 8; signed char var_1_42 = -8; unsigned long int var_1_43 = 50; signed short int var_1_44 = 256; unsigned long int var_1_45 = 100; unsigned char var_1_46 = 0; unsigned long int var_1_47 = 1000; unsigned long int var_1_50 = 2026986786; signed short int var_1_51 = -1; unsigned long int var_1_52 = 64; unsigned long int var_1_54 = 1; signed char var_1_56 = 4; unsigned long int var_1_57 = 32; unsigned long int var_1_59 = 4012610487; unsigned long int var_1_60 = 2071316436; unsigned short int var_1_61 = 128; unsigned short int var_1_62 = 57978; unsigned short int var_1_63 = 16; float var_1_64 = 500.5; signed long int var_1_65 = 4; double var_1_66 = 256.6; signed long int var_1_67 = 50; signed short int var_1_68 = -1; signed short int var_1_70 = 2; signed long int var_1_72 = 25; unsigned short int var_1_74 = 63279; unsigned char var_1_75 = 0; unsigned char var_1_76 = 0; unsigned char var_1_77 = 25; unsigned char var_1_78 = 0; unsigned long int var_1_79 = 128; float var_1_81 = 49.75; float var_1_82 = 32.6; unsigned char var_1_83 = 1; double var_1_84 = 128.3; double var_1_85 = 15.5; double var_1_86 = 15.5; double var_1_87 = 25.375; double var_1_88 = 127.5; double var_1_89 = 999999999.6; unsigned long int var_1_90 = 50; float var_1_91 = 256.4; float var_1_92 = 10.5; unsigned short int var_1_93 = 2; unsigned short int var_1_97 = 33685; unsigned short int var_1_98 = 18495; unsigned short int var_1_99 = 18293; unsigned long int var_1_100 = 50; double var_1_101 = -0.4; float var_1_102 = 2.25; signed char var_1_103 = 0; double var_1_104 = 1000000000000.5; signed short int var_1_105 = -256; unsigned short int var_1_106 = 1000; unsigned short int var_1_107 = 10; unsigned short int var_1_108 = 5; unsigned char var_1_109 = 16; signed short int var_1_110 = 64; double var_1_111 = 15.8; unsigned char var_1_112 = 0; signed char var_1_113 = 5; signed short int var_1_114 = 128; unsigned char var_1_115 = 1; unsigned char var_1_116 = 0; double var_1_117 = -0.5; signed short int var_1_118 = 8; signed long int var_1_119 = 5; unsigned char var_1_120 = 0; signed char var_1_121 = 4; unsigned char var_1_122 = 1; unsigned char var_1_123 = 1; signed short int var_1_124 = 256; unsigned long int last_1_var_1_15 = 0; unsigned char last_1_var_1_41 = 8; unsigned long int last_1_var_1_43 = 50; unsigned char last_1_var_1_46 = 0; signed short int last_1_var_1_51 = -1; unsigned long int last_1_var_1_52 = 64; unsigned long int last_1_var_1_54 = 1; unsigned long int last_1_var_1_57 = 32; unsigned short int last_1_var_1_63 = 16; signed long int last_1_var_1_67 = 50; signed short int last_1_var_1_68 = -1; signed long int last_1_var_1_72 = 25; unsigned char last_1_var_1_76 = 0; unsigned long int last_1_var_1_79 = 128; unsigned short int last_1_var_1_93 = 2; unsigned short int last_1_var_1_107 = 10; unsigned short int last_1_var_1_108 = 5; unsigned char last_1_var_1_109 = 16; signed short int last_1_var_1_118 = 8; signed char last_1_var_1_121 = 4; void initially(void) { } void step(void) { if ((last_1_var_1_63 >> var_1_77) > last_1_var_1_67) { var_1_76 = ((! var_1_31) || var_1_30); } else { if (last_1_var_1_118 >= last_1_var_1_54) { var_1_76 = var_1_31; } else { var_1_76 = (var_1_30 || ((! var_1_31) || var_1_78)); } } signed long int stepLocal_10 = last_1_var_1_121; if (stepLocal_10 < (last_1_var_1_52 * var_1_35)) { var_1_46 = 0; } else { var_1_46 = var_1_30; } signed long int stepLocal_16 = last_1_var_1_107; if (last_1_var_1_52 < stepLocal_16) { var_1_63 = (((((((((var_1_35 + var_1_36)) < (last_1_var_1_72)) ? ((var_1_35 + var_1_36)) : (last_1_var_1_72)))) < ((last_1_var_1_109 + var_1_5))) ? ((((((var_1_35 + var_1_36)) < (last_1_var_1_72)) ? ((var_1_35 + var_1_36)) : (last_1_var_1_72)))) : ((last_1_var_1_109 + var_1_5)))); } if (last_1_var_1_46) { var_1_107 = last_1_var_1_43; } else { var_1_107 = var_1_98; } unsigned long int stepLocal_22 = last_1_var_1_15; signed long int stepLocal_21 = var_1_37 / ((((var_1_13) < (var_1_35)) ? (var_1_13) : (var_1_35))); if (last_1_var_1_107 < stepLocal_21) { var_1_68 = var_1_34; } else { if (! last_1_var_1_76) { if (last_1_var_1_79 > stepLocal_22) { var_1_68 = var_1_5; } else { var_1_68 = ((((last_1_var_1_68) > (last_1_var_1_51)) ? (last_1_var_1_68) : (last_1_var_1_51))); } } } var_1_124 = var_1_68; unsigned long int stepLocal_14 = (var_1_38 ^ last_1_var_1_108) | var_1_8; if ((last_1_var_1_54 / var_1_33) >= stepLocal_14) { var_1_54 = (last_1_var_1_108 + var_1_11); } var_1_23 = var_1_5; var_1_24 = (((((var_1_25) > (var_1_26)) ? (var_1_25) : (var_1_26))) - (var_1_27 - var_1_28)); var_1_40 = ((((var_1_28) > ((((((var_1_25) > (var_1_27)) ? (var_1_25) : (var_1_27))) - var_1_26))) ? (var_1_28) : ((((((var_1_25) > (var_1_27)) ? (var_1_25) : (var_1_27))) - var_1_26)))); var_1_42 = (var_1_13 - ((((var_1_37) > (var_1_5)) ? (var_1_37) : (var_1_5)))); var_1_56 = (((((var_1_36 - var_1_37)) > (((((var_1_13) < 0 ) ? -(var_1_13) : (var_1_13))))) ? ((var_1_36 - var_1_37)) : (((((var_1_13) < 0 ) ? -(var_1_13) : (var_1_13)))))); signed long int stepLocal_15 = var_1_33 - var_1_38; if (var_1_37 <= stepLocal_15) { var_1_61 = (var_1_62 - 1); } var_1_64 = ((((var_1_26) > ((var_1_28 - ((((var_1_27) < 0 ) ? -(var_1_27) : (var_1_27)))))) ? (var_1_26) : ((var_1_28 - ((((var_1_27) < 0 ) ? -(var_1_27) : (var_1_27))))))); if (var_1_30) { var_1_66 = var_1_26; } var_1_75 = ((((var_1_38) < (var_1_5)) ? (var_1_38) : (var_1_5))); var_1_83 = var_1_78; if (var_1_30) { var_1_86 = (var_1_28 + ((((63.5) > (100.5)) ? (63.5) : (100.5)))); } else { var_1_86 = (var_1_28 + var_1_87); } if (var_1_85 > var_1_28) { var_1_91 = (((((var_1_25) < (var_1_28)) ? (var_1_25) : (var_1_28))) - (var_1_27 - (4.0994868604932741E18f - var_1_92))); } else { var_1_91 = ((((var_1_28) < (((((var_1_87) > (-0.75f)) ? (var_1_87) : (-0.75f))))) ? (var_1_28) : (((((var_1_87) > (-0.75f)) ? (var_1_87) : (-0.75f)))))); } unsigned long int stepLocal_32 = (~ 50u) / var_1_60; if ((var_1_50 * var_1_37) >= stepLocal_32) { var_1_103 = ((((((((var_1_5) < 0 ) ? -(var_1_5) : (var_1_5)))) > (var_1_38)) ? (((((var_1_5) < 0 ) ? -(var_1_5) : (var_1_5)))) : (var_1_38))); } if (var_1_30) { var_1_106 = var_1_34; } else { var_1_106 = 10; } var_1_110 = var_1_38; var_1_111 = var_1_27; var_1_112 = var_1_30; var_1_113 = var_1_77; if (var_1_112) { var_1_114 = var_1_35; } var_1_115 = var_1_116; if (var_1_83) { var_1_120 = (! (! var_1_31)); } else { var_1_120 = (var_1_31 && (! var_1_116)); } var_1_121 = var_1_77; var_1_122 = var_1_123; if (var_1_76) { var_1_118 = var_1_33; } else { var_1_118 = var_1_124; } signed long int stepLocal_20 = - var_1_13; signed long int stepLocal_19 = - (var_1_13 / var_1_35); if (var_1_107 < stepLocal_19) { if (last_1_var_1_67 < stepLocal_20) { var_1_67 = var_1_38; } else { var_1_67 = ((((((((var_1_35) > (var_1_34)) ? (var_1_35) : (var_1_34)))) < (-128)) ? (((((var_1_35) > (var_1_34)) ? (var_1_35) : (var_1_34)))) : (-128))); } } else { var_1_67 = (var_1_54 + var_1_61); } unsigned char stepLocal_34 = var_1_30; unsigned short int stepLocal_33 = var_1_106; if (stepLocal_33 <= var_1_68) { if (var_1_78 && stepLocal_34) { var_1_104 = (var_1_27 - var_1_82); } else { var_1_104 = ((var_1_28 + var_1_89) - var_1_92); } } else { var_1_104 = var_1_85; } if (! var_1_120) { if (var_1_120) { var_1_14 = ((32 + var_1_113) + (((((((var_1_5) < (-50)) ? (var_1_5) : (-50))) < 0 ) ? -((((var_1_5) < (-50)) ? (var_1_5) : (-50))) : ((((var_1_5) < (-50)) ? (var_1_5) : (-50)))))); } else { var_1_14 = var_1_13; } } unsigned char stepLocal_2 = var_1_83; if (var_1_120 || stepLocal_2) { if (! var_1_120) { var_1_21 = (var_1_5 + ((((var_1_13) < 0 ) ? -(var_1_13) : (var_1_13)))); } } unsigned short int stepLocal_4 = var_1_106; if (var_1_19 < (var_1_28 / var_1_27)) { if (var_1_5 > stepLocal_4) { var_1_32 = ((((var_1_5) < ((var_1_33 - var_1_13))) ? (var_1_5) : ((var_1_33 - var_1_13)))); } else { var_1_32 = (((((var_1_5) < (var_1_13)) ? (var_1_5) : (var_1_13))) + var_1_34); } } else { var_1_32 = ((var_1_35 - ((((var_1_5) < (var_1_36)) ? (var_1_5) : (var_1_36)))) - (((((var_1_37 + var_1_38)) < (var_1_13)) ? ((var_1_37 + var_1_38)) : (var_1_13)))); } signed long int stepLocal_6 = var_1_33 - var_1_38; unsigned char stepLocal_5 = var_1_34; if (var_1_8 != stepLocal_5) { if (var_1_120) { var_1_39 = (var_1_13 - var_1_37); } else { if (var_1_35 < stepLocal_6) { var_1_39 = (var_1_38 + var_1_36); } else { var_1_39 = var_1_38; } } } if ((-16 * var_1_121) >= ((var_1_37 % var_1_35) + last_1_var_1_41)) { if (var_1_83) { var_1_41 = var_1_5; } else { var_1_41 = ((((((((var_1_37) > (((((var_1_34) < (var_1_13)) ? (var_1_34) : (var_1_13))))) ? (var_1_37) : (((((var_1_34) < (var_1_13)) ? (var_1_34) : (var_1_13))))))) < (var_1_33)) ? (((((var_1_37) > (((((var_1_34) < (var_1_13)) ? (var_1_34) : (var_1_13))))) ? (var_1_37) : (((((var_1_34) < (var_1_13)) ? (var_1_34) : (var_1_13))))))) : (var_1_33))); } } else { var_1_41 = ((((var_1_13) > (25)) ? (var_1_13) : (25))); } var_1_44 = ((((var_1_13) > (var_1_39)) ? (var_1_13) : (var_1_39))); signed long int stepLocal_27 = var_1_37 / var_1_35; signed char stepLocal_26 = var_1_103; if (var_1_42 < stepLocal_26) { if (var_1_121 >= stepLocal_27) { var_1_84 = var_1_27; } else { var_1_84 = ((((var_1_85) > (((((var_1_28) > (var_1_27)) ? (var_1_28) : (var_1_27))))) ? (var_1_85) : (((((var_1_28) > (var_1_27)) ? (var_1_28) : (var_1_27)))))); } } else { var_1_84 = ((((var_1_25) < 0 ) ? -(var_1_25) : (var_1_25))); } if (var_1_31) { var_1_100 = (var_1_21 + var_1_103); } else { var_1_100 = (((((2u + var_1_99)) < ((var_1_103 + var_1_37))) ? ((2u + var_1_99)) : ((var_1_103 + var_1_37)))); } if (var_1_115) { if (var_1_112) { var_1_102 = var_1_26; } } if (var_1_120) { var_1_105 = var_1_106; } else { var_1_105 = var_1_13; } if (var_1_112) { var_1_109 = var_1_35; } else { var_1_109 = var_1_34; } if (var_1_122) { var_1_117 = var_1_89; } else { var_1_117 = 10.125; } var_1_119 = var_1_21; unsigned long int stepLocal_7 = var_1_10; if (var_1_109 <= stepLocal_7) { if (var_1_46) { var_1_43 = (((((((((((var_1_5) > (var_1_109)) ? (var_1_5) : (var_1_109))) < 0 ) ? -((((var_1_5) > (var_1_109)) ? (var_1_5) : (var_1_109))) : ((((var_1_5) > (var_1_109)) ? (var_1_5) : (var_1_109)))))) < (((((var_1_34) > (var_1_109)) ? (var_1_34) : (var_1_109))))) ? ((((((((var_1_5) > (var_1_109)) ? (var_1_5) : (var_1_109))) < 0 ) ? -((((var_1_5) > (var_1_109)) ? (var_1_5) : (var_1_109))) : ((((var_1_5) > (var_1_109)) ? (var_1_5) : (var_1_109)))))) : (((((var_1_34) > (var_1_109)) ? (var_1_34) : (var_1_109)))))); } else { var_1_43 = ((((((var_1_10) < 0 ) ? -(var_1_10) : (var_1_10))) - 128u) + 16u); } } else { var_1_43 = var_1_37; } signed short int stepLocal_24 = var_1_23; unsigned char stepLocal_23 = var_1_35; if (stepLocal_24 > var_1_105) { var_1_79 = ((((((var_1_62 + var_1_106)) > (var_1_23)) ? ((var_1_62 + var_1_106)) : (var_1_23))) + var_1_37); } else { if (stepLocal_23 > var_1_74) { if (var_1_46) { var_1_79 = ((((((var_1_59 - var_1_74) - var_1_63)) < ((var_1_8 - var_1_33))) ? (((var_1_59 - var_1_74) - var_1_63)) : ((var_1_8 - var_1_33)))); } else { var_1_79 = ((((((var_1_59 - var_1_38) - 4u)) < (var_1_60)) ? (((var_1_59 - var_1_38) - 4u)) : (var_1_60))); } } } signed long int stepLocal_31 = ~ var_1_118; signed long int stepLocal_30 = 64 + (- var_1_21); if (stepLocal_31 >= (last_1_var_1_93 + var_1_103)) { var_1_93 = (var_1_62 - var_1_35); } else { if (var_1_120) { if (stepLocal_30 > (((((var_1_8 - var_1_21)) > (var_1_38)) ? ((var_1_8 - var_1_21)) : (var_1_38)))) { var_1_93 = (((((var_1_62) < (var_1_97)) ? (var_1_62) : (var_1_97))) - var_1_35); } else { var_1_93 = (((((((((var_1_97) < (var_1_62)) ? (var_1_97) : (var_1_62)))) < (45680)) ? (((((var_1_97) < (var_1_62)) ? (var_1_97) : (var_1_62)))) : (45680))) - ((((var_1_13) < (var_1_38)) ? (var_1_13) : (var_1_38)))); } } else { var_1_93 = ((((((var_1_98 + var_1_99) - var_1_34)) > (((((var_1_77 + var_1_33) < 0 ) ? -(var_1_77 + var_1_33) : (var_1_77 + var_1_33))))) ? (((var_1_98 + var_1_99) - var_1_34)) : (((((var_1_77 + var_1_33) < 0 ) ? -(var_1_77 + var_1_33) : (var_1_77 + var_1_33)))))); } } signed long int stepLocal_9 = var_1_35 + var_1_37; signed long int stepLocal_8 = var_1_5; if ((var_1_61 * (var_1_33 | -128)) >= stepLocal_8) { if (stepLocal_9 <= ((((var_1_93) > (var_1_36)) ? (var_1_93) : (var_1_36)))) { var_1_45 = ((((((((var_1_33) < 0 ) ? -(var_1_33) : (var_1_33)))) > (var_1_34)) ? (((((var_1_33) < 0 ) ? -(var_1_33) : (var_1_33)))) : (var_1_34))); } } if (var_1_64 != var_1_86) { if (var_1_8 >= var_1_11) { var_1_70 = (((((var_1_14 + var_1_68) + var_1_13) < 0 ) ? -((var_1_14 + var_1_68) + var_1_13) : ((var_1_14 + var_1_68) + var_1_13))); } else { var_1_70 = (var_1_34 + var_1_54); } } else { var_1_70 = ((var_1_13 + var_1_38) - var_1_124); } signed short int stepLocal_25 = var_1_70; if (stepLocal_25 >= var_1_9) { var_1_81 = (((((((((var_1_26) < (var_1_82)) ? (var_1_26) : (var_1_82))) - var_1_27)) < (var_1_28)) ? ((((((var_1_26) < (var_1_82)) ? (var_1_26) : (var_1_82))) - var_1_27)) : (var_1_28))); } else { var_1_81 = var_1_27; } signed long int stepLocal_18 = 2; unsigned char stepLocal_17 = var_1_41; if (var_1_36 < stepLocal_18) { if (stepLocal_17 <= (var_1_32 >> var_1_10)) { var_1_65 = (((var_1_35 + var_1_118) + var_1_121) + (var_1_107 + var_1_70)); } else { var_1_65 = (var_1_37 - var_1_38); } } else { var_1_65 = ((((var_1_13) > (var_1_68)) ? (var_1_13) : (var_1_68))); } if (var_1_81 < var_1_86) { var_1_101 = ((var_1_92 - var_1_89) + ((((var_1_87) < (var_1_28)) ? (var_1_87) : (var_1_28)))); } unsigned long int stepLocal_1 = 50u; unsigned char stepLocal_0 = var_1_43 >= var_1_32; if (stepLocal_0 || var_1_112) { if (((var_1_43 * var_1_32) >> var_1_5) >= stepLocal_1) { var_1_1 = (var_1_5 + (var_1_21 + var_1_41)); } else { var_1_1 = (var_1_5 + ((((var_1_41) < (var_1_21)) ? (var_1_41) : (var_1_21)))); } } else { if (var_1_112) { var_1_1 = (((((var_1_8) < (var_1_9)) ? (var_1_8) : (var_1_9))) - (var_1_10 - (var_1_11 - var_1_5))); } } if (var_1_1 == var_1_5) { var_1_12 = (var_1_5 - (var_1_13 - 8)); } if (var_1_28 >= 1.00000000000002E13) { var_1_51 = (((((-128 + var_1_45)) < (-100)) ? ((-128 + var_1_45)) : (-100))); } else { var_1_51 = ((((var_1_34) > ((((((var_1_35) < (var_1_36)) ? (var_1_35) : (var_1_36))) - var_1_5))) ? (var_1_34) : ((((((var_1_35) < (var_1_36)) ? (var_1_35) : (var_1_36))) - var_1_5)))); } if (var_1_75 <= last_1_var_1_57) { var_1_57 = ((((var_1_9) < 0 ) ? -(var_1_9) : (var_1_9))); } else { var_1_57 = (((var_1_59 - var_1_13) - var_1_51) - ((var_1_60 - var_1_37) - var_1_34)); } if (((((var_1_104) < (var_1_81)) ? (var_1_104) : (var_1_81))) > (var_1_64 / ((((var_1_19) < 0 ) ? -(var_1_19) : (var_1_19))))) { var_1_15 = ((var_1_10 - var_1_41) + (5u + var_1_11)); } else { var_1_15 = (var_1_41 + (var_1_61 + var_1_11)); } signed long int stepLocal_3 = var_1_5 + var_1_21; if ((var_1_13 | (var_1_57 + var_1_107)) <= stepLocal_3) { var_1_29 = (! (! var_1_30)); } else { var_1_29 = ((var_1_66 > (var_1_26 - var_1_28)) || var_1_31); } if (var_1_29) { var_1_90 = ((((var_1_37) < (var_1_1)) ? (var_1_37) : (var_1_1))); } if ((128 >= (~ last_1_var_1_72)) || (last_1_var_1_72 < var_1_93)) { if (var_1_75 > (var_1_63 * var_1_90)) { var_1_72 = ((((var_1_34) < ((var_1_79 - var_1_62))) ? (var_1_34) : ((var_1_79 - var_1_62)))); } else { if (((var_1_74 - var_1_38) - var_1_5) <= ((-10 / var_1_13) + var_1_21)) { var_1_72 = ((((((((var_1_68) > (((((var_1_74) < (var_1_12)) ? (var_1_74) : (var_1_12))))) ? (var_1_68) : (((((var_1_74) < (var_1_12)) ? (var_1_74) : (var_1_12))))))) > ((var_1_121 + var_1_38))) ? (((((var_1_68) > (((((var_1_74) < (var_1_12)) ? (var_1_74) : (var_1_12))))) ? (var_1_68) : (((((var_1_74) < (var_1_12)) ? (var_1_74) : (var_1_12))))))) : ((var_1_121 + var_1_38)))); } else { var_1_72 = (var_1_79 - var_1_12); } } } if (var_1_112) { var_1_108 = var_1_72; } else { var_1_108 = var_1_36; } signed long int stepLocal_29 = var_1_119 / ((((var_1_33) < (128)) ? (var_1_33) : (128))); signed long int stepLocal_28 = (((var_1_23) < 0 ) ? -(var_1_23) : (var_1_23)); if (stepLocal_28 > ((((((((50) > (var_1_108)) ? (50) : (var_1_108)))) > (-50)) ? (((((50) > (var_1_108)) ? (50) : (var_1_108)))) : (-50)))) { if (var_1_103 <= stepLocal_29) { if (var_1_122) { if ((((((var_1_28) > (var_1_26)) ? (var_1_28) : (var_1_26))) - var_1_25) >= (var_1_117 / var_1_19)) { var_1_88 = ((((var_1_26) < (8.5)) ? (var_1_26) : (8.5))); } else { var_1_88 = ((var_1_28 - var_1_89) + var_1_87); } } } else { var_1_88 = (var_1_28 - var_1_26); } } unsigned char stepLocal_13 = var_1_38 <= 50; unsigned long int stepLocal_12 = (((var_1_54) < (var_1_67)) ? (var_1_54) : (var_1_67)); if (var_1_76) { if (stepLocal_13 && (var_1_51 > last_1_var_1_52)) { if (stepLocal_12 >= var_1_41) { var_1_52 = (var_1_35 + ((((var_1_13) < (var_1_108)) ? (var_1_13) : (var_1_108)))); } } else { var_1_52 = (var_1_9 - var_1_37); } } unsigned char stepLocal_11 = var_1_109; if (! (var_1_25 <= ((((var_1_40) < (var_1_19)) ? (var_1_40) : (var_1_19))))) { if (var_1_88 >= (var_1_27 + var_1_102)) { if (stepLocal_11 < var_1_67) { var_1_47 = ((((var_1_9 - (var_1_10 - var_1_35)) < 0 ) ? -(var_1_9 - (var_1_10 - var_1_35)) : (var_1_9 - (var_1_10 - var_1_35)))); } else { var_1_47 = (((((var_1_35) < (var_1_10)) ? (var_1_35) : (var_1_10))) + (var_1_50 - var_1_63)); } } else { var_1_47 = (4063477532u - var_1_11); } } else { var_1_47 = (var_1_63 + (var_1_10 - var_1_36)); } } void updateVariables() { var_1_5 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_5 >= 0); assume_abort_if_not(var_1_5 <= 33); var_1_8 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_8 >= 2147483647); assume_abort_if_not(var_1_8 <= 4294967294); var_1_9 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_9 >= 2147483647); assume_abort_if_not(var_1_9 <= 4294967294); var_1_10 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_10 >= 1073741823); assume_abort_if_not(var_1_10 <= 2147483647); var_1_11 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_11 >= 536870911); assume_abort_if_not(var_1_11 <= 1073741823); var_1_13 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_13 >= 63); assume_abort_if_not(var_1_13 <= 126); var_1_19 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_19 >= -922337.2036854776000e+13F && var_1_19 <= -1.0e-20F) || (var_1_19 <= 9223372.036854776000e+12F && var_1_19 >= 1.0e-20F )); assume_abort_if_not(var_1_19 != 0.0F); var_1_25 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_25 >= 0.0F && var_1_25 <= -1.0e-20F) || (var_1_25 <= 9223372.036854765600e+12F && var_1_25 >= 1.0e-20F )); var_1_26 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_26 >= 0.0F && var_1_26 <= -1.0e-20F) || (var_1_26 <= 9223372.036854765600e+12F && var_1_26 >= 1.0e-20F )); var_1_27 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_27 >= 4611686.018427382800e+12F && var_1_27 <= -1.0e-20F) || (var_1_27 <= 9223372.036854765600e+12F && var_1_27 >= 1.0e-20F )); var_1_28 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_28 >= 0.0F && var_1_28 <= -1.0e-20F) || (var_1_28 <= 4611686.018427382800e+12F && var_1_28 >= 1.0e-20F )); var_1_30 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_30 >= 0); assume_abort_if_not(var_1_30 <= 0); var_1_31 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_31 >= 1); assume_abort_if_not(var_1_31 <= 1); var_1_33 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_33 >= 127); assume_abort_if_not(var_1_33 <= 254); var_1_34 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_34 >= 0); assume_abort_if_not(var_1_34 <= 127); var_1_35 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_35 >= 190); assume_abort_if_not(var_1_35 <= 254); var_1_36 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_36 >= 0); assume_abort_if_not(var_1_36 <= 63); var_1_37 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_37 >= 0); assume_abort_if_not(var_1_37 <= 64); var_1_38 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_38 >= 0); assume_abort_if_not(var_1_38 <= 63); var_1_50 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_50 >= 1073741823); assume_abort_if_not(var_1_50 <= 2147483647); var_1_59 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_59 >= 3758096382); assume_abort_if_not(var_1_59 <= 4294967294); var_1_60 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_60 >= 1610612735); assume_abort_if_not(var_1_60 <= 2147483647); var_1_62 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_62 >= 32767); assume_abort_if_not(var_1_62 <= 65534); var_1_74 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_74 >= 49151); assume_abort_if_not(var_1_74 <= 65535); var_1_77 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_77 >= 0); assume_abort_if_not(var_1_77 <= 33); var_1_78 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_78 >= 0); assume_abort_if_not(var_1_78 <= 0); var_1_82 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_82 >= 0.0F && var_1_82 <= -1.0e-20F) || (var_1_82 <= 9223372.036854765600e+12F && var_1_82 >= 1.0e-20F )); var_1_85 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_85 >= -922337.2036854765600e+13F && var_1_85 <= -1.0e-20F) || (var_1_85 <= 9223372.036854765600e+12F && var_1_85 >= 1.0e-20F )); var_1_87 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_87 >= -461168.6018427382800e+13F && var_1_87 <= -1.0e-20F) || (var_1_87 <= 4611686.018427382800e+12F && var_1_87 >= 1.0e-20F )); var_1_89 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_89 >= 0.0F && var_1_89 <= -1.0e-20F) || (var_1_89 <= 4611686.018427382800e+12F && var_1_89 >= 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 <= 2305843.009213691390e+12F && var_1_92 >= 1.0e-20F )); var_1_97 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_97 >= 32767); assume_abort_if_not(var_1_97 <= 65534); var_1_98 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_98 >= 16383); assume_abort_if_not(var_1_98 <= 32767); var_1_99 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_99 >= 16384); assume_abort_if_not(var_1_99 <= 32767); var_1_116 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_116 >= 0); assume_abort_if_not(var_1_116 <= 0); var_1_123 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_123 >= 1); assume_abort_if_not(var_1_123 <= 1); } void updateLastVariables() { last_1_var_1_15 = var_1_15; last_1_var_1_41 = var_1_41; last_1_var_1_43 = var_1_43; last_1_var_1_46 = var_1_46; last_1_var_1_51 = var_1_51; last_1_var_1_52 = var_1_52; last_1_var_1_54 = var_1_54; last_1_var_1_57 = var_1_57; last_1_var_1_63 = var_1_63; last_1_var_1_67 = var_1_67; last_1_var_1_68 = var_1_68; last_1_var_1_72 = var_1_72; last_1_var_1_76 = var_1_76; last_1_var_1_79 = var_1_79; last_1_var_1_93 = var_1_93; last_1_var_1_107 = var_1_107; last_1_var_1_108 = var_1_108; last_1_var_1_109 = var_1_109; last_1_var_1_118 = var_1_118; last_1_var_1_121 = var_1_121; } int property() { return (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((var_1_43 >= var_1_32) || var_1_112) ? ((((var_1_43 * var_1_32) >> var_1_5) >= 50u) ? (var_1_1 == ((unsigned long int) (var_1_5 + (var_1_21 + var_1_41)))) : (var_1_1 == ((unsigned long int) (var_1_5 + ((((var_1_41) < (var_1_21)) ? (var_1_41) : (var_1_21))))))) : (var_1_112 ? (var_1_1 == ((unsigned long int) (((((var_1_8) < (var_1_9)) ? (var_1_8) : (var_1_9))) - (var_1_10 - (var_1_11 - var_1_5))))) : 1)) && ((var_1_1 == var_1_5) ? (var_1_12 == ((signed char) (var_1_5 - (var_1_13 - 8)))) : 1)) && ((! var_1_120) ? (var_1_120 ? (var_1_14 == ((signed short int) ((32 + var_1_113) + (((((((var_1_5) < (-50)) ? (var_1_5) : (-50))) < 0 ) ? -((((var_1_5) < (-50)) ? (var_1_5) : (-50))) : ((((var_1_5) < (-50)) ? (var_1_5) : (-50)))))))) : (var_1_14 == ((signed short int) var_1_13))) : 1)) && ((((((var_1_104) < (var_1_81)) ? (var_1_104) : (var_1_81))) > (var_1_64 / ((((var_1_19) < 0 ) ? -(var_1_19) : (var_1_19))))) ? (var_1_15 == ((unsigned long int) ((var_1_10 - var_1_41) + (5u + var_1_11)))) : (var_1_15 == ((unsigned long int) (var_1_41 + (var_1_61 + var_1_11)))))) && ((var_1_120 || var_1_83) ? ((! var_1_120) ? (var_1_21 == ((unsigned char) (var_1_5 + ((((var_1_13) < 0 ) ? -(var_1_13) : (var_1_13)))))) : 1) : 1)) && (var_1_23 == ((signed short int) var_1_5))) && (var_1_24 == ((double) (((((var_1_25) > (var_1_26)) ? (var_1_25) : (var_1_26))) - (var_1_27 - var_1_28))))) && (((var_1_13 | (var_1_57 + var_1_107)) <= (var_1_5 + var_1_21)) ? (var_1_29 == ((unsigned char) (! (! var_1_30)))) : (var_1_29 == ((unsigned char) ((var_1_66 > (var_1_26 - var_1_28)) || var_1_31))))) && ((var_1_19 < (var_1_28 / var_1_27)) ? ((var_1_5 > var_1_106) ? (var_1_32 == ((unsigned char) ((((var_1_5) < ((var_1_33 - var_1_13))) ? (var_1_5) : ((var_1_33 - var_1_13)))))) : (var_1_32 == ((unsigned char) (((((var_1_5) < (var_1_13)) ? (var_1_5) : (var_1_13))) + var_1_34)))) : (var_1_32 == ((unsigned char) ((var_1_35 - ((((var_1_5) < (var_1_36)) ? (var_1_5) : (var_1_36)))) - (((((var_1_37 + var_1_38)) < (var_1_13)) ? ((var_1_37 + var_1_38)) : (var_1_13)))))))) && ((var_1_8 != var_1_34) ? (var_1_120 ? (var_1_39 == ((signed char) (var_1_13 - var_1_37))) : ((var_1_35 < (var_1_33 - var_1_38)) ? (var_1_39 == ((signed char) (var_1_38 + var_1_36))) : (var_1_39 == ((signed char) var_1_38)))) : 1)) && (var_1_40 == ((double) ((((var_1_28) > ((((((var_1_25) > (var_1_27)) ? (var_1_25) : (var_1_27))) - var_1_26))) ? (var_1_28) : ((((((var_1_25) > (var_1_27)) ? (var_1_25) : (var_1_27))) - var_1_26))))))) && (((-16 * var_1_121) >= ((var_1_37 % var_1_35) + last_1_var_1_41)) ? (var_1_83 ? (var_1_41 == ((unsigned char) var_1_5)) : (var_1_41 == ((unsigned char) ((((((((var_1_37) > (((((var_1_34) < (var_1_13)) ? (var_1_34) : (var_1_13))))) ? (var_1_37) : (((((var_1_34) < (var_1_13)) ? (var_1_34) : (var_1_13))))))) < (var_1_33)) ? (((((var_1_37) > (((((var_1_34) < (var_1_13)) ? (var_1_34) : (var_1_13))))) ? (var_1_37) : (((((var_1_34) < (var_1_13)) ? (var_1_34) : (var_1_13))))))) : (var_1_33)))))) : (var_1_41 == ((unsigned char) ((((var_1_13) > (25)) ? (var_1_13) : (25))))))) && (var_1_42 == ((signed char) (var_1_13 - ((((var_1_37) > (var_1_5)) ? (var_1_37) : (var_1_5))))))) && ((var_1_109 <= var_1_10) ? (var_1_46 ? (var_1_43 == ((unsigned long int) (((((((((((var_1_5) > (var_1_109)) ? (var_1_5) : (var_1_109))) < 0 ) ? -((((var_1_5) > (var_1_109)) ? (var_1_5) : (var_1_109))) : ((((var_1_5) > (var_1_109)) ? (var_1_5) : (var_1_109)))))) < (((((var_1_34) > (var_1_109)) ? (var_1_34) : (var_1_109))))) ? ((((((((var_1_5) > (var_1_109)) ? (var_1_5) : (var_1_109))) < 0 ) ? -((((var_1_5) > (var_1_109)) ? (var_1_5) : (var_1_109))) : ((((var_1_5) > (var_1_109)) ? (var_1_5) : (var_1_109)))))) : (((((var_1_34) > (var_1_109)) ? (var_1_34) : (var_1_109)))))))) : (var_1_43 == ((unsigned long int) ((((((var_1_10) < 0 ) ? -(var_1_10) : (var_1_10))) - 128u) + 16u)))) : (var_1_43 == ((unsigned long int) var_1_37)))) && (var_1_44 == ((signed short int) ((((var_1_13) > (var_1_39)) ? (var_1_13) : (var_1_39)))))) && (((var_1_61 * (var_1_33 | -128)) >= var_1_5) ? (((var_1_35 + var_1_37) <= ((((var_1_93) > (var_1_36)) ? (var_1_93) : (var_1_36)))) ? (var_1_45 == ((unsigned long int) ((((((((var_1_33) < 0 ) ? -(var_1_33) : (var_1_33)))) > (var_1_34)) ? (((((var_1_33) < 0 ) ? -(var_1_33) : (var_1_33)))) : (var_1_34))))) : 1) : 1)) && ((last_1_var_1_121 < (last_1_var_1_52 * var_1_35)) ? (var_1_46 == ((unsigned char) 0)) : (var_1_46 == ((unsigned char) var_1_30)))) && ((! (var_1_25 <= ((((var_1_40) < (var_1_19)) ? (var_1_40) : (var_1_19))))) ? ((var_1_88 >= (var_1_27 + var_1_102)) ? ((var_1_109 < var_1_67) ? (var_1_47 == ((unsigned long int) ((((var_1_9 - (var_1_10 - var_1_35)) < 0 ) ? -(var_1_9 - (var_1_10 - var_1_35)) : (var_1_9 - (var_1_10 - var_1_35)))))) : (var_1_47 == ((unsigned long int) (((((var_1_35) < (var_1_10)) ? (var_1_35) : (var_1_10))) + (var_1_50 - var_1_63))))) : (var_1_47 == ((unsigned long int) (4063477532u - var_1_11)))) : (var_1_47 == ((unsigned long int) (var_1_63 + (var_1_10 - var_1_36)))))) && ((var_1_28 >= 1.00000000000002E13) ? (var_1_51 == ((signed short int) (((((-128 + var_1_45)) < (-100)) ? ((-128 + var_1_45)) : (-100))))) : (var_1_51 == ((signed short int) ((((var_1_34) > ((((((var_1_35) < (var_1_36)) ? (var_1_35) : (var_1_36))) - var_1_5))) ? (var_1_34) : ((((((var_1_35) < (var_1_36)) ? (var_1_35) : (var_1_36))) - var_1_5)))))))) && (var_1_76 ? (((var_1_38 <= 50) && (var_1_51 > last_1_var_1_52)) ? ((((((var_1_54) < (var_1_67)) ? (var_1_54) : (var_1_67))) >= var_1_41) ? (var_1_52 == ((unsigned long int) (var_1_35 + ((((var_1_13) < (var_1_108)) ? (var_1_13) : (var_1_108)))))) : 1) : (var_1_52 == ((unsigned long int) (var_1_9 - var_1_37)))) : 1)) && (((last_1_var_1_54 / var_1_33) >= ((var_1_38 ^ last_1_var_1_108) | var_1_8)) ? (var_1_54 == ((unsigned long int) (last_1_var_1_108 + var_1_11))) : 1)) && (var_1_56 == ((signed char) (((((var_1_36 - var_1_37)) > (((((var_1_13) < 0 ) ? -(var_1_13) : (var_1_13))))) ? ((var_1_36 - var_1_37)) : (((((var_1_13) < 0 ) ? -(var_1_13) : (var_1_13))))))))) && ((var_1_75 <= last_1_var_1_57) ? (var_1_57 == ((unsigned long int) ((((var_1_9) < 0 ) ? -(var_1_9) : (var_1_9))))) : (var_1_57 == ((unsigned long int) (((var_1_59 - var_1_13) - var_1_51) - ((var_1_60 - var_1_37) - var_1_34)))))) && ((var_1_37 <= (var_1_33 - var_1_38)) ? (var_1_61 == ((unsigned short int) (var_1_62 - 1))) : 1)) && ((last_1_var_1_52 < last_1_var_1_107) ? (var_1_63 == ((unsigned short int) (((((((((var_1_35 + var_1_36)) < (last_1_var_1_72)) ? ((var_1_35 + var_1_36)) : (last_1_var_1_72)))) < ((last_1_var_1_109 + var_1_5))) ? ((((((var_1_35 + var_1_36)) < (last_1_var_1_72)) ? ((var_1_35 + var_1_36)) : (last_1_var_1_72)))) : ((last_1_var_1_109 + var_1_5)))))) : 1)) && (var_1_64 == ((float) ((((var_1_26) > ((var_1_28 - ((((var_1_27) < 0 ) ? -(var_1_27) : (var_1_27)))))) ? (var_1_26) : ((var_1_28 - ((((var_1_27) < 0 ) ? -(var_1_27) : (var_1_27)))))))))) && ((var_1_36 < 2) ? ((var_1_41 <= (var_1_32 >> var_1_10)) ? (var_1_65 == ((signed long int) (((var_1_35 + var_1_118) + var_1_121) + (var_1_107 + var_1_70)))) : (var_1_65 == ((signed long int) (var_1_37 - var_1_38)))) : (var_1_65 == ((signed long int) ((((var_1_13) > (var_1_68)) ? (var_1_13) : (var_1_68))))))) && (var_1_30 ? (var_1_66 == ((double) var_1_26)) : 1)) && ((var_1_107 < (- (var_1_13 / var_1_35))) ? ((last_1_var_1_67 < (- var_1_13)) ? (var_1_67 == ((signed long int) var_1_38)) : (var_1_67 == ((signed long int) ((((((((var_1_35) > (var_1_34)) ? (var_1_35) : (var_1_34)))) < (-128)) ? (((((var_1_35) > (var_1_34)) ? (var_1_35) : (var_1_34)))) : (-128)))))) : (var_1_67 == ((signed long int) (var_1_54 + var_1_61))))) && ((last_1_var_1_107 < (var_1_37 / ((((var_1_13) < (var_1_35)) ? (var_1_13) : (var_1_35))))) ? (var_1_68 == ((signed short int) var_1_34)) : ((! last_1_var_1_76) ? ((last_1_var_1_79 > last_1_var_1_15) ? (var_1_68 == ((signed short int) var_1_5)) : (var_1_68 == ((signed short int) ((((last_1_var_1_68) > (last_1_var_1_51)) ? (last_1_var_1_68) : (last_1_var_1_51)))))) : 1))) && ((var_1_64 != var_1_86) ? ((var_1_8 >= var_1_11) ? (var_1_70 == ((signed short int) (((((var_1_14 + var_1_68) + var_1_13) < 0 ) ? -((var_1_14 + var_1_68) + var_1_13) : ((var_1_14 + var_1_68) + var_1_13))))) : (var_1_70 == ((signed short int) (var_1_34 + var_1_54)))) : (var_1_70 == ((signed short int) ((var_1_13 + var_1_38) - var_1_124))))) && (((128 >= (~ last_1_var_1_72)) || (last_1_var_1_72 < var_1_93)) ? ((var_1_75 > (var_1_63 * var_1_90)) ? (var_1_72 == ((signed long int) ((((var_1_34) < ((var_1_79 - var_1_62))) ? (var_1_34) : ((var_1_79 - var_1_62)))))) : ((((var_1_74 - var_1_38) - var_1_5) <= ((-10 / var_1_13) + var_1_21)) ? (var_1_72 == ((signed long int) ((((((((var_1_68) > (((((var_1_74) < (var_1_12)) ? (var_1_74) : (var_1_12))))) ? (var_1_68) : (((((var_1_74) < (var_1_12)) ? (var_1_74) : (var_1_12))))))) > ((var_1_121 + var_1_38))) ? (((((var_1_68) > (((((var_1_74) < (var_1_12)) ? (var_1_74) : (var_1_12))))) ? (var_1_68) : (((((var_1_74) < (var_1_12)) ? (var_1_74) : (var_1_12))))))) : ((var_1_121 + var_1_38)))))) : (var_1_72 == ((signed long int) (var_1_79 - var_1_12))))) : 1)) && (var_1_75 == ((unsigned char) ((((var_1_38) < (var_1_5)) ? (var_1_38) : (var_1_5)))))) && (((last_1_var_1_63 >> var_1_77) > last_1_var_1_67) ? (var_1_76 == ((unsigned char) ((! var_1_31) || var_1_30))) : ((last_1_var_1_118 >= last_1_var_1_54) ? (var_1_76 == ((unsigned char) var_1_31)) : (var_1_76 == ((unsigned char) (var_1_30 || ((! var_1_31) || var_1_78))))))) && ((var_1_23 > var_1_105) ? (var_1_79 == ((unsigned long int) ((((((var_1_62 + var_1_106)) > (var_1_23)) ? ((var_1_62 + var_1_106)) : (var_1_23))) + var_1_37))) : ((var_1_35 > var_1_74) ? (var_1_46 ? (var_1_79 == ((unsigned long int) ((((((var_1_59 - var_1_74) - var_1_63)) < ((var_1_8 - var_1_33))) ? (((var_1_59 - var_1_74) - var_1_63)) : ((var_1_8 - var_1_33)))))) : (var_1_79 == ((unsigned long int) ((((((var_1_59 - var_1_38) - 4u)) < (var_1_60)) ? (((var_1_59 - var_1_38) - 4u)) : (var_1_60)))))) : 1))) && ((var_1_70 >= var_1_9) ? (var_1_81 == ((float) (((((((((var_1_26) < (var_1_82)) ? (var_1_26) : (var_1_82))) - var_1_27)) < (var_1_28)) ? ((((((var_1_26) < (var_1_82)) ? (var_1_26) : (var_1_82))) - var_1_27)) : (var_1_28))))) : (var_1_81 == ((float) var_1_27)))) && (var_1_83 == ((unsigned char) var_1_78))) && ((var_1_42 < var_1_103) ? ((var_1_121 >= (var_1_37 / var_1_35)) ? (var_1_84 == ((double) var_1_27)) : (var_1_84 == ((double) ((((var_1_85) > (((((var_1_28) > (var_1_27)) ? (var_1_28) : (var_1_27))))) ? (var_1_85) : (((((var_1_28) > (var_1_27)) ? (var_1_28) : (var_1_27))))))))) : (var_1_84 == ((double) ((((var_1_25) < 0 ) ? -(var_1_25) : (var_1_25))))))) && (var_1_30 ? (var_1_86 == ((double) (var_1_28 + ((((63.5) > (100.5)) ? (63.5) : (100.5)))))) : (var_1_86 == ((double) (var_1_28 + var_1_87))))) && ((((((var_1_23) < 0 ) ? -(var_1_23) : (var_1_23))) > ((((((((50) > (var_1_108)) ? (50) : (var_1_108)))) > (-50)) ? (((((50) > (var_1_108)) ? (50) : (var_1_108)))) : (-50)))) ? ((var_1_103 <= (var_1_119 / ((((var_1_33) < (128)) ? (var_1_33) : (128))))) ? (var_1_122 ? (((((((var_1_28) > (var_1_26)) ? (var_1_28) : (var_1_26))) - var_1_25) >= (var_1_117 / var_1_19)) ? (var_1_88 == ((double) ((((var_1_26) < (8.5)) ? (var_1_26) : (8.5))))) : (var_1_88 == ((double) ((var_1_28 - var_1_89) + var_1_87)))) : 1) : (var_1_88 == ((double) (var_1_28 - var_1_26)))) : 1)) && (var_1_29 ? (var_1_90 == ((unsigned long int) ((((var_1_37) < (var_1_1)) ? (var_1_37) : (var_1_1))))) : 1)) && ((var_1_85 > var_1_28) ? (var_1_91 == ((float) (((((var_1_25) < (var_1_28)) ? (var_1_25) : (var_1_28))) - (var_1_27 - (4.0994868604932741E18f - var_1_92))))) : (var_1_91 == ((float) ((((var_1_28) < (((((var_1_87) > (-0.75f)) ? (var_1_87) : (-0.75f))))) ? (var_1_28) : (((((var_1_87) > (-0.75f)) ? (var_1_87) : (-0.75f)))))))))) && (((~ var_1_118) >= (last_1_var_1_93 + var_1_103)) ? (var_1_93 == ((unsigned short int) (var_1_62 - var_1_35))) : (var_1_120 ? (((64 + (- var_1_21)) > (((((var_1_8 - var_1_21)) > (var_1_38)) ? ((var_1_8 - var_1_21)) : (var_1_38)))) ? (var_1_93 == ((unsigned short int) (((((var_1_62) < (var_1_97)) ? (var_1_62) : (var_1_97))) - var_1_35))) : (var_1_93 == ((unsigned short int) (((((((((var_1_97) < (var_1_62)) ? (var_1_97) : (var_1_62)))) < (45680)) ? (((((var_1_97) < (var_1_62)) ? (var_1_97) : (var_1_62)))) : (45680))) - ((((var_1_13) < (var_1_38)) ? (var_1_13) : (var_1_38))))))) : (var_1_93 == ((unsigned short int) ((((((var_1_98 + var_1_99) - var_1_34)) > (((((var_1_77 + var_1_33) < 0 ) ? -(var_1_77 + var_1_33) : (var_1_77 + var_1_33))))) ? (((var_1_98 + var_1_99) - var_1_34)) : (((((var_1_77 + var_1_33) < 0 ) ? -(var_1_77 + var_1_33) : (var_1_77 + var_1_33))))))))))) && (var_1_31 ? (var_1_100 == ((unsigned long int) (var_1_21 + var_1_103))) : (var_1_100 == ((unsigned long int) (((((2u + var_1_99)) < ((var_1_103 + var_1_37))) ? ((2u + var_1_99)) : ((var_1_103 + var_1_37)))))))) && ((var_1_81 < var_1_86) ? (var_1_101 == ((double) ((var_1_92 - var_1_89) + ((((var_1_87) < (var_1_28)) ? (var_1_87) : (var_1_28)))))) : 1)) && (var_1_115 ? (var_1_112 ? (var_1_102 == ((float) var_1_26)) : 1) : 1)) && (((var_1_50 * var_1_37) >= ((~ 50u) / var_1_60)) ? (var_1_103 == ((signed char) ((((((((var_1_5) < 0 ) ? -(var_1_5) : (var_1_5)))) > (var_1_38)) ? (((((var_1_5) < 0 ) ? -(var_1_5) : (var_1_5)))) : (var_1_38))))) : 1)) && ((var_1_106 <= var_1_68) ? ((var_1_78 && var_1_30) ? (var_1_104 == ((double) (var_1_27 - var_1_82))) : (var_1_104 == ((double) ((var_1_28 + var_1_89) - var_1_92)))) : (var_1_104 == ((double) var_1_85)))) && (var_1_120 ? (var_1_105 == ((signed short int) var_1_106)) : (var_1_105 == ((signed short int) var_1_13)))) && (var_1_30 ? (var_1_106 == ((unsigned short int) var_1_34)) : (var_1_106 == ((unsigned short int) 10)))) && (last_1_var_1_46 ? (var_1_107 == ((unsigned short int) last_1_var_1_43)) : (var_1_107 == ((unsigned short int) var_1_98)))) && (var_1_112 ? (var_1_108 == ((unsigned short int) var_1_72)) : (var_1_108 == ((unsigned short int) var_1_36)))) && (var_1_112 ? (var_1_109 == ((unsigned char) var_1_35)) : (var_1_109 == ((unsigned char) var_1_34)))) && (var_1_110 == ((signed short int) var_1_38))) && (var_1_111 == ((double) var_1_27))) && (var_1_112 == ((unsigned char) var_1_30))) && (var_1_113 == ((signed char) var_1_77))) && (var_1_112 ? (var_1_114 == ((signed short int) var_1_35)) : 1)) && (var_1_115 == ((unsigned char) var_1_116))) && (var_1_122 ? (var_1_117 == ((double) var_1_89)) : (var_1_117 == ((double) 10.125)))) && (var_1_76 ? (var_1_118 == ((signed short int) var_1_33)) : (var_1_118 == ((signed short int) var_1_124)))) && (var_1_119 == ((signed long int) var_1_21))) && (var_1_83 ? (var_1_120 == ((unsigned char) (! (! var_1_31)))) : (var_1_120 == ((unsigned char) (var_1_31 && (! var_1_116)))))) && (var_1_121 == ((signed char) var_1_77))) && (var_1_122 == ((unsigned char) var_1_123))) && (var_1_124 == ((signed short int) var_1_68)) ; } int main(void) { isInitial = 1; initially(); while (1) { updateLastVariables(); updateVariables(); step(); __VERIFIER_assert(property()); isInitial = 0; } return 0; }