// 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 // Prototype declarations of the functions used to communicate with the model checkers 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_Batch77Amount500.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(); } } #define max(a,b) (((a) > (b)) ? (a) : (b)) #define min(a,b) (((a) < (b)) ? (a) : (b)) #define abs(a) (((a) < 0 ) ? -(a) : (a)) // Function prototypes // Internal control logic variables unsigned char isInitial = 0; // Signal variables signed long int var_1_1 = -8; float var_1_2 = 1.5; float var_1_3 = 24.7; unsigned short int var_1_10 = 32; unsigned short int var_1_16 = 49860; signed char var_1_17 = 32; signed char var_1_18 = -2; signed char var_1_19 = 10; signed char var_1_20 = 2; unsigned short int var_1_21 = 100; signed char var_1_23 = 16; signed char var_1_24 = 1; signed char var_1_25 = -10; float var_1_26 = 127.6; float var_1_27 = 5.625; float var_1_28 = 99.75; float var_1_29 = 16.8; float var_1_30 = 7.975; float var_1_31 = 10.75; unsigned char var_1_32 = 1; unsigned char var_1_33 = 0; unsigned char var_1_34 = 1; unsigned char var_1_35 = 0; signed char var_1_36 = 64; unsigned char var_1_37 = 1; unsigned char var_1_38 = 1; unsigned char var_1_39 = 0; unsigned char var_1_40 = 0; unsigned char var_1_41 = 0; unsigned char var_1_42 = 64; unsigned char var_1_43 = 128; unsigned char var_1_44 = 64; unsigned char var_1_45 = 64; unsigned long int var_1_46 = 256; unsigned long int var_1_48 = 2555450654; signed short int var_1_49 = 5; float var_1_50 = 64.5; unsigned short int var_1_51 = 1; signed short int var_1_53 = -2; signed long int var_1_54 = 32; float var_1_55 = 10000.3; unsigned char var_1_56 = 64; unsigned char var_1_57 = 237; signed long int var_1_58 = -256; signed long int var_1_59 = -10000000; unsigned short int var_1_60 = 1; unsigned short int var_1_61 = 28258; double var_1_62 = 10.2; double var_1_63 = 50.8; double var_1_64 = 100.5; double var_1_65 = 15.5; double var_1_66 = 63.2; unsigned long int var_1_67 = 10000000; unsigned long int var_1_68 = 10; unsigned char var_1_70 = 0; unsigned char var_1_71 = 0; unsigned short int var_1_72 = 256; unsigned char var_1_73 = 0; signed short int var_1_74 = 5; unsigned char var_1_75 = 1; double var_1_76 = 9.125; double var_1_77 = 0.0; signed long int var_1_78 = 16; unsigned char var_1_79 = 0; signed char var_1_80 = -50; double var_1_81 = 0.8; signed long int var_1_82 = -1; unsigned short int var_1_84 = 5; unsigned short int var_1_86 = 62187; unsigned char var_1_87 = 128; unsigned char var_1_88 = 4; signed char var_1_89 = -64; unsigned short int var_1_90 = 2; unsigned long int var_1_91 = 10000; signed long int var_1_92 = -500; signed short int var_1_93 = -32; signed short int var_1_94 = 10; signed char var_1_95 = 10; signed long int var_1_96 = 25; double var_1_97 = 1.2; signed long int var_1_98 = -8; float var_1_99 = 24.2; unsigned char var_1_100 = 4; double var_1_101 = 10.225; unsigned char var_1_102 = 1; unsigned char var_1_103 = 0; // Calibration values // Last'ed variables unsigned short int last_1_var_1_10 = 32; signed char last_1_var_1_17 = 32; unsigned short int last_1_var_1_21 = 100; signed char last_1_var_1_23 = 16; float last_1_var_1_26 = 127.6; unsigned char last_1_var_1_32 = 1; signed char last_1_var_1_36 = 64; unsigned char last_1_var_1_39 = 0; unsigned char last_1_var_1_42 = 64; unsigned long int last_1_var_1_46 = 256; unsigned short int last_1_var_1_51 = 1; signed long int last_1_var_1_54 = 32; unsigned char last_1_var_1_56 = 64; signed long int last_1_var_1_58 = -256; unsigned short int last_1_var_1_60 = 1; double last_1_var_1_62 = 10.2; unsigned long int last_1_var_1_67 = 10000000; unsigned long int last_1_var_1_68 = 10; unsigned char last_1_var_1_70 = 0; signed short int last_1_var_1_74 = 5; unsigned char last_1_var_1_75 = 1; signed long int last_1_var_1_78 = 16; unsigned char last_1_var_1_79 = 0; signed long int last_1_var_1_82 = -1; unsigned short int last_1_var_1_84 = 5; unsigned char last_1_var_1_87 = 128; signed char last_1_var_1_89 = -64; unsigned short int last_1_var_1_90 = 2; signed long int last_1_var_1_92 = -500; signed short int last_1_var_1_93 = -32; signed char last_1_var_1_95 = 10; double last_1_var_1_97 = 1.2; signed long int last_1_var_1_98 = -8; unsigned char last_1_var_1_100 = 4; // Additional functions void initially(void) { } void step(void) { // From: Req36Batch77Amount500 if (last_1_var_1_93 >= (max (last_1_var_1_58 , last_1_var_1_67))) { if ((last_1_var_1_82 == (last_1_var_1_56 / var_1_48)) && ((last_1_var_1_60 > last_1_var_1_67) || var_1_34)) { if (last_1_var_1_70) { var_1_82 = (min ((min (last_1_var_1_36 , last_1_var_1_93)) , last_1_var_1_89)); } else { var_1_82 = last_1_var_1_90; } } else { var_1_82 = (last_1_var_1_51 - last_1_var_1_36); } } else { var_1_82 = last_1_var_1_87; } // From: Req14Batch77Amount500 if ((max (last_1_var_1_26 , last_1_var_1_62)) >= var_1_29) { var_1_49 = (last_1_var_1_17 - (max (16 , var_1_19))); } else { if (var_1_3 < (var_1_2 / var_1_50)) { var_1_49 = (max (last_1_var_1_21 , (var_1_24 - 16))); } else { if (last_1_var_1_67 >= var_1_20) { var_1_49 = ((min ((var_1_19 + var_1_44) , var_1_43)) - var_1_24); } else { var_1_49 = (last_1_var_1_21 + (min (32 , var_1_20))); } } } // From: Req32Batch77Amount500 signed long int stepLocal_24 = min (var_1_45 , last_1_var_1_51); if (stepLocal_24 <= (last_1_var_1_78 - last_1_var_1_98)) { var_1_78 = (abs (abs (last_1_var_1_74))); } else { var_1_78 = (min (var_1_45 , last_1_var_1_95)); } // From: Req45Batch77Amount500 if (last_1_var_1_32) { var_1_95 = var_1_20; } else { var_1_95 = var_1_25; } // From: Req26Batch77Amount500 if ((last_1_var_1_78 % 4) <= var_1_18) { var_1_70 = (! var_1_35); } // From: Req10Batch77Amount500 if (! var_1_34) { if (var_1_28 >= var_1_29) { var_1_38 = ((var_1_35 && var_1_33) || (var_1_70 || var_1_34)); } } // From: Req2Batch77Amount500 if (last_1_var_1_39 || ((- last_1_var_1_84) < (last_1_var_1_10 + last_1_var_1_21))) { if (((last_1_var_1_84 * last_1_var_1_74) * last_1_var_1_90) != (last_1_var_1_21 * last_1_var_1_60)) { var_1_10 = (last_1_var_1_87 + last_1_var_1_100); } else { var_1_10 = (last_1_var_1_100 + last_1_var_1_87); } } else { if (last_1_var_1_39 && (last_1_var_1_87 >= (- last_1_var_1_90))) { var_1_10 = (last_1_var_1_87 + last_1_var_1_100); } else { if (last_1_var_1_67 <= 500) { var_1_10 = (last_1_var_1_100 + last_1_var_1_87); } else { var_1_10 = (max ((var_1_16 - last_1_var_1_100) , (min (last_1_var_1_87 , 100)))); } } } // From: Req24Batch77Amount500 if (! ((-256 * last_1_var_1_87) < var_1_61)) { if (last_1_var_1_54 <= (min ((last_1_var_1_87 & var_1_24) , 16))) { if ((-16 < 50) || last_1_var_1_39) { var_1_67 = (max ((max ((var_1_48 - var_1_19) , var_1_61)) , var_1_57)); } else { if (var_1_3 >= var_1_63) { var_1_67 = last_1_var_1_87; } else { var_1_67 = var_1_61; } } } } // From: Req19Batch77Amount500 unsigned long int stepLocal_14 = last_1_var_1_46 / var_1_45; unsigned char stepLocal_13 = var_1_31 >= last_1_var_1_97; if (stepLocal_14 > var_1_24) { var_1_56 = (((var_1_57 - 10) - var_1_19) - var_1_45); } else { if (last_1_var_1_75 && stepLocal_13) { var_1_56 = var_1_43; } else { if (last_1_var_1_75) { var_1_56 = (max (var_1_43 , (max ((var_1_57 - var_1_45) , 2)))); } else { var_1_56 = (var_1_57 - var_1_19); } } } // From: Req4Batch77Amount500 signed long int stepLocal_4 = last_1_var_1_36; signed long int stepLocal_3 = (var_1_20 - var_1_19) * last_1_var_1_42; signed long int stepLocal_2 = last_1_var_1_90; if (var_1_20 >= stepLocal_2) { if (stepLocal_3 > last_1_var_1_21) { var_1_21 = var_1_16; } else { if (last_1_var_1_87 != stepLocal_4) { var_1_21 = (var_1_19 + last_1_var_1_42); } else { var_1_21 = (var_1_16 - 10); } } } else { if (last_1_var_1_39) { if (last_1_var_1_32) { var_1_21 = last_1_var_1_87; } else { var_1_21 = last_1_var_1_42; } } else { var_1_21 = var_1_19; } } // From: Req12Batch77Amount500 if (last_1_var_1_56 > last_1_var_1_23) { if ((- (last_1_var_1_17 * last_1_var_1_84)) == (last_1_var_1_67 * (-256 / var_1_16))) { var_1_42 = (var_1_43 - ((min (var_1_44 , var_1_45)) - (max (var_1_19 , 0)))); } } else { if (var_1_33) { var_1_42 = (min ((var_1_45 + var_1_44) , var_1_43)); } else { var_1_42 = ((abs (var_1_43)) - var_1_44); } } // From: Req5Batch77Amount500 signed long int stepLocal_5 = -100; if (stepLocal_5 != var_1_21) { var_1_23 = (max ((max ((min (var_1_18 , var_1_19)) , (var_1_20 - var_1_24))) , (var_1_25 + 50))); } else { var_1_23 = var_1_24; } // From: Req50Batch77Amount500 if (last_1_var_1_79) { var_1_100 = var_1_20; } // From: Req17Batch77Amount500 var_1_54 = var_1_100; // From: Req41Batch77Amount500 var_1_91 = var_1_100; // From: Req38Batch77Amount500 signed long int stepLocal_25 = last_1_var_1_92; if ((-0.8 / var_1_77) >= var_1_3) { if (stepLocal_25 == last_1_var_1_90) { var_1_87 = var_1_44; } else { var_1_87 = (min ((max ((var_1_20 + var_1_88) , var_1_24)) , var_1_57)); } } else { var_1_87 = (min (var_1_19 , var_1_57)); } // From: Req8Batch77Amount500 if (! (! var_1_33)) { var_1_36 = var_1_19; } // From: Req9Batch77Amount500 if (! var_1_33) { var_1_37 = ((var_1_18 != (var_1_24 - var_1_20)) || var_1_33); } else { var_1_37 = (! (! var_1_33)); } // From: Req18Batch77Amount500 if (var_1_33) { var_1_55 = (var_1_29 + var_1_30); } else { var_1_55 = (min (var_1_28 , var_1_31)); } // From: Req21Batch77Amount500 signed long int stepLocal_15 = (~ var_1_43) % var_1_45; if (var_1_16 > stepLocal_15) { var_1_59 = (var_1_44 - var_1_21); } else { var_1_59 = (abs (var_1_57)); } // From: Req31Batch77Amount500 if (-0.75f <= (- var_1_63)) { var_1_76 = var_1_63; } else { var_1_76 = ((var_1_29 - (var_1_77 - var_1_30)) + var_1_31); } // From: Req34Batch77Amount500 if (var_1_76 <= var_1_76) { var_1_80 = (max (var_1_25 , 50)); } else { var_1_80 = (max (var_1_24 , var_1_57)); } // From: Req39Batch77Amount500 if ((var_1_27 / var_1_77) > (var_1_28 - (var_1_30 + var_1_29))) { if ((var_1_55 * 7.8f) < ((- var_1_29) / var_1_77)) { var_1_89 = var_1_57; } else { var_1_89 = var_1_25; } } // From: Req43Batch77Amount500 if (var_1_41) { var_1_93 = var_1_25; } // From: Req46Batch77Amount500 if (var_1_35) { var_1_96 = var_1_93; } else { var_1_96 = 8; } // From: Req47Batch77Amount500 var_1_97 = var_1_66; // From: Req48Batch77Amount500 var_1_98 = var_1_45; // From: Req49Batch77Amount500 var_1_99 = var_1_31; // From: Req51Batch77Amount500 if (var_1_40) { var_1_101 = var_1_64; } else { var_1_101 = var_1_66; } // From: Req15Batch77Amount500 signed long int stepLocal_11 = (var_1_82 / var_1_43) & 8; if (last_1_var_1_51 >= stepLocal_11) { var_1_51 = (var_1_16 - var_1_42); } else { if (var_1_34) { var_1_51 = (var_1_44 + (27467 - var_1_45)); } else { var_1_51 = ((abs (var_1_100)) + var_1_42); } } // From: Req22Batch77Amount500 if ((var_1_87 * var_1_10) < var_1_91) { var_1_60 = (min (var_1_49 , var_1_16)); } else { var_1_60 = (max (((var_1_61 - var_1_57) + var_1_19) , var_1_67)); } // From: Req13Batch77Amount500 signed char stepLocal_10 = var_1_36; signed long int stepLocal_9 = var_1_42 / var_1_44; if (var_1_25 > stepLocal_9) { if (var_1_78 > stepLocal_10) { var_1_46 = (var_1_48 - var_1_19); } else { var_1_46 = (var_1_48 - var_1_42); } } else { var_1_46 = var_1_20; } // From: Req20Batch77Amount500 var_1_58 = var_1_46; // From: Req7Batch77Amount500 if (var_1_100 != var_1_78) { var_1_32 = (var_1_33 && var_1_34); } else { if (var_1_36 != ((var_1_95 / 500) >> var_1_54)) { if ((var_1_78 / var_1_16) <= var_1_100) { var_1_32 = (! var_1_33); } } else { var_1_32 = ((! var_1_38) && var_1_35); } } // From: Req30Batch77Amount500 if (var_1_40 || ((var_1_21 + var_1_58) >= var_1_57)) { var_1_75 = (! (! 0)); } else { var_1_75 = (((var_1_29 * var_1_64) >= var_1_3) && var_1_40); } // From: Req40Batch77Amount500 if (var_1_75) { var_1_90 = var_1_24; } else { var_1_90 = 32; } // From: Req25Batch77Amount500 unsigned short int stepLocal_19 = var_1_16; if (stepLocal_19 >= last_1_var_1_68) { if (var_1_32) { var_1_68 = var_1_43; } else { var_1_68 = (var_1_48 - 100u); } } // From: Req3Batch77Amount500 signed long int stepLocal_1 = var_1_95 / var_1_16; signed long int stepLocal_0 = var_1_56 ^ var_1_87; if (stepLocal_1 > (var_1_21 * var_1_10)) { if (var_1_100 > stepLocal_0) { var_1_17 = (var_1_18 + (var_1_19 - var_1_20)); } } else { var_1_17 = (var_1_20 - var_1_19); } // From: Req37Batch77Amount500 if (var_1_93 <= var_1_60) { if ((var_1_2 + 3.4f) > 8.25f) { var_1_84 = var_1_42; } } else { var_1_84 = (max (((max (var_1_16 , var_1_86)) - var_1_61) , (min (var_1_20 , var_1_100)))); } // From: Req42Batch77Amount500 if (var_1_75) { var_1_92 = var_1_87; } else { var_1_92 = var_1_10; } // From: Req28Batch77Amount500 unsigned long int stepLocal_23 = min (var_1_43 , (2352903485u - var_1_21)); if (var_1_56 < stepLocal_23) { var_1_73 = var_1_34; } // From: Req29Batch77Amount500 if ((max (var_1_31 , var_1_50)) <= var_1_30) { var_1_74 = -5; } else { if (var_1_42 == var_1_100) { var_1_74 = ((min ((var_1_44 + last_1_var_1_74) , last_1_var_1_74)) + var_1_19); } } // From: Req1Batch77Amount500 if ((var_1_2 - var_1_3) >= var_1_99) { var_1_1 = ((var_1_49 + var_1_60) + var_1_42); } else { var_1_1 = (var_1_90 - var_1_42); } // From: Req16Batch77Amount500 signed char stepLocal_12 = var_1_89; if (var_1_38) { if (stepLocal_12 <= var_1_19) { var_1_53 = ((min (var_1_18 , var_1_20)) + var_1_19); } else { var_1_53 = var_1_19; } } else { var_1_53 = (((max (var_1_1 , var_1_67)) + (var_1_18 + var_1_44)) + var_1_19); } // From: Req27Batch77Amount500 signed char stepLocal_22 = var_1_95; unsigned char stepLocal_21 = var_1_17 <= (var_1_95 + var_1_82); signed long int stepLocal_20 = var_1_95 % (max (var_1_57 , var_1_72)); if (((var_1_48 + var_1_82) <= (min (var_1_56 , var_1_19))) && stepLocal_21) { if (stepLocal_22 <= var_1_42) { var_1_71 = (! var_1_35); } else { var_1_71 = 0; } } else { if (var_1_78 >= stepLocal_20) { var_1_71 = (! var_1_41); } else { var_1_71 = ((var_1_33 || (var_1_45 != var_1_57)) || var_1_34); } } // From: Req44Batch77Amount500 if (var_1_71) { var_1_94 = var_1_93; } else { var_1_94 = var_1_20; } // From: Req52Batch77Amount500 unsigned short int stepLocal_26 = var_1_21; if ((var_1_42 * var_1_87) >= stepLocal_26) { var_1_102 = (((var_1_84 < var_1_94) || var_1_33) && (var_1_34 && var_1_103)); } else { var_1_102 = var_1_33; } // From: Req6Batch77Amount500 unsigned char stepLocal_7 = var_1_2 < (var_1_3 - var_1_27); signed short int stepLocal_6 = var_1_49; if (var_1_73) { if (stepLocal_6 <= (var_1_16 - (max (var_1_42 , var_1_93)))) { if (var_1_70 || stepLocal_7) { var_1_26 = (var_1_28 - ((var_1_29 + var_1_30) + var_1_31)); } else { var_1_26 = (var_1_30 - var_1_29); } } } else { if (var_1_28 <= 4.5f) { var_1_26 = (abs (-0.5f)); } } // From: Req23Batch77Amount500 signed long int stepLocal_18 = var_1_87 + var_1_89; signed long int stepLocal_17 = abs (var_1_89); unsigned long int stepLocal_16 = (min (var_1_19 , var_1_61)) - (max (var_1_42 , var_1_46)); if (stepLocal_16 < var_1_82) { var_1_62 = var_1_31; } else { if (stepLocal_17 != var_1_25) { if (stepLocal_18 > (max (-1 , (var_1_56 >> var_1_68)))) { var_1_62 = (var_1_29 - var_1_28); } else { var_1_62 = (var_1_63 - 127.2); } } else { var_1_62 = ((var_1_29 + (var_1_64 + var_1_65)) + (var_1_30 + var_1_66)); } } // From: Req33Batch77Amount500 if ((max (var_1_10 , var_1_92)) < var_1_87) { var_1_79 = (! (! var_1_35)); } else { var_1_79 = (var_1_75 || (! 0)); } // From: Req11Batch77Amount500 unsigned char stepLocal_8 = var_1_73 || var_1_79; if (var_1_27 < var_1_55) { if ((16 <= var_1_84) && stepLocal_8) { if ((var_1_28 * var_1_31) >= ((var_1_29 * var_1_2) * var_1_55)) { var_1_39 = ((! var_1_33) || (var_1_35 || var_1_40)); } else { var_1_39 = var_1_41; } } } else { var_1_39 = var_1_33; } // From: Req35Batch77Amount500 if (var_1_39 || var_1_38) { if (var_1_45 > ((var_1_46 & var_1_10) + var_1_21)) { var_1_81 = (max (var_1_64 , var_1_65)); } } else { if ((var_1_28 - 499.25) != 25.4) { var_1_81 = (abs (var_1_66 + (min (var_1_31 , var_1_29)))); } } } void updateVariables() { var_1_2 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_2 >= 0.0F && var_1_2 <= -1.0e-20F) || (var_1_2 <= 9223372.036854776000e+12F && var_1_2 >= 1.0e-20F )); var_1_3 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_3 >= 0.0F && var_1_3 <= -1.0e-20F) || (var_1_3 <= 9223372.036854776000e+12F && var_1_3 >= 1.0e-20F )); var_1_16 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_16 >= 32767); assume_abort_if_not(var_1_16 <= 65534); var_1_18 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_18 >= -63); assume_abort_if_not(var_1_18 <= 63); var_1_19 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_19 >= 0); assume_abort_if_not(var_1_19 <= 63); var_1_20 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_20 >= 0); assume_abort_if_not(var_1_20 <= 63); var_1_24 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_24 >= 0); assume_abort_if_not(var_1_24 <= 126); var_1_25 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_25 >= -63); assume_abort_if_not(var_1_25 <= 63); var_1_27 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_27 >= 0.0F && var_1_27 <= -1.0e-20F) || (var_1_27 <= 9223372.036854776000e+12F && var_1_27 >= 1.0e-20F )); var_1_28 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_28 >= 0.0F && var_1_28 <= -1.0e-20F) || (var_1_28 <= 9223372.036854765600e+12F && var_1_28 >= 1.0e-20F )); var_1_29 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_29 >= 0.0F && var_1_29 <= -1.0e-20F) || (var_1_29 <= 2305843.009213691390e+12F && var_1_29 >= 1.0e-20F )); var_1_30 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_30 >= 0.0F && var_1_30 <= -1.0e-20F) || (var_1_30 <= 2305843.009213691390e+12F && var_1_30 >= 1.0e-20F )); var_1_31 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_31 >= 0.0F && var_1_31 <= -1.0e-20F) || (var_1_31 <= 4611686.018427382800e+12F && var_1_31 >= 1.0e-20F )); var_1_33 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_33 >= 1); assume_abort_if_not(var_1_33 <= 1); var_1_34 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_34 >= 1); assume_abort_if_not(var_1_34 <= 1); var_1_35 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_35 >= 0); assume_abort_if_not(var_1_35 <= 0); var_1_40 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_40 >= 0); assume_abort_if_not(var_1_40 <= 0); var_1_41 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_41 >= 0); assume_abort_if_not(var_1_41 <= 0); var_1_43 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_43 >= 127); assume_abort_if_not(var_1_43 <= 254); var_1_44 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_44 >= 63); assume_abort_if_not(var_1_44 <= 127); var_1_45 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_45 >= 63); assume_abort_if_not(var_1_45 <= 127); var_1_48 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_48 >= 2147483647); assume_abort_if_not(var_1_48 <= 4294967294); var_1_50 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_50 >= -922337.2036854776000e+13F && var_1_50 <= -1.0e-20F) || (var_1_50 <= 9223372.036854776000e+12F && var_1_50 >= 1.0e-20F )); assume_abort_if_not(var_1_50 != 0.0F); var_1_57 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_57 >= 222); assume_abort_if_not(var_1_57 <= 254); var_1_61 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_61 >= 16383); assume_abort_if_not(var_1_61 <= 32767); var_1_63 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_63 >= 0.0F && var_1_63 <= -1.0e-20F) || (var_1_63 <= 9223372.036854765600e+12F && var_1_63 >= 1.0e-20F )); var_1_64 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_64 >= -115292.1504606845700e+13F && var_1_64 <= -1.0e-20F) || (var_1_64 <= 1152921.504606845700e+12F && var_1_64 >= 1.0e-20F )); var_1_65 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_65 >= -115292.1504606845700e+13F && var_1_65 <= -1.0e-20F) || (var_1_65 <= 1152921.504606845700e+12F && var_1_65 >= 1.0e-20F )); var_1_66 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_66 >= -230584.3009213691390e+13F && var_1_66 <= -1.0e-20F) || (var_1_66 <= 2305843.009213691390e+12F && var_1_66 >= 1.0e-20F )); var_1_72 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_72 >= 0); assume_abort_if_not(var_1_72 <= 65535); assume_abort_if_not(var_1_72 != 0); var_1_77 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_77 >= 2305843.009213691390e+12F && var_1_77 <= -1.0e-20F) || (var_1_77 <= 4611686.018427382800e+12F && var_1_77 >= 1.0e-20F )); var_1_86 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_86 >= 32767); assume_abort_if_not(var_1_86 <= 65534); var_1_88 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_88 >= 0); assume_abort_if_not(var_1_88 <= 127); var_1_103 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_103 >= 1); assume_abort_if_not(var_1_103 <= 1); } void updateLastVariables() { last_1_var_1_10 = var_1_10; last_1_var_1_17 = var_1_17; last_1_var_1_21 = var_1_21; last_1_var_1_23 = var_1_23; last_1_var_1_26 = var_1_26; last_1_var_1_32 = var_1_32; last_1_var_1_36 = var_1_36; last_1_var_1_39 = var_1_39; last_1_var_1_42 = var_1_42; last_1_var_1_46 = var_1_46; last_1_var_1_51 = var_1_51; last_1_var_1_54 = var_1_54; last_1_var_1_56 = var_1_56; last_1_var_1_58 = var_1_58; last_1_var_1_60 = var_1_60; last_1_var_1_62 = var_1_62; last_1_var_1_67 = var_1_67; last_1_var_1_68 = var_1_68; last_1_var_1_70 = var_1_70; last_1_var_1_74 = var_1_74; last_1_var_1_75 = var_1_75; last_1_var_1_78 = var_1_78; last_1_var_1_79 = var_1_79; last_1_var_1_82 = var_1_82; last_1_var_1_84 = var_1_84; last_1_var_1_87 = var_1_87; last_1_var_1_89 = var_1_89; last_1_var_1_90 = var_1_90; last_1_var_1_92 = var_1_92; last_1_var_1_93 = var_1_93; last_1_var_1_95 = var_1_95; last_1_var_1_97 = var_1_97; last_1_var_1_98 = var_1_98; last_1_var_1_100 = var_1_100; } int property() { return (((((((((((((((((((((((((((((((((((((((((((((((((((((var_1_2 - var_1_3) >= var_1_99) ? (var_1_1 == ((signed long int) ((var_1_49 + var_1_60) + var_1_42))) : (var_1_1 == ((signed long int) (var_1_90 - var_1_42)))) && ((last_1_var_1_39 || ((- last_1_var_1_84) < (last_1_var_1_10 + last_1_var_1_21))) ? ((((last_1_var_1_84 * last_1_var_1_74) * last_1_var_1_90) != (last_1_var_1_21 * last_1_var_1_60)) ? (var_1_10 == ((unsigned short int) (last_1_var_1_87 + last_1_var_1_100))) : (var_1_10 == ((unsigned short int) (last_1_var_1_100 + last_1_var_1_87)))) : ((last_1_var_1_39 && (last_1_var_1_87 >= (- last_1_var_1_90))) ? (var_1_10 == ((unsigned short int) (last_1_var_1_87 + last_1_var_1_100))) : ((last_1_var_1_67 <= 500) ? (var_1_10 == ((unsigned short int) (last_1_var_1_100 + last_1_var_1_87))) : (var_1_10 == ((unsigned short int) (max ((var_1_16 - last_1_var_1_100) , (min (last_1_var_1_87 , 100)))))))))) && (((var_1_95 / var_1_16) > (var_1_21 * var_1_10)) ? ((var_1_100 > (var_1_56 ^ var_1_87)) ? (var_1_17 == ((signed char) (var_1_18 + (var_1_19 - var_1_20)))) : 1) : (var_1_17 == ((signed char) (var_1_20 - var_1_19))))) && ((var_1_20 >= last_1_var_1_90) ? ((((var_1_20 - var_1_19) * last_1_var_1_42) > last_1_var_1_21) ? (var_1_21 == ((unsigned short int) var_1_16)) : ((last_1_var_1_87 != last_1_var_1_36) ? (var_1_21 == ((unsigned short int) (var_1_19 + last_1_var_1_42))) : (var_1_21 == ((unsigned short int) (var_1_16 - 10))))) : (last_1_var_1_39 ? (last_1_var_1_32 ? (var_1_21 == ((unsigned short int) last_1_var_1_87)) : (var_1_21 == ((unsigned short int) last_1_var_1_42))) : (var_1_21 == ((unsigned short int) var_1_19))))) && ((-100 != var_1_21) ? (var_1_23 == ((signed char) (max ((max ((min (var_1_18 , var_1_19)) , (var_1_20 - var_1_24))) , (var_1_25 + 50))))) : (var_1_23 == ((signed char) var_1_24)))) && (var_1_73 ? ((var_1_49 <= (var_1_16 - (max (var_1_42 , var_1_93)))) ? ((var_1_70 || (var_1_2 < (var_1_3 - var_1_27))) ? (var_1_26 == ((float) (var_1_28 - ((var_1_29 + var_1_30) + var_1_31)))) : (var_1_26 == ((float) (var_1_30 - var_1_29)))) : 1) : ((var_1_28 <= 4.5f) ? (var_1_26 == ((float) (abs (-0.5f)))) : 1))) && ((var_1_100 != var_1_78) ? (var_1_32 == ((unsigned char) (var_1_33 && var_1_34))) : ((var_1_36 != ((var_1_95 / 500) >> var_1_54)) ? (((var_1_78 / var_1_16) <= var_1_100) ? (var_1_32 == ((unsigned char) (! var_1_33))) : 1) : (var_1_32 == ((unsigned char) ((! var_1_38) && var_1_35)))))) && ((! (! var_1_33)) ? (var_1_36 == ((signed char) var_1_19)) : 1)) && ((! var_1_33) ? (var_1_37 == ((unsigned char) ((var_1_18 != (var_1_24 - var_1_20)) || var_1_33))) : (var_1_37 == ((unsigned char) (! (! var_1_33)))))) && ((! var_1_34) ? ((var_1_28 >= var_1_29) ? (var_1_38 == ((unsigned char) ((var_1_35 && var_1_33) || (var_1_70 || var_1_34)))) : 1) : 1)) && ((var_1_27 < var_1_55) ? (((16 <= var_1_84) && (var_1_73 || var_1_79)) ? (((var_1_28 * var_1_31) >= ((var_1_29 * var_1_2) * var_1_55)) ? (var_1_39 == ((unsigned char) ((! var_1_33) || (var_1_35 || var_1_40)))) : (var_1_39 == ((unsigned char) var_1_41))) : 1) : (var_1_39 == ((unsigned char) var_1_33)))) && ((last_1_var_1_56 > last_1_var_1_23) ? (((- (last_1_var_1_17 * last_1_var_1_84)) == (last_1_var_1_67 * (-256 / var_1_16))) ? (var_1_42 == ((unsigned char) (var_1_43 - ((min (var_1_44 , var_1_45)) - (max (var_1_19 , 0)))))) : 1) : (var_1_33 ? (var_1_42 == ((unsigned char) (min ((var_1_45 + var_1_44) , var_1_43)))) : (var_1_42 == ((unsigned char) ((abs (var_1_43)) - var_1_44)))))) && ((var_1_25 > (var_1_42 / var_1_44)) ? ((var_1_78 > var_1_36) ? (var_1_46 == ((unsigned long int) (var_1_48 - var_1_19))) : (var_1_46 == ((unsigned long int) (var_1_48 - var_1_42)))) : (var_1_46 == ((unsigned long int) var_1_20)))) && (((max (last_1_var_1_26 , last_1_var_1_62)) >= var_1_29) ? (var_1_49 == ((signed short int) (last_1_var_1_17 - (max (16 , var_1_19))))) : ((var_1_3 < (var_1_2 / var_1_50)) ? (var_1_49 == ((signed short int) (max (last_1_var_1_21 , (var_1_24 - 16))))) : ((last_1_var_1_67 >= var_1_20) ? (var_1_49 == ((signed short int) ((min ((var_1_19 + var_1_44) , var_1_43)) - var_1_24))) : (var_1_49 == ((signed short int) (last_1_var_1_21 + (min (32 , var_1_20))))))))) && ((last_1_var_1_51 >= ((var_1_82 / var_1_43) & 8)) ? (var_1_51 == ((unsigned short int) (var_1_16 - var_1_42))) : (var_1_34 ? (var_1_51 == ((unsigned short int) (var_1_44 + (27467 - var_1_45)))) : (var_1_51 == ((unsigned short int) ((abs (var_1_100)) + var_1_42)))))) && (var_1_38 ? ((var_1_89 <= var_1_19) ? (var_1_53 == ((signed short int) ((min (var_1_18 , var_1_20)) + var_1_19))) : (var_1_53 == ((signed short int) var_1_19))) : (var_1_53 == ((signed short int) (((max (var_1_1 , var_1_67)) + (var_1_18 + var_1_44)) + var_1_19))))) && (var_1_54 == ((signed long int) var_1_100))) && (var_1_33 ? (var_1_55 == ((float) (var_1_29 + var_1_30))) : (var_1_55 == ((float) (min (var_1_28 , var_1_31)))))) && (((last_1_var_1_46 / var_1_45) > var_1_24) ? (var_1_56 == ((unsigned char) (((var_1_57 - 10) - var_1_19) - var_1_45))) : ((last_1_var_1_75 && (var_1_31 >= last_1_var_1_97)) ? (var_1_56 == ((unsigned char) var_1_43)) : (last_1_var_1_75 ? (var_1_56 == ((unsigned char) (max (var_1_43 , (max ((var_1_57 - var_1_45) , 2)))))) : (var_1_56 == ((unsigned char) (var_1_57 - var_1_19))))))) && (var_1_58 == ((signed long int) var_1_46))) && ((var_1_16 > ((~ var_1_43) % var_1_45)) ? (var_1_59 == ((signed long int) (var_1_44 - var_1_21))) : (var_1_59 == ((signed long int) (abs (var_1_57)))))) && (((var_1_87 * var_1_10) < var_1_91) ? (var_1_60 == ((unsigned short int) (min (var_1_49 , var_1_16)))) : (var_1_60 == ((unsigned short int) (max (((var_1_61 - var_1_57) + var_1_19) , var_1_67)))))) && ((((min (var_1_19 , var_1_61)) - (max (var_1_42 , var_1_46))) < var_1_82) ? (var_1_62 == ((double) var_1_31)) : (((abs (var_1_89)) != var_1_25) ? (((var_1_87 + var_1_89) > (max (-1 , (var_1_56 >> var_1_68)))) ? (var_1_62 == ((double) (var_1_29 - var_1_28))) : (var_1_62 == ((double) (var_1_63 - 127.2)))) : (var_1_62 == ((double) ((var_1_29 + (var_1_64 + var_1_65)) + (var_1_30 + var_1_66))))))) && ((! ((-256 * last_1_var_1_87) < var_1_61)) ? ((last_1_var_1_54 <= (min ((last_1_var_1_87 & var_1_24) , 16))) ? (((-16 < 50) || last_1_var_1_39) ? (var_1_67 == ((unsigned long int) (max ((max ((var_1_48 - var_1_19) , var_1_61)) , var_1_57)))) : ((var_1_3 >= var_1_63) ? (var_1_67 == ((unsigned long int) last_1_var_1_87)) : (var_1_67 == ((unsigned long int) var_1_61)))) : 1) : 1)) && ((var_1_16 >= last_1_var_1_68) ? (var_1_32 ? (var_1_68 == ((unsigned long int) var_1_43)) : (var_1_68 == ((unsigned long int) (var_1_48 - 100u)))) : 1)) && (((last_1_var_1_78 % 4) <= var_1_18) ? (var_1_70 == ((unsigned char) (! var_1_35))) : 1)) && ((((var_1_48 + var_1_82) <= (min (var_1_56 , var_1_19))) && (var_1_17 <= (var_1_95 + var_1_82))) ? ((var_1_95 <= var_1_42) ? (var_1_71 == ((unsigned char) (! var_1_35))) : (var_1_71 == ((unsigned char) 0))) : ((var_1_78 >= (var_1_95 % (max (var_1_57 , var_1_72)))) ? (var_1_71 == ((unsigned char) (! var_1_41))) : (var_1_71 == ((unsigned char) ((var_1_33 || (var_1_45 != var_1_57)) || var_1_34)))))) && ((var_1_56 < (min (var_1_43 , (2352903485u - var_1_21)))) ? (var_1_73 == ((unsigned char) var_1_34)) : 1)) && (((max (var_1_31 , var_1_50)) <= var_1_30) ? (var_1_74 == ((signed short int) -5)) : ((var_1_42 == var_1_100) ? (var_1_74 == ((signed short int) ((min ((var_1_44 + last_1_var_1_74) , last_1_var_1_74)) + var_1_19))) : 1))) && ((var_1_40 || ((var_1_21 + var_1_58) >= var_1_57)) ? (var_1_75 == ((unsigned char) (! (! 0)))) : (var_1_75 == ((unsigned char) (((var_1_29 * var_1_64) >= var_1_3) && var_1_40))))) && ((-0.75f <= (- var_1_63)) ? (var_1_76 == ((double) var_1_63)) : (var_1_76 == ((double) ((var_1_29 - (var_1_77 - var_1_30)) + var_1_31))))) && (((min (var_1_45 , last_1_var_1_51)) <= (last_1_var_1_78 - last_1_var_1_98)) ? (var_1_78 == ((signed long int) (abs (abs (last_1_var_1_74))))) : (var_1_78 == ((signed long int) (min (var_1_45 , last_1_var_1_95)))))) && (((max (var_1_10 , var_1_92)) < var_1_87) ? (var_1_79 == ((unsigned char) (! (! var_1_35)))) : (var_1_79 == ((unsigned char) (var_1_75 || (! 0)))))) && ((var_1_76 <= var_1_76) ? (var_1_80 == ((signed char) (max (var_1_25 , 50)))) : (var_1_80 == ((signed char) (max (var_1_24 , var_1_57)))))) && ((var_1_39 || var_1_38) ? ((var_1_45 > ((var_1_46 & var_1_10) + var_1_21)) ? (var_1_81 == ((double) (max (var_1_64 , var_1_65)))) : 1) : (((var_1_28 - 499.25) != 25.4) ? (var_1_81 == ((double) (abs (var_1_66 + (min (var_1_31 , var_1_29)))))) : 1))) && ((last_1_var_1_93 >= (max (last_1_var_1_58 , last_1_var_1_67))) ? (((last_1_var_1_82 == (last_1_var_1_56 / var_1_48)) && ((last_1_var_1_60 > last_1_var_1_67) || var_1_34)) ? (last_1_var_1_70 ? (var_1_82 == ((signed long int) (min ((min (last_1_var_1_36 , last_1_var_1_93)) , last_1_var_1_89)))) : (var_1_82 == ((signed long int) last_1_var_1_90))) : (var_1_82 == ((signed long int) (last_1_var_1_51 - last_1_var_1_36)))) : (var_1_82 == ((signed long int) last_1_var_1_87)))) && ((var_1_93 <= var_1_60) ? (((var_1_2 + 3.4f) > 8.25f) ? (var_1_84 == ((unsigned short int) var_1_42)) : 1) : (var_1_84 == ((unsigned short int) (max (((max (var_1_16 , var_1_86)) - var_1_61) , (min (var_1_20 , var_1_100)))))))) && (((-0.8 / var_1_77) >= var_1_3) ? ((last_1_var_1_92 == last_1_var_1_90) ? (var_1_87 == ((unsigned char) var_1_44)) : (var_1_87 == ((unsigned char) (min ((max ((var_1_20 + var_1_88) , var_1_24)) , var_1_57))))) : (var_1_87 == ((unsigned char) (min (var_1_19 , var_1_57)))))) && (((var_1_27 / var_1_77) > (var_1_28 - (var_1_30 + var_1_29))) ? (((var_1_55 * 7.8f) < ((- var_1_29) / var_1_77)) ? (var_1_89 == ((signed char) var_1_57)) : (var_1_89 == ((signed char) var_1_25))) : 1)) && (var_1_75 ? (var_1_90 == ((unsigned short int) var_1_24)) : (var_1_90 == ((unsigned short int) 32)))) && (var_1_91 == ((unsigned long int) var_1_100))) && (var_1_75 ? (var_1_92 == ((signed long int) var_1_87)) : (var_1_92 == ((signed long int) var_1_10)))) && (var_1_41 ? (var_1_93 == ((signed short int) var_1_25)) : 1)) && (var_1_71 ? (var_1_94 == ((signed short int) var_1_93)) : (var_1_94 == ((signed short int) var_1_20)))) && (last_1_var_1_32 ? (var_1_95 == ((signed char) var_1_20)) : (var_1_95 == ((signed char) var_1_25)))) && (var_1_35 ? (var_1_96 == ((signed long int) var_1_93)) : (var_1_96 == ((signed long int) 8)))) && (var_1_97 == ((double) var_1_66))) && (var_1_98 == ((signed long int) var_1_45))) && (var_1_99 == ((float) var_1_31))) && (last_1_var_1_79 ? (var_1_100 == ((unsigned char) var_1_20)) : 1)) && (var_1_40 ? (var_1_101 == ((double) var_1_64)) : (var_1_101 == ((double) var_1_66)))) && (((var_1_42 * var_1_87) >= var_1_21) ? (var_1_102 == ((unsigned char) (((var_1_84 < var_1_94) || var_1_33) && (var_1_34 && var_1_103)))) : (var_1_102 == ((unsigned char) var_1_33))) ; } int main(void) { isInitial = 1; initially(); while (1) { updateLastVariables(); updateVariables(); step(); __VERIFIER_assert(property()); isInitial = 0; } return 0; }