// 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_Batch62Amount500.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 double var_1_1 = 32.2; double var_1_4 = 10000000.9; double var_1_5 = 32.46; double var_1_6 = 10000.6; unsigned long int var_1_7 = 128; unsigned long int var_1_9 = 3574816166; unsigned long int var_1_10 = 1286461316; double var_1_12 = -0.75; double var_1_13 = 127.875; double var_1_14 = 0.4; double var_1_15 = 255.125; double var_1_16 = 15.2; double var_1_17 = 4.4; double var_1_18 = 1.4; signed long int var_1_20 = 4; double var_1_21 = 0.0; double var_1_22 = 64.4; signed short int var_1_23 = 100; float var_1_25 = 256.5; unsigned char var_1_26 = 0; unsigned char var_1_27 = 0; unsigned char var_1_28 = 0; unsigned char var_1_29 = 0; double var_1_30 = 49.875; double var_1_31 = 31.625; unsigned long int var_1_32 = 1; double var_1_33 = 4.3; unsigned char var_1_35 = 0; unsigned char var_1_36 = 0; unsigned char var_1_37 = 1; signed char var_1_38 = 25; signed char var_1_40 = 8; signed char var_1_41 = -1; signed char var_1_42 = -5; signed long int var_1_43 = -1; unsigned char var_1_44 = 200; unsigned char var_1_45 = 4; unsigned char var_1_46 = 8; signed short int var_1_47 = 200; double var_1_48 = 256.25; double var_1_49 = 4.4; double var_1_50 = 49.8; signed long int var_1_51 = 5; signed char var_1_52 = -32; double var_1_53 = 0.75; unsigned short int var_1_54 = 32; unsigned short int var_1_55 = 49157; unsigned short int var_1_57 = 19530; signed char var_1_58 = 4; signed long int var_1_59 = -4; signed char var_1_60 = 5; signed char var_1_61 = 10; signed char var_1_62 = 8; signed char var_1_63 = 64; unsigned long int var_1_64 = 5; unsigned long int var_1_65 = 1000000000; unsigned long int var_1_66 = 1000000000; signed long int var_1_67 = 0; signed long int var_1_68 = 32; unsigned char var_1_69 = 1; unsigned char var_1_70 = 100; unsigned char var_1_71 = 8; unsigned char var_1_72 = 16; float var_1_73 = 63.5; signed long int var_1_74 = 4; unsigned char var_1_75 = 100; signed long int var_1_76 = 1231421306; unsigned long int var_1_77 = 16; signed char var_1_78 = -5; signed char var_1_79 = 8; signed char var_1_80 = 0; signed long int var_1_81 = 64; signed short int var_1_82 = 4; unsigned char var_1_83 = 0; unsigned char var_1_84 = 0; unsigned short int var_1_85 = 5; double var_1_86 = 7.7; unsigned char var_1_88 = 10; unsigned char var_1_89 = 128; unsigned char var_1_90 = 10; unsigned char var_1_91 = 128; unsigned long int var_1_92 = 1; signed short int var_1_93 = 1; signed short int var_1_94 = 17430; signed short int var_1_95 = 10; double var_1_97 = 8.05; signed long int var_1_98 = 100; signed long int var_1_100 = 1915818250; signed long int var_1_101 = 1750935421; unsigned char var_1_103 = 1; signed long int var_1_104 = -256; signed long int var_1_105 = 10; unsigned char var_1_107 = 16; unsigned long int var_1_108 = 1000000000; signed long int var_1_109 = -10000; unsigned char var_1_110 = 64; unsigned char var_1_111 = 4; signed short int var_1_112 = 10000; signed char var_1_113 = -8; unsigned long int var_1_114 = 8; signed char var_1_115 = 64; float var_1_116 = 15.8; float var_1_117 = 24.7; double var_1_118 = 100000000000.9; signed long int var_1_119 = 4; unsigned short int var_1_120 = 10; unsigned short int var_1_121 = 25; signed long int var_1_122 = 256; // Calibration values // Last'ed variables double last_1_var_1_18 = 1.4; signed short int last_1_var_1_23 = 100; unsigned char last_1_var_1_35 = 0; signed long int last_1_var_1_43 = -1; signed char last_1_var_1_52 = -32; unsigned short int last_1_var_1_54 = 32; signed long int last_1_var_1_59 = -4; signed long int last_1_var_1_68 = 32; unsigned char last_1_var_1_69 = 1; unsigned long int last_1_var_1_77 = 16; signed long int last_1_var_1_81 = 64; unsigned short int last_1_var_1_85 = 5; unsigned char last_1_var_1_90 = 10; unsigned long int last_1_var_1_92 = 1; signed short int last_1_var_1_93 = 1; unsigned char last_1_var_1_103 = 1; signed long int last_1_var_1_104 = -256; signed long int last_1_var_1_105 = 10; unsigned char last_1_var_1_110 = 64; unsigned char last_1_var_1_111 = 4; signed long int last_1_var_1_119 = 4; unsigned short int last_1_var_1_121 = 25; signed long int last_1_var_1_122 = 256; // Additional functions void initially(void) { } void step(void) { // From: Req25Batch62Amount500 unsigned long int stepLocal_10 = var_1_9 * last_1_var_1_54; signed long int stepLocal_9 = last_1_var_1_90; signed long int stepLocal_8 = var_1_46 - var_1_62; signed long int stepLocal_7 = var_1_46 - var_1_61; if (! var_1_37) { var_1_69 = ((var_1_70 - var_1_61) + (max (var_1_46 , (max (64 , var_1_45))))); } else { if ((max (last_1_var_1_69 , var_1_44)) == stepLocal_10) { if (stepLocal_8 >= last_1_var_1_69) { var_1_69 = var_1_46; } else { if (last_1_var_1_77 >= stepLocal_7) { var_1_69 = (abs (var_1_45)); } } } else { if ((last_1_var_1_69 | (4 / var_1_20)) > stepLocal_9) { var_1_69 = (min (var_1_45 , var_1_46)); } else { var_1_69 = (var_1_62 + (var_1_70 - (var_1_71 + var_1_72))); } } } // From: Req46Batch62Amount500 var_1_109 = var_1_69; // From: Req34Batch62Amount500 signed long int stepLocal_18 = last_1_var_1_119; if (stepLocal_18 > var_1_10) { var_1_88 = (min ((var_1_89 - var_1_80) , ((var_1_70 - var_1_62) + var_1_75))); } else { if ((last_1_var_1_18 + var_1_4) != (- var_1_33)) { var_1_88 = (min ((var_1_71 + var_1_80) , var_1_75)); } } // From: Req6Batch62Amount500 if (((25u * last_1_var_1_85) * 5u) > (last_1_var_1_92 + var_1_20)) { var_1_25 = var_1_17; } // From: Req38Batch62Amount500 signed long int stepLocal_22 = 16 - (1668748462 - 32); if (var_1_33 >= 25.375) { if (stepLocal_22 != (~ (last_1_var_1_105 / var_1_44))) { var_1_95 = ((last_1_var_1_43 + var_1_45) - var_1_89); } else { var_1_95 = (var_1_91 + ((var_1_75 + var_1_46) - var_1_70)); } } else { if (var_1_86 < var_1_14) { var_1_95 = (((var_1_72 + last_1_var_1_111) + var_1_46) - var_1_79); } else { var_1_95 = -256; } } // From: Req2Batch62Amount500 signed long int stepLocal_2 = last_1_var_1_68 - last_1_var_1_111; signed long int stepLocal_1 = last_1_var_1_68; if (32 > stepLocal_1) { if ((- last_1_var_1_119) != stepLocal_2) { var_1_7 = (min ((min (5u , last_1_var_1_111)) , last_1_var_1_119)); } else { var_1_7 = (var_1_9 - 32u); } } else { var_1_7 = (min ((max (last_1_var_1_111 , (last_1_var_1_119 + last_1_var_1_68))) , (var_1_9 - (var_1_10 - last_1_var_1_90)))); } // From: Req30Batch62Amount500 unsigned long int stepLocal_14 = 1u; unsigned char stepLocal_13 = last_1_var_1_103; if (stepLocal_13 || (last_1_var_1_90 >= var_1_44)) { if ((last_1_var_1_110 ^ (var_1_75 / var_1_10)) <= stepLocal_14) { if (last_1_var_1_103) { var_1_81 = (last_1_var_1_121 - (abs (var_1_80 - last_1_var_1_90))); } } else { var_1_81 = (last_1_var_1_122 + var_1_75); } } else { if (last_1_var_1_35) { var_1_81 = ((5 + last_1_var_1_52) + var_1_46); } else { var_1_81 = (abs (last_1_var_1_81)); } } // From: Req32Batch62Amount500 signed long int stepLocal_17 = (last_1_var_1_54 / var_1_70) & last_1_var_1_59; signed long int stepLocal_16 = last_1_var_1_93; if (last_1_var_1_35) { if (! (var_1_44 <= 4)) { var_1_83 = ((var_1_36 && var_1_37) && ((last_1_var_1_54 >= last_1_var_1_23) || var_1_84)); } else { if (stepLocal_16 < (abs (1))) { if (last_1_var_1_81 > stepLocal_17) { var_1_83 = (! (var_1_27 && var_1_28)); } } else { var_1_83 = (! var_1_28); } } } // From: Req57Batch62Amount500 if (var_1_83) { var_1_121 = var_1_79; } // From: Req3Batch62Amount500 if ((min (var_1_4 , var_1_6)) <= (var_1_13 - var_1_14)) { var_1_12 = (var_1_15 - var_1_16); } else { var_1_12 = (max ((var_1_6 + var_1_5) , (var_1_4 + var_1_17))); } // From: Req7Batch62Amount500 var_1_26 = ((var_1_27 || var_1_28) || var_1_29); // From: Req8Batch62Amount500 if (var_1_13 < var_1_5) { var_1_30 = ((abs (var_1_31 + 256.6)) + var_1_22); } // From: Req10Batch62Amount500 var_1_35 = (var_1_36 && var_1_37); // From: Req13Batch62Amount500 var_1_47 = (min (-256 , (max (-64 , var_1_45)))); // From: Req15Batch62Amount500 if (var_1_27) { var_1_51 = var_1_46; } // From: Req16Batch62Amount500 var_1_52 = var_1_41; // From: Req21Batch62Amount500 var_1_60 = (min ((var_1_45 - 100) , ((var_1_61 + var_1_62) - var_1_63))); // From: Req22Batch62Amount500 var_1_64 = (((var_1_65 + var_1_66) - var_1_46) + var_1_62); // From: Req23Batch62Amount500 if ((max (var_1_5 , (var_1_14 - var_1_15))) < var_1_49) { var_1_67 = (max (5 , 100000)); } // From: Req26Batch62Amount500 if (var_1_33 < var_1_13) { var_1_73 = (var_1_4 + var_1_50); } else { var_1_73 = (abs (var_1_5)); } // From: Req29Batch62Amount500 signed long int stepLocal_12 = abs (var_1_20); if (var_1_28) { if (var_1_57 == stepLocal_12) { var_1_78 = (var_1_71 - var_1_72); } else { var_1_78 = ((var_1_71 + var_1_62) - (var_1_72 + (var_1_79 + var_1_80))); } } else { if (var_1_37) { var_1_78 = var_1_45; } else { var_1_78 = (min (var_1_63 , ((max (var_1_71 , var_1_79)) - var_1_45))); } } // From: Req39Batch62Amount500 if (var_1_28) { var_1_97 = (min (var_1_4 , (var_1_15 - (max (5.25 , var_1_22))))); } // From: Req44Batch62Amount500 if (var_1_37) { var_1_107 = var_1_70; } else { var_1_107 = var_1_91; } // From: Req47Batch62Amount500 var_1_110 = var_1_75; // From: Req48Batch62Amount500 if (var_1_26) { var_1_111 = var_1_71; } else { var_1_111 = var_1_89; } // From: Req49Batch62Amount500 var_1_112 = var_1_44; // From: Req50Batch62Amount500 var_1_113 = var_1_40; // From: Req51Batch62Amount500 var_1_114 = var_1_10; // From: Req52Batch62Amount500 var_1_115 = var_1_72; // From: Req53Batch62Amount500 if (var_1_37) { var_1_116 = var_1_17; } else { var_1_116 = var_1_117; } // From: Req54Batch62Amount500 if (var_1_26) { var_1_118 = var_1_86; } else { var_1_118 = 9.99999999999996E13; } // From: Req56Batch62Amount500 if (var_1_84) { var_1_120 = var_1_45; } else { var_1_120 = var_1_94; } // From: Req35Batch62Amount500 unsigned char stepLocal_19 = var_1_27 || (var_1_17 >= var_1_14); if ((var_1_109 != var_1_110) || stepLocal_19) { var_1_90 = var_1_91; } // From: Req33Batch62Amount500 if (((var_1_22 + var_1_86) - var_1_13) <= var_1_25) { if (var_1_115 != ((var_1_51 / 50) * var_1_45)) { var_1_85 = ((var_1_44 + (min (var_1_61 , var_1_115))) + var_1_79); } else { var_1_85 = (abs ((var_1_71 + var_1_70) + var_1_46)); } } else { if (var_1_83 && var_1_84) { var_1_85 = (var_1_115 + var_1_61); } else { var_1_85 = (min ((min ((var_1_55 - var_1_80) , var_1_61)) , var_1_70)); } } // From: Req31Batch62Amount500 signed long int stepLocal_15 = abs (var_1_57); if (! (var_1_30 > (min (var_1_25 , var_1_33)))) { if ((var_1_69 | var_1_81) > stepLocal_15) { if (! (var_1_63 >= var_1_72)) { var_1_82 = (5 + (max (var_1_80 , (var_1_79 + var_1_46)))); } } } // From: Req9Batch62Amount500 if ((var_1_21 / var_1_33) >= var_1_17) { var_1_32 = ((min (var_1_121 , var_1_111)) + var_1_111); } // From: Req5Batch62Amount500 if (var_1_107 != (var_1_20 * var_1_120)) { if (var_1_114 > var_1_9) { var_1_23 = (var_1_69 - 4); } } // From: Req18Batch62Amount500 if (var_1_46 >= var_1_111) { var_1_54 = (max (((var_1_55 - var_1_46) - var_1_45) , (var_1_44 + var_1_110))); } else { var_1_54 = ((var_1_57 - var_1_45) + var_1_44); } // From: Req19Batch62Amount500 if (var_1_118 < var_1_21) { var_1_58 = (abs (var_1_40)); } // From: Req20Batch62Amount500 var_1_59 = (var_1_55 + var_1_107); // From: Req27Batch62Amount500 signed long int stepLocal_11 = var_1_78 / (var_1_70 + var_1_75); if (stepLocal_11 < (min (var_1_10 , (256 + var_1_23)))) { var_1_74 = (max ((min ((var_1_111 - var_1_44) , var_1_57)) , var_1_41)); } // From: Req28Batch62Amount500 if (! (128 > var_1_62)) { var_1_77 = (min ((64u + (var_1_10 - var_1_63)) , var_1_110)); } // From: Req41Batch62Amount500 signed long int stepLocal_26 = var_1_74; if (stepLocal_26 < var_1_55) { var_1_103 = var_1_84; } // From: Req45Batch62Amount500 if (var_1_36) { var_1_108 = var_1_90; } // From: Req55Batch62Amount500 if (var_1_103) { var_1_119 = var_1_70; } else { var_1_119 = var_1_88; } // From: Req43Batch62Amount500 unsigned char stepLocal_29 = var_1_90; if (var_1_40 == stepLocal_29) { var_1_105 = (var_1_66 - (abs (var_1_70 + var_1_95))); } else { if (var_1_83) { var_1_105 = var_1_32; } } // From: Req40Batch62Amount500 unsigned short int stepLocal_25 = var_1_57; signed char stepLocal_24 = var_1_61; unsigned char stepLocal_23 = var_1_107 < var_1_78; if (stepLocal_24 > var_1_108) { if (stepLocal_23 || var_1_103) { if (var_1_69 >= stepLocal_25) { var_1_98 = (((var_1_100 - var_1_57) - (min (var_1_61 , var_1_75))) - (var_1_101 - (min (var_1_94 , var_1_63)))); } else { var_1_98 = var_1_70; } } else { var_1_98 = ((-32 + var_1_7) + var_1_113); } } // From: Req42Batch62Amount500 unsigned char stepLocal_28 = var_1_110; signed long int stepLocal_27 = var_1_95 + var_1_40; if (stepLocal_27 >= (var_1_61 - (1 + var_1_69))) { var_1_104 = (var_1_78 + ((1000000000 - var_1_94) - var_1_95)); } else { if ((last_1_var_1_104 / var_1_20) <= stepLocal_28) { var_1_104 = ((last_1_var_1_104 - var_1_54) + (var_1_46 - var_1_111)); } } // From: Req4Batch62Amount500 if (var_1_103) { if ((min (var_1_82 , var_1_77)) == (- (- var_1_9))) { if (((var_1_109 / var_1_10) / var_1_20) > var_1_9) { var_1_18 = (max (var_1_17 , 10.25)); } } else { var_1_18 = (min ((var_1_16 - (var_1_21 - var_1_22)) , var_1_4)); } } // From: Req36Batch62Amount500 signed char stepLocal_21 = var_1_62; unsigned char stepLocal_20 = var_1_37 || var_1_84; if (stepLocal_21 < ((-50 + var_1_60) ^ var_1_54)) { if (stepLocal_20 && (var_1_63 < (var_1_57 << var_1_89))) { var_1_92 = ((abs (1000000000u)) + (var_1_81 + (var_1_63 + var_1_70))); } else { var_1_92 = ((min (25u , var_1_76)) + var_1_69); } } else { var_1_92 = (max (var_1_44 , (min (var_1_91 , 100000u)))); } // From: Req14Batch62Amount500 signed long int stepLocal_6 = var_1_51; unsigned long int stepLocal_5 = var_1_85 * var_1_108; if (var_1_54 >= stepLocal_5) { var_1_48 = (var_1_31 + (max (var_1_17 , var_1_6))); } else { if (((var_1_54 & var_1_44) + var_1_108) >= stepLocal_6) { var_1_48 = (var_1_31 + (var_1_49 + var_1_50)); } else { var_1_48 = var_1_6; } } // From: Req17Batch62Amount500 if (! (var_1_77 < 100)) { if ((4.25 < var_1_6) || var_1_26) { var_1_53 = var_1_50; } else { var_1_53 = ((max (var_1_16 , (var_1_21 - var_1_22))) - var_1_15); } } // From: Req58Batch62Amount500 unsigned long int stepLocal_30 = var_1_9; if (! var_1_83) { if (var_1_36) { if (stepLocal_30 <= var_1_46) { var_1_122 = (max ((min (var_1_70 , (min (var_1_98 , var_1_46)))) , var_1_62)); } else { var_1_122 = var_1_91; } } else { var_1_122 = var_1_54; } } else { var_1_122 = var_1_46; } // From: Req1Batch62Amount500 signed long int stepLocal_0 = var_1_104; if (var_1_112 >= stepLocal_0) { var_1_1 = (abs ((max (var_1_4 , var_1_5)) + var_1_6)); } else { var_1_1 = (var_1_4 + var_1_5); } // From: Req12Batch62Amount500 unsigned char stepLocal_4 = var_1_88; signed long int stepLocal_3 = (var_1_44 - var_1_45) - var_1_46; if (var_1_28) { var_1_43 = (abs (var_1_42)); } else { if (stepLocal_3 <= var_1_88) { if (var_1_45 < stepLocal_4) { var_1_43 = (abs (var_1_122)); } } else { var_1_43 = ((1576379696 - (var_1_45 + 5)) - 100000); } } // From: Req24Batch62Amount500 if (var_1_61 > var_1_7) { if (var_1_42 <= var_1_113) { if ((min (var_1_31 , var_1_16)) != ((var_1_1 * var_1_118) + var_1_15)) { var_1_68 = last_1_var_1_68; } else { var_1_68 = (abs (var_1_51)); } } else { var_1_68 = var_1_55; } } // From: Req37Batch62Amount500 if (! var_1_27) { if (var_1_37) { var_1_93 = var_1_41; } else { if (var_1_54 < var_1_60) { if (var_1_73 < var_1_1) { var_1_93 = (min (((var_1_45 + var_1_89) - (var_1_94 - var_1_75)) , (min (last_1_var_1_93 , var_1_80)))); } else { var_1_93 = (var_1_79 + (var_1_91 + var_1_60)); } } else { var_1_93 = (max (var_1_71 , (var_1_89 - var_1_72))); } } } // From: Req11Batch62Amount500 if (var_1_37) { if (var_1_43 <= var_1_85) { var_1_38 = (abs (var_1_40)); } else { var_1_38 = (1 + (abs (1))); } } else { var_1_38 = (var_1_41 + var_1_42); } } void updateVariables() { var_1_4 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_4 >= -461168.6018427382800e+13F && var_1_4 <= -1.0e-20F) || (var_1_4 <= 4611686.018427382800e+12F && var_1_4 >= 1.0e-20F )); var_1_5 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_5 >= -461168.6018427382800e+13F && var_1_5 <= -1.0e-20F) || (var_1_5 <= 4611686.018427382800e+12F && var_1_5 >= 1.0e-20F )); var_1_6 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_6 >= -461168.6018427382800e+13F && var_1_6 <= -1.0e-20F) || (var_1_6 <= 4611686.018427382800e+12F && var_1_6 >= 1.0e-20F )); 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_13 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_13 >= 0.0F && var_1_13 <= -1.0e-20F) || (var_1_13 <= 9223372.036854776000e+12F && var_1_13 >= 1.0e-20F )); var_1_14 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_14 >= 0.0F && var_1_14 <= -1.0e-20F) || (var_1_14 <= 9223372.036854776000e+12F && var_1_14 >= 1.0e-20F )); var_1_15 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_15 >= 0.0F && var_1_15 <= -1.0e-20F) || (var_1_15 <= 9223372.036854765600e+12F && var_1_15 >= 1.0e-20F )); var_1_16 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_16 >= 0.0F && var_1_16 <= -1.0e-20F) || (var_1_16 <= 9223372.036854765600e+12F && var_1_16 >= 1.0e-20F )); var_1_17 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_17 >= -461168.6018427382800e+13F && var_1_17 <= -1.0e-20F) || (var_1_17 <= 4611686.018427382800e+12F && var_1_17 >= 1.0e-20F )); var_1_20 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_20 >= -2147483648); assume_abort_if_not(var_1_20 <= 2147483647); assume_abort_if_not(var_1_20 != 0); var_1_21 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_21 >= 4611686.018427382800e+12F && var_1_21 <= -1.0e-20F) || (var_1_21 <= 9223372.036854765600e+12F && var_1_21 >= 1.0e-20F )); var_1_22 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_22 >= 0.0F && var_1_22 <= -1.0e-20F) || (var_1_22 <= 4611686.018427382800e+12F && var_1_22 >= 1.0e-20F )); var_1_27 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_27 >= 0); assume_abort_if_not(var_1_27 <= 0); var_1_28 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_28 >= 0); assume_abort_if_not(var_1_28 <= 0); var_1_29 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_29 >= 0); assume_abort_if_not(var_1_29 <= 0); var_1_31 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_31 >= -230584.3009213691390e+13F && var_1_31 <= -1.0e-20F) || (var_1_31 <= 2305843.009213691390e+12F && var_1_31 >= 1.0e-20F )); var_1_33 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_33 >= -922337.2036854776000e+13F && var_1_33 <= -1.0e-20F) || (var_1_33 <= 9223372.036854776000e+12F && var_1_33 >= 1.0e-20F )); assume_abort_if_not(var_1_33 != 0.0F); var_1_36 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_36 >= 1); assume_abort_if_not(var_1_36 <= 1); var_1_37 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_37 >= 1); assume_abort_if_not(var_1_37 <= 1); var_1_40 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_40 >= -126); assume_abort_if_not(var_1_40 <= 126); var_1_41 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_41 >= -63); assume_abort_if_not(var_1_41 <= 63); var_1_42 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_42 >= -63); assume_abort_if_not(var_1_42 <= 63); var_1_44 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_44 >= 191); assume_abort_if_not(var_1_44 <= 255); var_1_45 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_45 >= 0); assume_abort_if_not(var_1_45 <= 64); var_1_46 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_46 >= 0); assume_abort_if_not(var_1_46 <= 127); var_1_49 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_49 >= -230584.3009213691390e+13F && var_1_49 <= -1.0e-20F) || (var_1_49 <= 2305843.009213691390e+12F && var_1_49 >= 1.0e-20F )); var_1_50 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_50 >= -230584.3009213691390e+13F && var_1_50 <= -1.0e-20F) || (var_1_50 <= 2305843.009213691390e+12F && var_1_50 >= 1.0e-20F )); var_1_55 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_55 >= 49150); assume_abort_if_not(var_1_55 <= 65534); var_1_57 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_57 >= 16383); assume_abort_if_not(var_1_57 <= 32767); var_1_61 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_61 >= 0); assume_abort_if_not(var_1_61 <= 63); var_1_62 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_62 >= 0); assume_abort_if_not(var_1_62 <= 63); var_1_63 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_63 >= 0); assume_abort_if_not(var_1_63 <= 126); var_1_65 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_65 >= 536870911); assume_abort_if_not(var_1_65 <= 1073741824); var_1_66 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_66 >= 536870912); assume_abort_if_not(var_1_66 <= 1073741823); var_1_70 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_70 >= 63); assume_abort_if_not(var_1_70 <= 127); var_1_71 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_71 >= 0); assume_abort_if_not(var_1_71 <= 32); var_1_72 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_72 >= 0); assume_abort_if_not(var_1_72 <= 31); var_1_75 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_75 >= 1); assume_abort_if_not(var_1_75 <= 127); var_1_76 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_76 >= 1073741822); assume_abort_if_not(var_1_76 <= 2147483646); var_1_79 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_79 >= 0); assume_abort_if_not(var_1_79 <= 32); var_1_80 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_80 >= 0); assume_abort_if_not(var_1_80 <= 31); var_1_84 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_84 >= 1); assume_abort_if_not(var_1_84 <= 1); var_1_86 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_86 >= 0.0F && var_1_86 <= -1.0e-20F) || (var_1_86 <= 4611686.018427387900e+12F && var_1_86 >= 1.0e-20F )); var_1_89 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_89 >= 127); assume_abort_if_not(var_1_89 <= 254); var_1_91 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_91 >= 0); assume_abort_if_not(var_1_91 <= 254); var_1_94 = __VERIFIER_nondet_short(); assume_abort_if_not(var_1_94 >= 16383); assume_abort_if_not(var_1_94 <= 32766); var_1_100 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_100 >= 1610612734); assume_abort_if_not(var_1_100 <= 2147483646); var_1_101 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_101 >= 1073741823); assume_abort_if_not(var_1_101 <= 2147483646); var_1_117 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_117 >= -922337.2036854765600e+13F && var_1_117 <= -1.0e-20F) || (var_1_117 <= 9223372.036854765600e+12F && var_1_117 >= 1.0e-20F )); } void updateLastVariables() { last_1_var_1_18 = var_1_18; last_1_var_1_23 = var_1_23; last_1_var_1_35 = var_1_35; last_1_var_1_43 = var_1_43; last_1_var_1_52 = var_1_52; last_1_var_1_54 = var_1_54; last_1_var_1_59 = var_1_59; last_1_var_1_68 = var_1_68; last_1_var_1_69 = var_1_69; last_1_var_1_77 = var_1_77; last_1_var_1_81 = var_1_81; last_1_var_1_85 = var_1_85; 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_103 = var_1_103; last_1_var_1_104 = var_1_104; last_1_var_1_105 = var_1_105; last_1_var_1_110 = var_1_110; last_1_var_1_111 = var_1_111; last_1_var_1_119 = var_1_119; last_1_var_1_121 = var_1_121; last_1_var_1_122 = var_1_122; } int property() { return ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((var_1_112 >= var_1_104) ? (var_1_1 == ((double) (abs ((max (var_1_4 , var_1_5)) + var_1_6)))) : (var_1_1 == ((double) (var_1_4 + var_1_5)))) && ((32 > last_1_var_1_68) ? (((- last_1_var_1_119) != (last_1_var_1_68 - last_1_var_1_111)) ? (var_1_7 == ((unsigned long int) (min ((min (5u , last_1_var_1_111)) , last_1_var_1_119)))) : (var_1_7 == ((unsigned long int) (var_1_9 - 32u)))) : (var_1_7 == ((unsigned long int) (min ((max (last_1_var_1_111 , (last_1_var_1_119 + last_1_var_1_68))) , (var_1_9 - (var_1_10 - last_1_var_1_90)))))))) && (((min (var_1_4 , var_1_6)) <= (var_1_13 - var_1_14)) ? (var_1_12 == ((double) (var_1_15 - var_1_16))) : (var_1_12 == ((double) (max ((var_1_6 + var_1_5) , (var_1_4 + var_1_17))))))) && (var_1_103 ? (((min (var_1_82 , var_1_77)) == (- (- var_1_9))) ? ((((var_1_109 / var_1_10) / var_1_20) > var_1_9) ? (var_1_18 == ((double) (max (var_1_17 , 10.25)))) : 1) : (var_1_18 == ((double) (min ((var_1_16 - (var_1_21 - var_1_22)) , var_1_4))))) : 1)) && ((var_1_107 != (var_1_20 * var_1_120)) ? ((var_1_114 > var_1_9) ? (var_1_23 == ((signed short int) (var_1_69 - 4))) : 1) : 1)) && ((((25u * last_1_var_1_85) * 5u) > (last_1_var_1_92 + var_1_20)) ? (var_1_25 == ((float) var_1_17)) : 1)) && (var_1_26 == ((unsigned char) ((var_1_27 || var_1_28) || var_1_29)))) && ((var_1_13 < var_1_5) ? (var_1_30 == ((double) ((abs (var_1_31 + 256.6)) + var_1_22))) : 1)) && (((var_1_21 / var_1_33) >= var_1_17) ? (var_1_32 == ((unsigned long int) ((min (var_1_121 , var_1_111)) + var_1_111))) : 1)) && (var_1_35 == ((unsigned char) (var_1_36 && var_1_37)))) && (var_1_37 ? ((var_1_43 <= var_1_85) ? (var_1_38 == ((signed char) (abs (var_1_40)))) : (var_1_38 == ((signed char) (1 + (abs (1)))))) : (var_1_38 == ((signed char) (var_1_41 + var_1_42))))) && (var_1_28 ? (var_1_43 == ((signed long int) (abs (var_1_42)))) : ((((var_1_44 - var_1_45) - var_1_46) <= var_1_88) ? ((var_1_45 < var_1_88) ? (var_1_43 == ((signed long int) (abs (var_1_122)))) : 1) : (var_1_43 == ((signed long int) ((1576379696 - (var_1_45 + 5)) - 100000)))))) && (var_1_47 == ((signed short int) (min (-256 , (max (-64 , var_1_45))))))) && ((var_1_54 >= (var_1_85 * var_1_108)) ? (var_1_48 == ((double) (var_1_31 + (max (var_1_17 , var_1_6))))) : ((((var_1_54 & var_1_44) + var_1_108) >= var_1_51) ? (var_1_48 == ((double) (var_1_31 + (var_1_49 + var_1_50)))) : (var_1_48 == ((double) var_1_6))))) && (var_1_27 ? (var_1_51 == ((signed long int) var_1_46)) : 1)) && (var_1_52 == ((signed char) var_1_41))) && ((! (var_1_77 < 100)) ? (((4.25 < var_1_6) || var_1_26) ? (var_1_53 == ((double) var_1_50)) : (var_1_53 == ((double) ((max (var_1_16 , (var_1_21 - var_1_22))) - var_1_15)))) : 1)) && ((var_1_46 >= var_1_111) ? (var_1_54 == ((unsigned short int) (max (((var_1_55 - var_1_46) - var_1_45) , (var_1_44 + var_1_110))))) : (var_1_54 == ((unsigned short int) ((var_1_57 - var_1_45) + var_1_44))))) && ((var_1_118 < var_1_21) ? (var_1_58 == ((signed char) (abs (var_1_40)))) : 1)) && (var_1_59 == ((signed long int) (var_1_55 + var_1_107)))) && (var_1_60 == ((signed char) (min ((var_1_45 - 100) , ((var_1_61 + var_1_62) - var_1_63)))))) && (var_1_64 == ((unsigned long int) (((var_1_65 + var_1_66) - var_1_46) + var_1_62)))) && (((max (var_1_5 , (var_1_14 - var_1_15))) < var_1_49) ? (var_1_67 == ((signed long int) (max (5 , 100000)))) : 1)) && ((var_1_61 > var_1_7) ? ((var_1_42 <= var_1_113) ? (((min (var_1_31 , var_1_16)) != ((var_1_1 * var_1_118) + var_1_15)) ? (var_1_68 == ((signed long int) last_1_var_1_68)) : (var_1_68 == ((signed long int) (abs (var_1_51))))) : (var_1_68 == ((signed long int) var_1_55))) : 1)) && ((! var_1_37) ? (var_1_69 == ((unsigned char) ((var_1_70 - var_1_61) + (max (var_1_46 , (max (64 , var_1_45))))))) : (((max (last_1_var_1_69 , var_1_44)) == (var_1_9 * last_1_var_1_54)) ? (((var_1_46 - var_1_62) >= last_1_var_1_69) ? (var_1_69 == ((unsigned char) var_1_46)) : ((last_1_var_1_77 >= (var_1_46 - var_1_61)) ? (var_1_69 == ((unsigned char) (abs (var_1_45)))) : 1)) : (((last_1_var_1_69 | (4 / var_1_20)) > last_1_var_1_90) ? (var_1_69 == ((unsigned char) (min (var_1_45 , var_1_46)))) : (var_1_69 == ((unsigned char) (var_1_62 + (var_1_70 - (var_1_71 + var_1_72))))))))) && ((var_1_33 < var_1_13) ? (var_1_73 == ((float) (var_1_4 + var_1_50))) : (var_1_73 == ((float) (abs (var_1_5)))))) && (((var_1_78 / (var_1_70 + var_1_75)) < (min (var_1_10 , (256 + var_1_23)))) ? (var_1_74 == ((signed long int) (max ((min ((var_1_111 - var_1_44) , var_1_57)) , var_1_41)))) : 1)) && ((! (128 > var_1_62)) ? (var_1_77 == ((unsigned long int) (min ((64u + (var_1_10 - var_1_63)) , var_1_110)))) : 1)) && (var_1_28 ? ((var_1_57 == (abs (var_1_20))) ? (var_1_78 == ((signed char) (var_1_71 - var_1_72))) : (var_1_78 == ((signed char) ((var_1_71 + var_1_62) - (var_1_72 + (var_1_79 + var_1_80)))))) : (var_1_37 ? (var_1_78 == ((signed char) var_1_45)) : (var_1_78 == ((signed char) (min (var_1_63 , ((max (var_1_71 , var_1_79)) - var_1_45)))))))) && ((last_1_var_1_103 || (last_1_var_1_90 >= var_1_44)) ? (((last_1_var_1_110 ^ (var_1_75 / var_1_10)) <= 1u) ? (last_1_var_1_103 ? (var_1_81 == ((signed long int) (last_1_var_1_121 - (abs (var_1_80 - last_1_var_1_90))))) : 1) : (var_1_81 == ((signed long int) (last_1_var_1_122 + var_1_75)))) : (last_1_var_1_35 ? (var_1_81 == ((signed long int) ((5 + last_1_var_1_52) + var_1_46))) : (var_1_81 == ((signed long int) (abs (last_1_var_1_81))))))) && ((! (var_1_30 > (min (var_1_25 , var_1_33)))) ? (((var_1_69 | var_1_81) > (abs (var_1_57))) ? ((! (var_1_63 >= var_1_72)) ? (var_1_82 == ((signed short int) (5 + (max (var_1_80 , (var_1_79 + var_1_46)))))) : 1) : 1) : 1)) && (last_1_var_1_35 ? ((! (var_1_44 <= 4)) ? (var_1_83 == ((unsigned char) ((var_1_36 && var_1_37) && ((last_1_var_1_54 >= last_1_var_1_23) || var_1_84)))) : ((last_1_var_1_93 < (abs (1))) ? ((last_1_var_1_81 > ((last_1_var_1_54 / var_1_70) & last_1_var_1_59)) ? (var_1_83 == ((unsigned char) (! (var_1_27 && var_1_28)))) : 1) : (var_1_83 == ((unsigned char) (! var_1_28))))) : 1)) && ((((var_1_22 + var_1_86) - var_1_13) <= var_1_25) ? ((var_1_115 != ((var_1_51 / 50) * var_1_45)) ? (var_1_85 == ((unsigned short int) ((var_1_44 + (min (var_1_61 , var_1_115))) + var_1_79))) : (var_1_85 == ((unsigned short int) (abs ((var_1_71 + var_1_70) + var_1_46))))) : ((var_1_83 && var_1_84) ? (var_1_85 == ((unsigned short int) (var_1_115 + var_1_61))) : (var_1_85 == ((unsigned short int) (min ((min ((var_1_55 - var_1_80) , var_1_61)) , var_1_70))))))) && ((last_1_var_1_119 > var_1_10) ? (var_1_88 == ((unsigned char) (min ((var_1_89 - var_1_80) , ((var_1_70 - var_1_62) + var_1_75))))) : (((last_1_var_1_18 + var_1_4) != (- var_1_33)) ? (var_1_88 == ((unsigned char) (min ((var_1_71 + var_1_80) , var_1_75)))) : 1))) && (((var_1_109 != var_1_110) || (var_1_27 || (var_1_17 >= var_1_14))) ? (var_1_90 == ((unsigned char) var_1_91)) : 1)) && ((var_1_62 < ((-50 + var_1_60) ^ var_1_54)) ? (((var_1_37 || var_1_84) && (var_1_63 < (var_1_57 << var_1_89))) ? (var_1_92 == ((unsigned long int) ((abs (1000000000u)) + (var_1_81 + (var_1_63 + var_1_70))))) : (var_1_92 == ((unsigned long int) ((min (25u , var_1_76)) + var_1_69)))) : (var_1_92 == ((unsigned long int) (max (var_1_44 , (min (var_1_91 , 100000u)))))))) && ((! var_1_27) ? (var_1_37 ? (var_1_93 == ((signed short int) var_1_41)) : ((var_1_54 < var_1_60) ? ((var_1_73 < var_1_1) ? (var_1_93 == ((signed short int) (min (((var_1_45 + var_1_89) - (var_1_94 - var_1_75)) , (min (last_1_var_1_93 , var_1_80)))))) : (var_1_93 == ((signed short int) (var_1_79 + (var_1_91 + var_1_60))))) : (var_1_93 == ((signed short int) (max (var_1_71 , (var_1_89 - var_1_72))))))) : 1)) && ((var_1_33 >= 25.375) ? (((16 - (1668748462 - 32)) != (~ (last_1_var_1_105 / var_1_44))) ? (var_1_95 == ((signed short int) ((last_1_var_1_43 + var_1_45) - var_1_89))) : (var_1_95 == ((signed short int) (var_1_91 + ((var_1_75 + var_1_46) - var_1_70))))) : ((var_1_86 < var_1_14) ? (var_1_95 == ((signed short int) (((var_1_72 + last_1_var_1_111) + var_1_46) - var_1_79))) : (var_1_95 == ((signed short int) -256))))) && (var_1_28 ? (var_1_97 == ((double) (min (var_1_4 , (var_1_15 - (max (5.25 , var_1_22))))))) : 1)) && ((var_1_61 > var_1_108) ? (((var_1_107 < var_1_78) || var_1_103) ? ((var_1_69 >= var_1_57) ? (var_1_98 == ((signed long int) (((var_1_100 - var_1_57) - (min (var_1_61 , var_1_75))) - (var_1_101 - (min (var_1_94 , var_1_63)))))) : (var_1_98 == ((signed long int) var_1_70))) : (var_1_98 == ((signed long int) ((-32 + var_1_7) + var_1_113)))) : 1)) && ((var_1_74 < var_1_55) ? (var_1_103 == ((unsigned char) var_1_84)) : 1)) && (((var_1_95 + var_1_40) >= (var_1_61 - (1 + var_1_69))) ? (var_1_104 == ((signed long int) (var_1_78 + ((1000000000 - var_1_94) - var_1_95)))) : (((last_1_var_1_104 / var_1_20) <= var_1_110) ? (var_1_104 == ((signed long int) ((last_1_var_1_104 - var_1_54) + (var_1_46 - var_1_111)))) : 1))) && ((var_1_40 == var_1_90) ? (var_1_105 == ((signed long int) (var_1_66 - (abs (var_1_70 + var_1_95))))) : (var_1_83 ? (var_1_105 == ((signed long int) var_1_32)) : 1))) && (var_1_37 ? (var_1_107 == ((unsigned char) var_1_70)) : (var_1_107 == ((unsigned char) var_1_91)))) && (var_1_36 ? (var_1_108 == ((unsigned long int) var_1_90)) : 1)) && (var_1_109 == ((signed long int) var_1_69))) && (var_1_110 == ((unsigned char) var_1_75))) && (var_1_26 ? (var_1_111 == ((unsigned char) var_1_71)) : (var_1_111 == ((unsigned char) var_1_89)))) && (var_1_112 == ((signed short int) var_1_44))) && (var_1_113 == ((signed char) var_1_40))) && (var_1_114 == ((unsigned long int) var_1_10))) && (var_1_115 == ((signed char) var_1_72))) && (var_1_37 ? (var_1_116 == ((float) var_1_17)) : (var_1_116 == ((float) var_1_117)))) && (var_1_26 ? (var_1_118 == ((double) var_1_86)) : (var_1_118 == ((double) 9.99999999999996E13)))) && (var_1_103 ? (var_1_119 == ((signed long int) var_1_70)) : (var_1_119 == ((signed long int) var_1_88)))) && (var_1_84 ? (var_1_120 == ((unsigned short int) var_1_45)) : (var_1_120 == ((unsigned short int) var_1_94)))) && (var_1_83 ? (var_1_121 == ((unsigned short int) var_1_79)) : 1)) && ((! var_1_83) ? (var_1_36 ? ((var_1_9 <= var_1_46) ? (var_1_122 == ((signed long int) (max ((min (var_1_70 , (min (var_1_98 , var_1_46)))) , var_1_62)))) : (var_1_122 == ((signed long int) var_1_91))) : (var_1_122 == ((signed long int) var_1_54))) : (var_1_122 == ((signed long int) var_1_46))) ; } int main(void) { isInitial = 1; initially(); while (1) { updateLastVariables(); updateVariables(); step(); __VERIFIER_assert(property()); isInitial = 0; } return 0; }