// 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_Batch16Amount500.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 short int var_1_1 = 2; float var_1_9 = 1.75; float var_1_12 = 2.125; float var_1_13 = 63.375; unsigned short int var_1_14 = 10; unsigned short int var_1_15 = 50820; unsigned long int var_1_16 = 1940175438; unsigned long int var_1_17 = 2058630425; unsigned short int var_1_20 = 41527; signed long int var_1_21 = -10; double var_1_22 = 127.1; double var_1_23 = 15.8; double var_1_24 = 63.2; signed long int var_1_26 = 0; signed long int var_1_28 = 1895511932; unsigned long int var_1_29 = 256; signed char var_1_31 = 4; signed long int var_1_32 = 10000; signed long int var_1_34 = 1744455711; unsigned short int var_1_35 = 16; double var_1_36 = 63.4; double var_1_37 = 50.4; double var_1_38 = 15.75; double var_1_39 = 499.25; double var_1_40 = 9.75; signed long int var_1_42 = -2; double var_1_43 = 0.0; double var_1_44 = 32.5; double var_1_45 = 128.2; unsigned short int var_1_46 = 4; unsigned char var_1_47 = 2; unsigned char var_1_48 = 200; unsigned char var_1_49 = 128; unsigned char var_1_50 = 10; float var_1_51 = 10.25; unsigned char var_1_52 = 4; unsigned char var_1_53 = 100; unsigned char var_1_54 = 100; unsigned char var_1_55 = 8; signed char var_1_56 = 4; signed char var_1_57 = 10; double var_1_58 = 10.5; signed char var_1_61 = 0; signed char var_1_62 = -50; signed char var_1_63 = 4; double var_1_64 = 5.5; unsigned char var_1_65 = 1; unsigned char var_1_66 = 0; float var_1_67 = 32.8; float var_1_68 = 7.5; unsigned char var_1_69 = 2; signed short int var_1_70 = 50; unsigned char var_1_72 = 0; signed short int var_1_73 = 256; unsigned short int var_1_75 = 16; unsigned short int var_1_76 = 32185; unsigned short int var_1_77 = 1; unsigned char var_1_78 = 100; signed long int var_1_79 = 10; unsigned long int var_1_80 = 2; unsigned long int var_1_82 = 3719526583; unsigned char var_1_83 = 1; unsigned char var_1_84 = 0; unsigned char var_1_85 = 0; unsigned char var_1_86 = 1; unsigned char var_1_87 = 1; unsigned char var_1_88 = 0; unsigned char var_1_89 = 1; unsigned char var_1_91 = 0; unsigned char var_1_92 = 0; unsigned short int var_1_94 = 10; double var_1_97 = 4.3; unsigned char var_1_98 = 0; signed long int var_1_99 = -2; signed char var_1_101 = -25; double var_1_102 = 0.0; signed char var_1_103 = 0; signed char var_1_104 = -5; signed char var_1_105 = 100; signed short int var_1_106 = 25; signed char var_1_108 = -16; unsigned short int var_1_109 = 4; signed char var_1_110 = 10; signed char var_1_111 = 1; signed char var_1_112 = -25; float var_1_113 = 32.2; float var_1_114 = 4.8; unsigned short int var_1_115 = 128; float var_1_116 = 255.125; unsigned char var_1_117 = 0; unsigned char var_1_118 = 0; unsigned long int var_1_119 = 256; signed long int var_1_120 = 10; signed long int var_1_121 = -16; unsigned short int var_1_122 = 5; unsigned long int var_1_123 = 500; unsigned short int var_1_124 = 32; unsigned char var_1_125 = 64; unsigned char var_1_126 = 1; signed char var_1_127 = -16; unsigned char var_1_128 = 1; // Calibration values // Last'ed variables unsigned short int last_1_var_1_14 = 10; unsigned long int last_1_var_1_29 = 256; signed long int last_1_var_1_32 = 10000; double last_1_var_1_40 = 9.75; unsigned char last_1_var_1_47 = 2; float last_1_var_1_51 = 10.25; unsigned char last_1_var_1_52 = 4; signed char last_1_var_1_56 = 4; double last_1_var_1_58 = 10.5; signed char last_1_var_1_61 = 0; double last_1_var_1_64 = 5.5; float last_1_var_1_67 = 32.8; unsigned char last_1_var_1_72 = 0; unsigned short int last_1_var_1_77 = 1; signed long int last_1_var_1_79 = 10; unsigned long int last_1_var_1_80 = 2; unsigned char last_1_var_1_83 = 1; unsigned char last_1_var_1_91 = 0; unsigned short int last_1_var_1_94 = 10; unsigned char last_1_var_1_98 = 0; signed short int last_1_var_1_106 = 25; unsigned short int last_1_var_1_109 = 4; float last_1_var_1_114 = 4.8; unsigned short int last_1_var_1_115 = 128; unsigned long int last_1_var_1_119 = 256; signed long int last_1_var_1_121 = -16; unsigned char last_1_var_1_125 = 64; unsigned char last_1_var_1_126 = 1; signed char last_1_var_1_127 = -16; // Additional functions void initially(void) { } void step(void) { // From: Req43Batch16Amount500 if (var_1_66) { if ((last_1_var_1_119 * (last_1_var_1_106 | -10)) > last_1_var_1_29) { var_1_113 = (max (var_1_38 , var_1_23)); } else { var_1_113 = ((max (var_1_45 , var_1_44)) + var_1_38); } } else { if ((var_1_43 * (- last_1_var_1_58)) == (last_1_var_1_67 / (abs (15.25)))) { var_1_113 = (var_1_37 - var_1_45); } } // From: Req13Batch16Amount500 if ((last_1_var_1_114 / var_1_43) >= last_1_var_1_58) { if ((var_1_20 >= last_1_var_1_47) || last_1_var_1_83) { var_1_51 = (abs (abs (var_1_38))); } } else { var_1_51 = ((max (var_1_12 , (var_1_43 - var_1_37))) - (max (var_1_24 , var_1_13))); } // From: Req58Batch16Amount500 signed long int stepLocal_21 = last_1_var_1_32; if ((last_1_var_1_80 * (last_1_var_1_121 / var_1_15)) >= stepLocal_21) { if (! last_1_var_1_91) { var_1_128 = (var_1_66 || (var_1_88 || var_1_92)); } else { var_1_128 = 0; } } else { var_1_128 = var_1_88; } // From: Req21Batch16Amount500 if (var_1_128) { var_1_69 = var_1_48; } // From: Req51Batch16Amount500 if (var_1_84) { var_1_121 = var_1_69; } // From: Req32Batch16Amount500 if (var_1_85) { if (last_1_var_1_127 == var_1_54) { var_1_89 = (! var_1_86); } } else { if ((max ((last_1_var_1_115 & var_1_53) , last_1_var_1_125)) >= last_1_var_1_98) { var_1_89 = (var_1_84 && var_1_86); } } // From: Req19Batch16Amount500 if (var_1_89) { var_1_65 = var_1_66; } // From: Req45Batch16Amount500 if (var_1_128) { var_1_115 = var_1_76; } else { var_1_115 = var_1_63; } // From: Req16Batch16Amount500 if (last_1_var_1_51 >= (last_1_var_1_64 + last_1_var_1_58)) { var_1_58 = var_1_24; } else { if ((max (var_1_15 , last_1_var_1_52)) > (min (var_1_31 , (max (last_1_var_1_14 , 100))))) { var_1_58 = (max (var_1_12 , (min ((min (64.8 , var_1_37)) , (min (var_1_23 , var_1_45)))))); } else { var_1_58 = ((var_1_43 - (var_1_45 + var_1_44)) - var_1_23); } } // From: Req57Batch16Amount500 if (last_1_var_1_83) { var_1_127 = var_1_104; } else { var_1_127 = var_1_63; } // From: Req48Batch16Amount500 if (var_1_65) { var_1_118 = var_1_63; } // From: Req7Batch16Amount500 signed long int stepLocal_3 = last_1_var_1_47; signed long int stepLocal_2 = last_1_var_1_126 / var_1_15; if (stepLocal_3 == ((last_1_var_1_56 & last_1_var_1_32) + last_1_var_1_32)) { if (stepLocal_2 < var_1_16) { var_1_32 = (((max (var_1_28 , var_1_34)) - var_1_20) - last_1_var_1_47); } } // From: Req12Batch16Amount500 if (last_1_var_1_72) { if (var_1_24 > (var_1_45 / var_1_43)) { var_1_47 = var_1_48; } else { var_1_47 = (var_1_49 - var_1_50); } } else { var_1_47 = var_1_48; } // From: Req50Batch16Amount500 if (var_1_88) { var_1_120 = var_1_47; } // From: Req9Batch16Amount500 if (var_1_23 <= (- (var_1_24 - var_1_22))) { var_1_36 = var_1_22; } else { var_1_36 = (max (((var_1_37 - var_1_38) + (10.25 + var_1_39)) , var_1_13)); } // From: Req27Batch16Amount500 var_1_78 = (var_1_49 - (min (var_1_53 , var_1_55))); // From: Req35Batch16Amount500 var_1_97 = (var_1_23 - (var_1_38 + (abs (var_1_44)))); // From: Req40Batch16Amount500 var_1_108 = ((max ((25 - var_1_55) , -50)) + (10 - var_1_103)); // From: Req41Batch16Amount500 if ((var_1_49 - (min (var_1_53 , var_1_105))) >= last_1_var_1_109) { var_1_109 = var_1_20; } // From: Req47Batch16Amount500 if (var_1_86) { var_1_117 = var_1_84; } else { var_1_117 = var_1_66; } // From: Req49Batch16Amount500 var_1_119 = var_1_103; // From: Req53Batch16Amount500 var_1_123 = var_1_119; // From: Req54Batch16Amount500 var_1_124 = var_1_53; // From: Req55Batch16Amount500 var_1_125 = var_1_54; // From: Req56Batch16Amount500 if (var_1_117) { var_1_126 = 1; } else { var_1_126 = var_1_48; } // From: Req38Batch16Amount500 signed long int stepLocal_16 = var_1_53 - var_1_54; if (var_1_51 > ((var_1_102 - var_1_23) - var_1_43)) { var_1_101 = (min (var_1_57 , ((var_1_55 - var_1_103) + var_1_104))); } else { if ((var_1_68 + var_1_43) > var_1_113) { if (stepLocal_16 <= (var_1_108 - (var_1_124 + var_1_125))) { var_1_101 = ((var_1_105 - var_1_103) - var_1_63); } } } // From: Req23Batch16Amount500 unsigned char stepLocal_10 = var_1_128; if (var_1_128 || stepLocal_10) { var_1_72 = var_1_66; } else { var_1_72 = (var_1_117 && var_1_66); } // From: Req15Batch16Amount500 if (! var_1_89) { var_1_56 = (max (var_1_55 , var_1_57)); } else { if (var_1_72) { var_1_56 = var_1_57; } else { var_1_56 = var_1_55; } } // From: Req11Batch16Amount500 if (var_1_65) { var_1_46 = (max (var_1_47 , var_1_20)); } // From: Req20Batch16Amount500 unsigned char stepLocal_8 = var_1_54; if ((99.2f / var_1_43) > last_1_var_1_67) { if ((var_1_46 >> var_1_124) >= stepLocal_8) { var_1_67 = (min (var_1_68 , var_1_12)); } else { var_1_67 = (abs (max (var_1_23 , var_1_44))); } } // From: Req44Batch16Amount500 signed char stepLocal_20 = var_1_56; if ((var_1_45 / var_1_43) == var_1_58) { if (var_1_127 > stepLocal_20) { var_1_114 = (min ((var_1_45 + var_1_39) , var_1_24)); } else { if (var_1_72) { var_1_114 = (max ((max (var_1_68 , var_1_44)) , 2.625f)); } } } // From: Req8Batch16Amount500 if (var_1_117) { var_1_35 = (max (var_1_118 , var_1_20)); } else { var_1_35 = var_1_20; } // From: Req2Batch16Amount500 if (var_1_108 <= ((min (var_1_118 , 16)) - var_1_118)) { var_1_9 = (var_1_12 - var_1_13); } else { var_1_9 = var_1_12; } // From: Req3Batch16Amount500 if ((var_1_32 + (var_1_15 - var_1_125)) >= ((var_1_16 + var_1_17) - (max (var_1_78 , var_1_46)))) { var_1_14 = var_1_125; } else { var_1_14 = (var_1_20 - (abs (2))); } // From: Req22Batch16Amount500 signed long int stepLocal_9 = var_1_28; if (stepLocal_9 >= (min (var_1_46 , var_1_125))) { var_1_70 = (max (var_1_49 , var_1_53)); } // From: Req36Batch16Amount500 if (var_1_123 <= var_1_32) { var_1_98 = var_1_50; } // From: Req18Batch16Amount500 unsigned short int stepLocal_7 = var_1_109; if (stepLocal_7 > (var_1_49 - (max (var_1_63 , var_1_55)))) { var_1_64 = (var_1_37 - var_1_12); } // From: Req46Batch16Amount500 if (var_1_117) { var_1_116 = var_1_44; } else { var_1_116 = var_1_23; } // From: Req52Batch16Amount500 if (var_1_66) { var_1_122 = var_1_124; } else { var_1_122 = var_1_76; } // From: Req33Batch16Amount500 if (var_1_36 <= var_1_67) { var_1_91 = (! ((var_1_88 || var_1_66) || var_1_92)); } else { if (var_1_89) { var_1_91 = ((var_1_76 <= var_1_28) && var_1_92); } } // From: Req28Batch16Amount500 if (var_1_109 == var_1_124) { if (var_1_63 >= (var_1_56 * (var_1_54 - 1))) { if (var_1_123 <= var_1_35) { var_1_79 = (max (last_1_var_1_79 , 10000)); } else { var_1_79 = (var_1_122 - 256); } } else { var_1_79 = (var_1_126 - var_1_109); } } else { var_1_79 = ((var_1_50 + var_1_20) + last_1_var_1_79); } // From: Req37Batch16Amount500 unsigned long int stepLocal_15 = (var_1_120 % var_1_34) * (min (4u , var_1_115)); signed long int stepLocal_14 = -64; if (stepLocal_14 > var_1_127) { if (! var_1_117) { if (((min (var_1_125 , var_1_32)) * var_1_35) > stepLocal_15) { var_1_99 = (max (var_1_78 , var_1_79)); } } else { var_1_99 = (var_1_54 + var_1_127); } } else { var_1_99 = (max (var_1_53 , (var_1_98 - var_1_125))); } // From: Req14Batch16Amount500 if (var_1_113 >= (31.5 / var_1_43)) { if (var_1_91) { var_1_52 = ((var_1_53 + (var_1_54 - var_1_55)) - var_1_50); } } // From: Req29Batch16Amount500 if (var_1_56 < var_1_98) { if (var_1_72 && var_1_91) { var_1_80 = (min ((var_1_82 - var_1_28) , var_1_54)); } else { var_1_80 = (var_1_98 + var_1_34); } } else { var_1_80 = (var_1_82 - var_1_20); } // From: Req1Batch16Amount500 unsigned long int stepLocal_0 = var_1_78 * (10u * var_1_69); if (var_1_99 >= stepLocal_0) { var_1_1 = ((var_1_127 + -25) + (min (var_1_125 , var_1_78))); } else { var_1_1 = (var_1_127 + (var_1_118 + -2)); } // From: Req6Batch16Amount500 if (var_1_70 <= ((-16 / var_1_31) & var_1_125)) { if (var_1_80 < var_1_125) { var_1_29 = (max ((var_1_47 + (1u + var_1_15)) , (min (10000u , (var_1_32 + var_1_17))))); } } // From: Req4Batch16Amount500 if ((var_1_12 - (9.3 + var_1_22)) < (var_1_13 - (var_1_23 + var_1_24))) { if (var_1_65) { var_1_21 = (min ((var_1_20 - var_1_120) , var_1_69)); } } else { var_1_21 = ((abs (var_1_52)) + var_1_108); } // From: Req25Batch16Amount500 if (var_1_117) { var_1_75 = (var_1_20 - (min (var_1_1 , (var_1_76 - var_1_55)))); } else { var_1_75 = (var_1_20 - ((min (var_1_119 , 5)) + var_1_121)); } // From: Req39Batch16Amount500 signed char stepLocal_18 = var_1_103; signed long int stepLocal_17 = var_1_53 + var_1_50; if (var_1_24 >= (var_1_12 / (min (2.75 , var_1_43)))) { if (var_1_75 != stepLocal_17) { var_1_106 = ((min (var_1_75 , (var_1_55 + var_1_50))) + (var_1_101 - var_1_105)); } else { var_1_106 = (var_1_69 - var_1_55); } } else { if (stepLocal_18 > var_1_105) { var_1_106 = (min (var_1_101 , var_1_69)); } else { var_1_106 = (var_1_54 - (var_1_103 + var_1_105)); } } // From: Req24Batch16Amount500 if ((var_1_51 + var_1_45) > (- (var_1_9 * var_1_58))) { if ((max (var_1_56 , var_1_120)) <= var_1_75) { var_1_73 = (max ((var_1_49 + var_1_1) , var_1_56)); } else { var_1_73 = (max ((4 + (max (var_1_62 , var_1_69))) , (var_1_115 + (max (var_1_125 , var_1_54))))); } } else { var_1_73 = (abs (var_1_47 + var_1_125)); } // From: Req34Batch16Amount500 signed long int stepLocal_13 = var_1_75 | var_1_121; if ((var_1_52 | last_1_var_1_94) <= stepLocal_13) { var_1_94 = (var_1_52 + (var_1_73 + var_1_63)); } else { if (((var_1_49 ^ last_1_var_1_94) % (var_1_82 - var_1_76)) < last_1_var_1_94) { var_1_94 = (var_1_52 + (var_1_55 + var_1_79)); } else { var_1_94 = (var_1_20 - (min ((var_1_76 - 10) , var_1_49))); } } // From: Req42Batch16Amount500 signed short int stepLocal_19 = var_1_106; if (var_1_128) { var_1_110 = ((min (var_1_103 , var_1_55)) + (max (var_1_104 , (max (var_1_111 , -4))))); } else { if (stepLocal_19 >= var_1_108) { var_1_110 = ((var_1_55 + var_1_112) + -8); } } // From: Req17Batch16Amount500 unsigned short int stepLocal_6 = var_1_94; if (last_1_var_1_61 <= stepLocal_6) { var_1_61 = ((max (var_1_55 , (abs (var_1_62)))) - var_1_63); } // From: Req5Batch16Amount500 unsigned char stepLocal_1 = var_1_125 == var_1_125; if (var_1_128) { if (stepLocal_1 && var_1_117) { var_1_26 = ((min ((max (var_1_61 , var_1_110)) , var_1_52)) + var_1_20); } else { var_1_26 = (var_1_20 - ((var_1_28 - var_1_80) - var_1_125)); } } else { var_1_26 = var_1_61; } // From: Req26Batch16Amount500 if (var_1_65) { if (var_1_110 > last_1_var_1_77) { var_1_77 = (var_1_20 - var_1_55); } else { var_1_77 = (var_1_110 + var_1_48); } } else { if ((32 % var_1_42) <= var_1_125) { var_1_77 = (var_1_20 - var_1_55); } else { var_1_77 = last_1_var_1_77; } } // From: Req31Batch16Amount500 if (var_1_26 >= ((- var_1_15) + var_1_14)) { var_1_87 = ((! (var_1_66 || var_1_86)) || var_1_88); } else { var_1_87 = var_1_85; } // From: Req30Batch16Amount500 signed long int stepLocal_12 = var_1_127 + var_1_61; unsigned char stepLocal_11 = var_1_31 > (var_1_125 / var_1_42); if ((-2 / -50) != stepLocal_12) { if (var_1_65) { var_1_83 = ((var_1_91 || var_1_84) && var_1_85); } else { var_1_83 = (var_1_89 || var_1_84); } } else { if (stepLocal_11 || ((min (var_1_121 , var_1_73)) > var_1_79)) { var_1_83 = ((var_1_84 || var_1_85) && var_1_86); } } // From: Req10Batch16Amount500 unsigned char stepLocal_5 = var_1_83; signed long int stepLocal_4 = (var_1_78 - var_1_47) % var_1_42; if (((last_1_var_1_40 < var_1_13) || var_1_72) || stepLocal_5) { var_1_40 = (abs (var_1_38)); } else { if (stepLocal_4 >= (var_1_15 * -1)) { if (var_1_72) { var_1_40 = (2.75 - (var_1_43 - (var_1_44 + var_1_45))); } else { var_1_40 = (var_1_39 + var_1_45); } } } } void updateVariables() { var_1_12 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_12 >= 0.0F && var_1_12 <= -1.0e-20F) || (var_1_12 <= 9223372.036854765600e+12F && var_1_12 >= 1.0e-20F )); var_1_13 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_13 >= 0.0F && var_1_13 <= -1.0e-20F) || (var_1_13 <= 9223372.036854765600e+12F && var_1_13 >= 1.0e-20F )); var_1_15 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_15 >= 32767); assume_abort_if_not(var_1_15 <= 65535); var_1_16 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_16 >= 1073741823); assume_abort_if_not(var_1_16 <= 2147483648); var_1_17 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_17 >= 1073741824); assume_abort_if_not(var_1_17 <= 2147483647); var_1_20 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_20 >= 32767); assume_abort_if_not(var_1_20 <= 65534); 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.018427387900e+12F && var_1_22 >= 1.0e-20F )); var_1_23 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_23 >= 0.0F && var_1_23 <= -1.0e-20F) || (var_1_23 <= 4611686.018427387900e+12F && var_1_23 >= 1.0e-20F )); var_1_24 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_24 >= 0.0F && var_1_24 <= -1.0e-20F) || (var_1_24 <= 4611686.018427387900e+12F && var_1_24 >= 1.0e-20F )); var_1_28 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_28 >= 1610612734); assume_abort_if_not(var_1_28 <= 2147483646); var_1_31 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_31 >= -128); assume_abort_if_not(var_1_31 <= 127); assume_abort_if_not(var_1_31 != 0); var_1_34 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_34 >= 1073741822); assume_abort_if_not(var_1_34 <= 2147483646); var_1_37 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_37 >= 0.0F && var_1_37 <= -1.0e-20F) || (var_1_37 <= 4611686.018427382800e+12F && var_1_37 >= 1.0e-20F )); var_1_38 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_38 >= 0.0F && var_1_38 <= -1.0e-20F) || (var_1_38 <= 4611686.018427382800e+12F && var_1_38 >= 1.0e-20F )); var_1_39 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_39 >= -230584.3009213691390e+13F && var_1_39 <= -1.0e-20F) || (var_1_39 <= 2305843.009213691390e+12F && var_1_39 >= 1.0e-20F )); var_1_42 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_42 >= -2147483648); assume_abort_if_not(var_1_42 <= 2147483647); assume_abort_if_not(var_1_42 != 0); var_1_43 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_43 >= 4611686.018427382800e+12F && var_1_43 <= -1.0e-20F) || (var_1_43 <= 9223372.036854765600e+12F && var_1_43 >= 1.0e-20F )); var_1_44 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_44 >= 0.0F && var_1_44 <= -1.0e-20F) || (var_1_44 <= 2305843.009213691390e+12F && var_1_44 >= 1.0e-20F )); var_1_45 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_45 >= 0.0F && var_1_45 <= -1.0e-20F) || (var_1_45 <= 2305843.009213691390e+12F && var_1_45 >= 1.0e-20F )); var_1_48 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_48 >= 0); assume_abort_if_not(var_1_48 <= 254); var_1_49 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_49 >= 127); assume_abort_if_not(var_1_49 <= 254); var_1_50 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_50 >= 0); assume_abort_if_not(var_1_50 <= 127); var_1_53 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_53 >= 63); assume_abort_if_not(var_1_53 <= 127); var_1_54 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_54 >= 95); assume_abort_if_not(var_1_54 <= 127); var_1_55 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_55 >= 0); assume_abort_if_not(var_1_55 <= 31); var_1_57 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_57 >= -127); assume_abort_if_not(var_1_57 <= 126); var_1_62 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_62 >= -126); assume_abort_if_not(var_1_62 <= 126); var_1_63 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_63 >= 0); assume_abort_if_not(var_1_63 <= 126); var_1_66 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_66 >= 0); assume_abort_if_not(var_1_66 <= 0); var_1_68 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_68 >= -922337.2036854765600e+13F && var_1_68 <= -1.0e-20F) || (var_1_68 <= 9223372.036854765600e+12F && var_1_68 >= 1.0e-20F )); var_1_76 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_76 >= 16383); assume_abort_if_not(var_1_76 <= 32767); var_1_82 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_82 >= 2147483647); assume_abort_if_not(var_1_82 <= 4294967294); var_1_84 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_84 >= 1); assume_abort_if_not(var_1_84 <= 1); var_1_85 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_85 >= 1); assume_abort_if_not(var_1_85 <= 1); var_1_86 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_86 >= 1); assume_abort_if_not(var_1_86 <= 1); var_1_88 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_88 >= 0); assume_abort_if_not(var_1_88 <= 0); var_1_92 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_92 >= 0); assume_abort_if_not(var_1_92 <= 0); var_1_102 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_102 >= 4611686.018427387900e+12F && var_1_102 <= -1.0e-20F) || (var_1_102 <= 9223372.036854776000e+12F && var_1_102 >= 1.0e-20F )); var_1_103 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_103 >= 0); assume_abort_if_not(var_1_103 <= 63); var_1_104 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_104 >= -63); assume_abort_if_not(var_1_104 <= 63); var_1_105 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_105 >= 62); assume_abort_if_not(var_1_105 <= 126); var_1_111 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_111 >= -63); assume_abort_if_not(var_1_111 <= 63); var_1_112 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_112 >= -31); assume_abort_if_not(var_1_112 <= 31); } void updateLastVariables() { last_1_var_1_14 = var_1_14; last_1_var_1_29 = var_1_29; last_1_var_1_32 = var_1_32; last_1_var_1_40 = var_1_40; last_1_var_1_47 = var_1_47; last_1_var_1_51 = var_1_51; last_1_var_1_52 = var_1_52; last_1_var_1_56 = var_1_56; last_1_var_1_58 = var_1_58; last_1_var_1_61 = var_1_61; last_1_var_1_64 = var_1_64; last_1_var_1_67 = var_1_67; last_1_var_1_72 = var_1_72; last_1_var_1_77 = var_1_77; last_1_var_1_79 = var_1_79; last_1_var_1_80 = var_1_80; last_1_var_1_83 = var_1_83; last_1_var_1_91 = var_1_91; last_1_var_1_94 = var_1_94; last_1_var_1_98 = var_1_98; last_1_var_1_106 = var_1_106; last_1_var_1_109 = var_1_109; last_1_var_1_114 = var_1_114; last_1_var_1_115 = var_1_115; last_1_var_1_119 = var_1_119; last_1_var_1_121 = var_1_121; last_1_var_1_125 = var_1_125; last_1_var_1_126 = var_1_126; last_1_var_1_127 = var_1_127; } int property() { return ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((var_1_99 >= (var_1_78 * (10u * var_1_69))) ? (var_1_1 == ((signed short int) ((var_1_127 + -25) + (min (var_1_125 , var_1_78))))) : (var_1_1 == ((signed short int) (var_1_127 + (var_1_118 + -2))))) && ((var_1_108 <= ((min (var_1_118 , 16)) - var_1_118)) ? (var_1_9 == ((float) (var_1_12 - var_1_13))) : (var_1_9 == ((float) var_1_12)))) && (((var_1_32 + (var_1_15 - var_1_125)) >= ((var_1_16 + var_1_17) - (max (var_1_78 , var_1_46)))) ? (var_1_14 == ((unsigned short int) var_1_125)) : (var_1_14 == ((unsigned short int) (var_1_20 - (abs (2))))))) && (((var_1_12 - (9.3 + var_1_22)) < (var_1_13 - (var_1_23 + var_1_24))) ? (var_1_65 ? (var_1_21 == ((signed long int) (min ((var_1_20 - var_1_120) , var_1_69)))) : 1) : (var_1_21 == ((signed long int) ((abs (var_1_52)) + var_1_108))))) && (var_1_128 ? (((var_1_125 == var_1_125) && var_1_117) ? (var_1_26 == ((signed long int) ((min ((max (var_1_61 , var_1_110)) , var_1_52)) + var_1_20))) : (var_1_26 == ((signed long int) (var_1_20 - ((var_1_28 - var_1_80) - var_1_125))))) : (var_1_26 == ((signed long int) var_1_61)))) && ((var_1_70 <= ((-16 / var_1_31) & var_1_125)) ? ((var_1_80 < var_1_125) ? (var_1_29 == ((unsigned long int) (max ((var_1_47 + (1u + var_1_15)) , (min (10000u , (var_1_32 + var_1_17))))))) : 1) : 1)) && ((last_1_var_1_47 == ((last_1_var_1_56 & last_1_var_1_32) + last_1_var_1_32)) ? (((last_1_var_1_126 / var_1_15) < var_1_16) ? (var_1_32 == ((signed long int) (((max (var_1_28 , var_1_34)) - var_1_20) - last_1_var_1_47))) : 1) : 1)) && (var_1_117 ? (var_1_35 == ((unsigned short int) (max (var_1_118 , var_1_20)))) : (var_1_35 == ((unsigned short int) var_1_20)))) && ((var_1_23 <= (- (var_1_24 - var_1_22))) ? (var_1_36 == ((double) var_1_22)) : (var_1_36 == ((double) (max (((var_1_37 - var_1_38) + (10.25 + var_1_39)) , var_1_13)))))) && ((((last_1_var_1_40 < var_1_13) || var_1_72) || var_1_83) ? (var_1_40 == ((double) (abs (var_1_38)))) : ((((var_1_78 - var_1_47) % var_1_42) >= (var_1_15 * -1)) ? (var_1_72 ? (var_1_40 == ((double) (2.75 - (var_1_43 - (var_1_44 + var_1_45))))) : (var_1_40 == ((double) (var_1_39 + var_1_45)))) : 1))) && (var_1_65 ? (var_1_46 == ((unsigned short int) (max (var_1_47 , var_1_20)))) : 1)) && (last_1_var_1_72 ? ((var_1_24 > (var_1_45 / var_1_43)) ? (var_1_47 == ((unsigned char) var_1_48)) : (var_1_47 == ((unsigned char) (var_1_49 - var_1_50)))) : (var_1_47 == ((unsigned char) var_1_48)))) && (((last_1_var_1_114 / var_1_43) >= last_1_var_1_58) ? (((var_1_20 >= last_1_var_1_47) || last_1_var_1_83) ? (var_1_51 == ((float) (abs (abs (var_1_38))))) : 1) : (var_1_51 == ((float) ((max (var_1_12 , (var_1_43 - var_1_37))) - (max (var_1_24 , var_1_13))))))) && ((var_1_113 >= (31.5 / var_1_43)) ? (var_1_91 ? (var_1_52 == ((unsigned char) ((var_1_53 + (var_1_54 - var_1_55)) - var_1_50))) : 1) : 1)) && ((! var_1_89) ? (var_1_56 == ((signed char) (max (var_1_55 , var_1_57)))) : (var_1_72 ? (var_1_56 == ((signed char) var_1_57)) : (var_1_56 == ((signed char) var_1_55))))) && ((last_1_var_1_51 >= (last_1_var_1_64 + last_1_var_1_58)) ? (var_1_58 == ((double) var_1_24)) : (((max (var_1_15 , last_1_var_1_52)) > (min (var_1_31 , (max (last_1_var_1_14 , 100))))) ? (var_1_58 == ((double) (max (var_1_12 , (min ((min (64.8 , var_1_37)) , (min (var_1_23 , var_1_45)))))))) : (var_1_58 == ((double) ((var_1_43 - (var_1_45 + var_1_44)) - var_1_23)))))) && ((last_1_var_1_61 <= var_1_94) ? (var_1_61 == ((signed char) ((max (var_1_55 , (abs (var_1_62)))) - var_1_63))) : 1)) && ((var_1_109 > (var_1_49 - (max (var_1_63 , var_1_55)))) ? (var_1_64 == ((double) (var_1_37 - var_1_12))) : 1)) && (var_1_89 ? (var_1_65 == ((unsigned char) var_1_66)) : 1)) && (((99.2f / var_1_43) > last_1_var_1_67) ? (((var_1_46 >> var_1_124) >= var_1_54) ? (var_1_67 == ((float) (min (var_1_68 , var_1_12)))) : (var_1_67 == ((float) (abs (max (var_1_23 , var_1_44)))))) : 1)) && (var_1_128 ? (var_1_69 == ((unsigned char) var_1_48)) : 1)) && ((var_1_28 >= (min (var_1_46 , var_1_125))) ? (var_1_70 == ((signed short int) (max (var_1_49 , var_1_53)))) : 1)) && ((var_1_128 || var_1_128) ? (var_1_72 == ((unsigned char) var_1_66)) : (var_1_72 == ((unsigned char) (var_1_117 && var_1_66))))) && (((var_1_51 + var_1_45) > (- (var_1_9 * var_1_58))) ? (((max (var_1_56 , var_1_120)) <= var_1_75) ? (var_1_73 == ((signed short int) (max ((var_1_49 + var_1_1) , var_1_56)))) : (var_1_73 == ((signed short int) (max ((4 + (max (var_1_62 , var_1_69))) , (var_1_115 + (max (var_1_125 , var_1_54)))))))) : (var_1_73 == ((signed short int) (abs (var_1_47 + var_1_125)))))) && (var_1_117 ? (var_1_75 == ((unsigned short int) (var_1_20 - (min (var_1_1 , (var_1_76 - var_1_55)))))) : (var_1_75 == ((unsigned short int) (var_1_20 - ((min (var_1_119 , 5)) + var_1_121)))))) && (var_1_65 ? ((var_1_110 > last_1_var_1_77) ? (var_1_77 == ((unsigned short int) (var_1_20 - var_1_55))) : (var_1_77 == ((unsigned short int) (var_1_110 + var_1_48)))) : (((32 % var_1_42) <= var_1_125) ? (var_1_77 == ((unsigned short int) (var_1_20 - var_1_55))) : (var_1_77 == ((unsigned short int) last_1_var_1_77))))) && (var_1_78 == ((unsigned char) (var_1_49 - (min (var_1_53 , var_1_55)))))) && ((var_1_109 == var_1_124) ? ((var_1_63 >= (var_1_56 * (var_1_54 - 1))) ? ((var_1_123 <= var_1_35) ? (var_1_79 == ((signed long int) (max (last_1_var_1_79 , 10000)))) : (var_1_79 == ((signed long int) (var_1_122 - 256)))) : (var_1_79 == ((signed long int) (var_1_126 - var_1_109)))) : (var_1_79 == ((signed long int) ((var_1_50 + var_1_20) + last_1_var_1_79))))) && ((var_1_56 < var_1_98) ? ((var_1_72 && var_1_91) ? (var_1_80 == ((unsigned long int) (min ((var_1_82 - var_1_28) , var_1_54)))) : (var_1_80 == ((unsigned long int) (var_1_98 + var_1_34)))) : (var_1_80 == ((unsigned long int) (var_1_82 - var_1_20))))) && (((-2 / -50) != (var_1_127 + var_1_61)) ? (var_1_65 ? (var_1_83 == ((unsigned char) ((var_1_91 || var_1_84) && var_1_85))) : (var_1_83 == ((unsigned char) (var_1_89 || var_1_84)))) : (((var_1_31 > (var_1_125 / var_1_42)) || ((min (var_1_121 , var_1_73)) > var_1_79)) ? (var_1_83 == ((unsigned char) ((var_1_84 || var_1_85) && var_1_86))) : 1))) && ((var_1_26 >= ((- var_1_15) + var_1_14)) ? (var_1_87 == ((unsigned char) ((! (var_1_66 || var_1_86)) || var_1_88))) : (var_1_87 == ((unsigned char) var_1_85)))) && (var_1_85 ? ((last_1_var_1_127 == var_1_54) ? (var_1_89 == ((unsigned char) (! var_1_86))) : 1) : (((max ((last_1_var_1_115 & var_1_53) , last_1_var_1_125)) >= last_1_var_1_98) ? (var_1_89 == ((unsigned char) (var_1_84 && var_1_86))) : 1))) && ((var_1_36 <= var_1_67) ? (var_1_91 == ((unsigned char) (! ((var_1_88 || var_1_66) || var_1_92)))) : (var_1_89 ? (var_1_91 == ((unsigned char) ((var_1_76 <= var_1_28) && var_1_92))) : 1))) && (((var_1_52 | last_1_var_1_94) <= (var_1_75 | var_1_121)) ? (var_1_94 == ((unsigned short int) (var_1_52 + (var_1_73 + var_1_63)))) : ((((var_1_49 ^ last_1_var_1_94) % (var_1_82 - var_1_76)) < last_1_var_1_94) ? (var_1_94 == ((unsigned short int) (var_1_52 + (var_1_55 + var_1_79)))) : (var_1_94 == ((unsigned short int) (var_1_20 - (min ((var_1_76 - 10) , var_1_49)))))))) && (var_1_97 == ((double) (var_1_23 - (var_1_38 + (abs (var_1_44))))))) && ((var_1_123 <= var_1_32) ? (var_1_98 == ((unsigned char) var_1_50)) : 1)) && ((-64 > var_1_127) ? ((! var_1_117) ? ((((min (var_1_125 , var_1_32)) * var_1_35) > ((var_1_120 % var_1_34) * (min (4u , var_1_115)))) ? (var_1_99 == ((signed long int) (max (var_1_78 , var_1_79)))) : 1) : (var_1_99 == ((signed long int) (var_1_54 + var_1_127)))) : (var_1_99 == ((signed long int) (max (var_1_53 , (var_1_98 - var_1_125))))))) && ((var_1_51 > ((var_1_102 - var_1_23) - var_1_43)) ? (var_1_101 == ((signed char) (min (var_1_57 , ((var_1_55 - var_1_103) + var_1_104))))) : (((var_1_68 + var_1_43) > var_1_113) ? (((var_1_53 - var_1_54) <= (var_1_108 - (var_1_124 + var_1_125))) ? (var_1_101 == ((signed char) ((var_1_105 - var_1_103) - var_1_63))) : 1) : 1))) && ((var_1_24 >= (var_1_12 / (min (2.75 , var_1_43)))) ? ((var_1_75 != (var_1_53 + var_1_50)) ? (var_1_106 == ((signed short int) ((min (var_1_75 , (var_1_55 + var_1_50))) + (var_1_101 - var_1_105)))) : (var_1_106 == ((signed short int) (var_1_69 - var_1_55)))) : ((var_1_103 > var_1_105) ? (var_1_106 == ((signed short int) (min (var_1_101 , var_1_69)))) : (var_1_106 == ((signed short int) (var_1_54 - (var_1_103 + var_1_105))))))) && (var_1_108 == ((signed char) ((max ((25 - var_1_55) , -50)) + (10 - var_1_103))))) && (((var_1_49 - (min (var_1_53 , var_1_105))) >= last_1_var_1_109) ? (var_1_109 == ((unsigned short int) var_1_20)) : 1)) && (var_1_128 ? (var_1_110 == ((signed char) ((min (var_1_103 , var_1_55)) + (max (var_1_104 , (max (var_1_111 , -4))))))) : ((var_1_106 >= var_1_108) ? (var_1_110 == ((signed char) ((var_1_55 + var_1_112) + -8))) : 1))) && (var_1_66 ? (((last_1_var_1_119 * (last_1_var_1_106 | -10)) > last_1_var_1_29) ? (var_1_113 == ((float) (max (var_1_38 , var_1_23)))) : (var_1_113 == ((float) ((max (var_1_45 , var_1_44)) + var_1_38)))) : (((var_1_43 * (- last_1_var_1_58)) == (last_1_var_1_67 / (abs (15.25)))) ? (var_1_113 == ((float) (var_1_37 - var_1_45))) : 1))) && (((var_1_45 / var_1_43) == var_1_58) ? ((var_1_127 > var_1_56) ? (var_1_114 == ((float) (min ((var_1_45 + var_1_39) , var_1_24)))) : (var_1_72 ? (var_1_114 == ((float) (max ((max (var_1_68 , var_1_44)) , 2.625f)))) : 1)) : 1)) && (var_1_128 ? (var_1_115 == ((unsigned short int) var_1_76)) : (var_1_115 == ((unsigned short int) var_1_63)))) && (var_1_117 ? (var_1_116 == ((float) var_1_44)) : (var_1_116 == ((float) var_1_23)))) && (var_1_86 ? (var_1_117 == ((unsigned char) var_1_84)) : (var_1_117 == ((unsigned char) var_1_66)))) && (var_1_65 ? (var_1_118 == ((unsigned char) var_1_63)) : 1)) && (var_1_119 == ((unsigned long int) var_1_103))) && (var_1_88 ? (var_1_120 == ((signed long int) var_1_47)) : 1)) && (var_1_84 ? (var_1_121 == ((signed long int) var_1_69)) : 1)) && (var_1_66 ? (var_1_122 == ((unsigned short int) var_1_124)) : (var_1_122 == ((unsigned short int) var_1_76)))) && (var_1_123 == ((unsigned long int) var_1_119))) && (var_1_124 == ((unsigned short int) var_1_53))) && (var_1_125 == ((unsigned char) var_1_54))) && (var_1_117 ? (var_1_126 == ((unsigned char) 1)) : (var_1_126 == ((unsigned char) var_1_48)))) && (last_1_var_1_83 ? (var_1_127 == ((signed char) var_1_104)) : (var_1_127 == ((signed char) var_1_63)))) && (((last_1_var_1_80 * (last_1_var_1_121 / var_1_15)) >= last_1_var_1_32) ? ((! last_1_var_1_91) ? (var_1_128 == ((unsigned char) (var_1_66 || (var_1_88 || var_1_92)))) : (var_1_128 == ((unsigned char) 0))) : (var_1_128 == ((unsigned char) var_1_88))) ; } int main(void) { isInitial = 1; initially(); while (1) { updateLastVariables(); updateVariables(); step(); __VERIFIER_assert(property()); isInitial = 0; } return 0; }