// 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_Batch57PS_CN_500.c", 13, "reach_error"); } void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } return; } void assume_abort_if_not(int cond) { if(!cond) { abort(); } } #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 unsigned char var_1_1 = 5; signed char var_1_2 = -1; signed char var_1_3 = 10; signed long int var_1_5 = 5; unsigned char var_1_6 = 0; double var_1_7 = 24.8; double var_1_8 = 500.5; double var_1_9 = 2.4; double var_1_10 = 0.4; double var_1_11 = 255.8; double var_1_12 = 50.75; unsigned char var_1_13 = 4; unsigned char var_1_14 = 200; unsigned char var_1_15 = 25; unsigned char var_1_16 = 128; unsigned char var_1_17 = 64; unsigned char var_1_18 = 32; unsigned char var_1_19 = 32; unsigned long int var_1_20 = 1; float var_1_21 = 9999999999.2; double var_1_23 = 10.875; unsigned char var_1_24 = 0; signed char var_1_25 = 64; signed char var_1_26 = -32; signed long int var_1_27 = 4; unsigned char var_1_28 = 0; unsigned long int var_1_29 = 2566817213; unsigned char var_1_30 = 0; unsigned char var_1_31 = 0; unsigned char var_1_32 = 0; unsigned char var_1_33 = 0; signed short int var_1_34 = -64; float var_1_35 = 1.8; signed short int var_1_36 = -16; unsigned char var_1_37 = 32; unsigned char var_1_38 = 50; unsigned char var_1_39 = 50; signed long int var_1_40 = -8; float var_1_41 = 0.875; double var_1_42 = 10.8; double var_1_43 = 15.5; float var_1_44 = 255.5; float var_1_45 = 0.75; float var_1_46 = 1.7; unsigned char var_1_47 = 25; unsigned char var_1_48 = 1; unsigned char var_1_49 = 8; unsigned char var_1_50 = 128; unsigned char var_1_51 = 16; unsigned short int var_1_52 = 256; unsigned short int var_1_53 = 5; float var_1_54 = 255.8; float var_1_55 = 499.4; float var_1_56 = 128.5; signed char var_1_57 = 0; signed char var_1_58 = 100; double var_1_59 = 9.5; signed char var_1_60 = 8; unsigned short int var_1_61 = 50; float var_1_62 = 24.8; float var_1_63 = 15.6; unsigned short int var_1_64 = 64160; unsigned short int var_1_65 = 2; unsigned short int var_1_66 = 64; unsigned char var_1_67 = 1; unsigned char var_1_68 = 0; unsigned char var_1_69 = 0; signed char var_1_70 = -8; signed char var_1_71 = -1; signed char var_1_72 = 64; signed char var_1_73 = 25; signed char var_1_74 = 64; unsigned short int var_1_75 = 32; signed short int var_1_76 = 32; signed short int var_1_77 = -5; double var_1_78 = 10.1; double var_1_79 = 128.8; double var_1_80 = 127.2; unsigned char var_1_81 = 0; unsigned char var_1_82 = 0; signed long int var_1_83 = 500; unsigned char var_1_84 = 4; signed short int var_1_85 = -100; signed long int var_1_86 = 1584867576; signed long int var_1_87 = 50; float var_1_88 = 16.375; float var_1_89 = 127.5; double var_1_90 = 15.7; double var_1_91 = 63.5; float var_1_92 = 4.25; float var_1_93 = 49.702; double var_1_94 = 63.75; unsigned char var_1_95 = 16; float var_1_96 = 50.5; double var_1_97 = 500.5; float var_1_98 = 1.5; signed short int var_1_99 = -25; signed char var_1_100 = -4; signed short int var_1_101 = 500; signed short int var_1_102 = 256; double var_1_103 = 128.5; double var_1_104 = 4.125; signed char var_1_105 = 10; unsigned char var_1_106 = 1; signed char var_1_107 = 1; signed char var_1_108 = 4; unsigned char var_1_109 = 10; signed char var_1_110 = -64; unsigned char var_1_111 = 1; unsigned char var_1_112 = 1; unsigned char var_1_113 = 0; double var_1_114 = 64.2; signed short int var_1_115 = 4; signed char var_1_116 = -8; signed char var_1_117 = -16; signed char var_1_118 = -2; signed char var_1_119 = 32; signed char var_1_120 = -4; unsigned char var_1_121 = 8; unsigned char var_1_122 = 5; unsigned long int var_1_123 = 10000000; signed long int var_1_124 = 10; signed long int var_1_125 = -5; signed char var_1_126 = -100; unsigned char var_1_127 = 1; double var_1_128 = 9.5; unsigned char var_1_129 = 1; unsigned char var_1_130 = 16; float var_1_131 = 99999999999999.5; unsigned long int var_1_132 = 64; unsigned char var_1_133 = 0; signed long int var_1_134 = 5; double var_1_135 = 9.4; float var_1_136 = 31.7; double var_1_137 = 4.15; float var_1_138 = 1.6; unsigned char var_1_139 = 16; signed short int var_1_140 = 16; // Calibration values // Last'ed variables // Additional functions void initially(void) { } void step(void) { // From: CodeObject1 if (((var_1_25 * var_1_26) <= var_1_27) || var_1_28) { if ((var_1_29 - 256u) < var_1_27) { var_1_24 = (! var_1_30); } } else { var_1_24 = ((var_1_30 || (var_1_31 || var_1_32)) || var_1_33); } // From: CodeObject2 if ((- var_1_35) <= (- 32.25f)) { var_1_34 = (max (var_1_36 , (abs (var_1_26)))); } // From: CodeObject3 if (var_1_31) { var_1_37 = (max (var_1_38 , var_1_39)); } // From: CodeObject4 if (var_1_34 < var_1_38) { var_1_40 = (abs (var_1_37)); } // From: CodeObject5 if ((var_1_35 / (min (24.125 , var_1_42))) < var_1_43) { if ((abs (var_1_39)) > var_1_38) { var_1_41 = ((min ((abs (var_1_44)) , var_1_45)) + var_1_46); } } else { if (var_1_46 <= var_1_44) { if (var_1_45 >= var_1_44) { var_1_41 = (abs (min (var_1_44 , var_1_46))); } } else { var_1_41 = var_1_45; } } // From: CodeObject6 if (var_1_31) { if (var_1_44 <= (min (var_1_42 , (- var_1_45)))) { var_1_47 = (var_1_48 + var_1_49); } else { var_1_47 = (min (var_1_49 , (var_1_50 - 32))); } } // From: CodeObject7 if (var_1_32) { if (var_1_25 > var_1_37) { var_1_51 = (abs (var_1_38)); } else { var_1_51 = (min (5 , (abs (var_1_50 - var_1_48)))); } } else { var_1_51 = (var_1_50 - var_1_49); } // From: CodeObject8 if (64 >= (var_1_39 - var_1_50)) { var_1_52 = (max ((max (var_1_50 , var_1_51)) , var_1_53)); } else { var_1_52 = (abs (var_1_39)); } // From: CodeObject9 if (((max (var_1_47 , -256)) >> var_1_26) > var_1_34) { var_1_54 = ((var_1_55 + var_1_56) + (max (var_1_44 , (min (var_1_45 , var_1_46))))); } else { var_1_54 = (99999.6f - 9.999999999999925E13f); } // From: CodeObject10 if (var_1_31 && var_1_24) { if (var_1_32) { var_1_57 = (abs (var_1_58)); } } // From: CodeObject11 if ((var_1_58 * (var_1_40 | var_1_36)) > var_1_39) { var_1_59 = (abs (var_1_55)); } // From: CodeObject12 if (var_1_29 >= (max (var_1_37 , var_1_50))) { var_1_60 = var_1_58; } // From: CodeObject13 if (((var_1_41 + var_1_46) * (var_1_62 - var_1_63)) > var_1_43) { if ((max (var_1_38 , var_1_39)) <= var_1_57) { var_1_61 = (min ((abs (min (var_1_49 , var_1_50))) , (max ((abs (var_1_53)) , var_1_39)))); } else { var_1_61 = (var_1_64 - var_1_48); } } // From: CodeObject14 if (var_1_52 < var_1_34) { if (var_1_31) { if (var_1_30 || (var_1_28 || var_1_32)) { var_1_65 = var_1_66; } } } else { var_1_65 = (max (((abs (var_1_39)) + var_1_38) , (min (var_1_64 , var_1_51)))); } // From: CodeObject15 if (var_1_24) { var_1_67 = (((min (var_1_40 , var_1_49)) == var_1_65) || (var_1_68 && var_1_69)); } else { var_1_67 = var_1_33; } // From: CodeObject16 if (var_1_49 > (var_1_52 & (var_1_36 % var_1_50))) { if (((abs (var_1_54)) - var_1_62) <= var_1_63) { var_1_70 = (abs (var_1_58)); } } else { if (var_1_41 < (var_1_63 - var_1_62)) { if (4u <= var_1_48) { if (var_1_62 <= (var_1_44 / (abs (var_1_42)))) { var_1_70 = (abs (abs (max (var_1_58 , var_1_71)))); } } else { var_1_70 = (abs ((var_1_72 - var_1_73) - var_1_74)); } } else { var_1_70 = (abs (var_1_71)); } } // From: CodeObject17 if ((var_1_29 % var_1_72) >= var_1_37) { if (var_1_44 <= ((max (var_1_42 , var_1_46)) * (- var_1_35))) { if (var_1_52 < var_1_73) { var_1_75 = ((abs (var_1_74)) + var_1_49); } } } else { var_1_75 = (10 + (var_1_37 + var_1_47)); } // From: CodeObject18 if (var_1_34 == (~ var_1_74)) { if (10 >= (var_1_48 & var_1_66)) { if ((abs (var_1_39 / var_1_64)) < (~ var_1_25)) { var_1_76 = (max (var_1_37 , var_1_58)); } } } // From: CodeObject19 if ((min ((abs (var_1_35)) , (var_1_62 - var_1_63))) >= 2.5f) { var_1_77 = (var_1_47 + (max (var_1_60 , var_1_57))); } // From: CodeObject20 if (var_1_76 >= var_1_34) { var_1_78 = ((var_1_55 + var_1_56) + (var_1_79 - var_1_80)); } // From: CodeObject21 if (((var_1_70 + var_1_65) > (var_1_71 | var_1_26)) || var_1_69) { if ((max (var_1_80 , (max (64.6f , var_1_55)))) > var_1_44) { var_1_81 = (var_1_69 && var_1_32); } } else { if ((64 & var_1_70) > (var_1_26 / var_1_50)) { var_1_81 = (! var_1_68); } else { var_1_81 = (var_1_33 || (var_1_82 || (var_1_30 || var_1_32))); } } // From: CodeObject22 if (((var_1_73 & var_1_40) / var_1_50) >= (var_1_60 ^ var_1_49)) { var_1_83 = (abs (abs (abs (var_1_36)))); } // From: CodeObject23 if (var_1_24 || (var_1_27 > var_1_53)) { var_1_84 = (abs (4 + var_1_73)); } else { var_1_84 = (min (var_1_72 , var_1_73)); } // From: CodeObject24 if (((min (var_1_61 , var_1_48)) & var_1_83) <= (var_1_73 - (var_1_86 - var_1_52))) { var_1_85 = var_1_70; } else { var_1_85 = (((abs (var_1_39)) + var_1_70) + (var_1_48 - var_1_72)); } // From: CodeObject25 if (var_1_85 <= var_1_65) { var_1_87 = (max (var_1_85 , (min (var_1_25 , var_1_60)))); } // From: CodeObject26 if (var_1_66 <= var_1_27) { var_1_88 = (max (var_1_44 , (max ((var_1_55 + 63.25f) , var_1_46)))); } // From: CodeObject27 if (var_1_28 || var_1_82) { var_1_89 = (abs (var_1_45)); } else { if (var_1_67) { var_1_89 = (abs (abs (1.000000075E7f))); } } // From: CodeObject28 if ((var_1_61 ^ (var_1_74 * var_1_39)) <= var_1_58) { var_1_90 = (var_1_91 + 127.912); } // From: CodeObject29 if (var_1_82) { var_1_92 = (var_1_80 - var_1_79); } // From: CodeObject30 if (var_1_83 > (min (var_1_26 , var_1_72))) { if (var_1_56 > (abs (var_1_43))) { if (var_1_68) { var_1_93 = var_1_45; } } } // From: CodeObject31 if (var_1_46 >= var_1_93) { var_1_94 = (var_1_80 - var_1_79); } else { var_1_94 = ((min (var_1_46 , var_1_80)) + var_1_45); } // From: CodeObject32 if ((abs (max (var_1_64 , var_1_38))) > (var_1_60 | (~ -128))) { if (var_1_88 != var_1_94) { if ((abs (var_1_62)) <= var_1_94) { var_1_95 = (min (var_1_48 , var_1_74)); } else { var_1_95 = var_1_74; } } } else { var_1_95 = (abs (var_1_50)); } // From: CodeObject33 if (var_1_90 <= (abs (var_1_97))) { var_1_96 = ((abs (var_1_91)) + var_1_56); } // From: CodeObject34 if ((~ (var_1_66 & 1)) >= (var_1_27 ^ (min (var_1_25 , var_1_64)))) { if ((var_1_47 * var_1_60) >= var_1_85) { var_1_98 = var_1_80; } } else { if (var_1_84 <= 16) { var_1_98 = (abs (var_1_55)); } else { var_1_98 = ((abs (var_1_79)) - var_1_80); } } // From: CodeObject35 if (((abs (128)) << var_1_74) <= var_1_61) { if (var_1_90 >= 9.75) { var_1_99 = -10; } } else { var_1_99 = (abs (var_1_58)); } // From: CodeObject36 var_1_100 = (abs (var_1_72 - (min (var_1_73 , var_1_74)))); // From: CodeObject37 if (var_1_30) { var_1_101 = (abs (var_1_102 + var_1_51)); } else { var_1_101 = (abs (var_1_26)); } // From: CodeObject38 if ((~ (var_1_49 ^ var_1_83)) <= var_1_72) { var_1_103 = (abs (var_1_46)); } // From: CodeObject39 if (var_1_75 <= (abs (var_1_37))) { if (var_1_58 <= var_1_73) { if ((~ var_1_36) <= var_1_102) { var_1_104 = ((abs (var_1_45)) - var_1_79); } } else { var_1_104 = (var_1_79 + var_1_46); } } // From: CodeObject40 if (var_1_106) { var_1_105 = ((abs (var_1_58)) - (min (var_1_73 , (var_1_107 + var_1_108)))); } else { var_1_105 = ((var_1_108 - var_1_107) + -5); } // From: CodeObject41 if ((abs (var_1_88)) >= var_1_93) { var_1_109 = (min ((max (var_1_38 , var_1_107)) , var_1_73)); } else { if (var_1_69 && (0 < var_1_86)) { var_1_109 = (abs (var_1_108)); } } // From: CodeObject42 if (var_1_109 <= (min (var_1_66 , var_1_60))) { if (var_1_34 > var_1_40) { var_1_110 = (max (var_1_58 , var_1_107)); } else { var_1_110 = (abs (var_1_58)); } } else { var_1_110 = -2; } // From: CodeObject43 if (((max (255.4 , var_1_63)) - var_1_62) >= var_1_89) { if ((abs (var_1_104)) >= var_1_62) { var_1_111 = (var_1_68 && (var_1_69 && var_1_112)); } else { var_1_111 = (! ((var_1_47 < var_1_70) && var_1_82)); } } // From: CodeObject44 if (! (var_1_40 > var_1_105)) { var_1_113 = (abs (var_1_38)); } else { var_1_113 = (min (var_1_49 , var_1_50)); } // From: CodeObject45 if (var_1_66 > var_1_76) { if (var_1_90 < var_1_103) { var_1_114 = (var_1_56 + (abs (var_1_45))); } else { var_1_114 = (min (10.9 , var_1_55)); } } // From: CodeObject46 var_1_115 = (max ((abs (var_1_113)) , var_1_48)); // From: CodeObject47 if (var_1_29 < var_1_27) { if (var_1_81) { var_1_116 = (abs (var_1_73)); } } else { if ((max ((abs (var_1_96)) , var_1_114)) >= var_1_88) { var_1_116 = (abs (min (var_1_71 , var_1_73))); } else { var_1_116 = (var_1_107 + (min ((var_1_117 + var_1_118) , (var_1_119 + var_1_120)))); } } // From: CodeObject48 if ((- var_1_104) <= var_1_79) { var_1_121 = 0; } else { var_1_121 = var_1_108; } // From: CodeObject49 if (var_1_69) { var_1_122 = 1; } // From: CodeObject50 if (var_1_106) { var_1_123 = var_1_49; } // From: CodeObject51 if (var_1_67) { var_1_124 = 1; } else { var_1_124 = 16; } // From: CodeObject52 var_1_125 = -50; // From: CodeObject53 if (var_1_30) { var_1_126 = var_1_108; } // From: CodeObject54 var_1_127 = var_1_33; // From: CodeObject55 if (var_1_68) { var_1_128 = 1.4; } else { var_1_128 = var_1_45; } // From: CodeObject56 if (var_1_127) { var_1_129 = var_1_30; } else { var_1_129 = var_1_33; } // From: CodeObject57 var_1_130 = var_1_72; // From: CodeObject58 var_1_131 = var_1_45; // From: CodeObject59 var_1_132 = 4u; // From: CodeObject60 if (var_1_33) { var_1_133 = var_1_48; } // From: CodeObject61 var_1_134 = var_1_50; // From: CodeObject62 if (var_1_111) { var_1_135 = var_1_46; } // From: CodeObject63 if (var_1_30) { var_1_136 = var_1_55; } else { var_1_136 = var_1_44; } // From: CodeObject64 if (var_1_91 > var_1_135) { var_1_137 = (var_1_79 - (var_1_80 + (abs (var_1_46)))); } // From: CodeObject65 var_1_138 = var_1_44; // From: CodeObject66 var_1_139 = var_1_38; // From: CodeObject67 var_1_140 = var_1_70; // From: Req2Batch57PS_CN_500 signed char stepLocal_0 = var_1_2; if (-256 <= stepLocal_0) { var_1_7 = (var_1_8 + ((max (var_1_9 , var_1_10)) + (var_1_11 + var_1_12))); } else { if (var_1_11 == var_1_9) { var_1_7 = var_1_8; } } // From: Req3Batch57PS_CN_500 if (var_1_11 <= var_1_9) { var_1_13 = ((max ((var_1_14 - var_1_15) , var_1_16)) - (var_1_17 + (max (var_1_18 , var_1_19)))); } // From: Req1Batch57PS_CN_500 if ((var_1_2 - var_1_3) > (var_1_13 / var_1_5)) { var_1_1 = (128 - var_1_3); } else { if (! var_1_6) { var_1_1 = var_1_3; } else { var_1_1 = var_1_3; } } // From: Req4Batch57PS_CN_500 signed long int stepLocal_1 = (var_1_2 * var_1_13) & var_1_1; if (var_1_3 < stepLocal_1) { var_1_20 = ((abs (var_1_18)) + var_1_14); } // From: Req5Batch57PS_CN_500 signed long int stepLocal_2 = var_1_1 & var_1_3; if (((max (var_1_1 , var_1_5)) + (var_1_1 / var_1_14)) <= stepLocal_2) { if (var_1_6) { var_1_21 = var_1_12; } else { var_1_21 = var_1_10; } } else { var_1_21 = var_1_12; } // From: Req6Batch57PS_CN_500 unsigned long int stepLocal_3 = var_1_20; if (var_1_1 > stepLocal_3) { if (! (! var_1_6)) { var_1_23 = var_1_8; } } } void updateVariables() { var_1_2 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_2 >= -1); assume_abort_if_not(var_1_2 <= 127); var_1_3 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_3 >= 0); assume_abort_if_not(var_1_3 <= 127); var_1_5 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_5 >= -2147483648); assume_abort_if_not(var_1_5 <= 2147483647); assume_abort_if_not(var_1_5 != 0); var_1_6 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_6 >= 0); assume_abort_if_not(var_1_6 <= 1); var_1_8 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_8 >= -461168.6018427382800e+13F && var_1_8 <= -1.0e-20F) || (var_1_8 <= 4611686.018427382800e+12F && var_1_8 >= 1.0e-20F )); var_1_9 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_9 >= -230584.3009213691390e+13F && var_1_9 <= -1.0e-20F) || (var_1_9 <= 2305843.009213691390e+12F && var_1_9 >= 1.0e-20F )); var_1_10 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_10 >= -230584.3009213691390e+13F && var_1_10 <= -1.0e-20F) || (var_1_10 <= 2305843.009213691390e+12F && var_1_10 >= 1.0e-20F )); var_1_11 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_11 >= -115292.1504606845700e+13F && var_1_11 <= -1.0e-20F) || (var_1_11 <= 1152921.504606845700e+12F && var_1_11 >= 1.0e-20F )); var_1_12 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_12 >= -115292.1504606845700e+13F && var_1_12 <= -1.0e-20F) || (var_1_12 <= 1152921.504606845700e+12F && var_1_12 >= 1.0e-20F )); var_1_14 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_14 >= 190); assume_abort_if_not(var_1_14 <= 254); var_1_15 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_15 >= 0); assume_abort_if_not(var_1_15 <= 63); var_1_16 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_16 >= 127); assume_abort_if_not(var_1_16 <= 254); var_1_17 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_17 >= 0); assume_abort_if_not(var_1_17 <= 64); var_1_18 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_18 >= 0); assume_abort_if_not(var_1_18 <= 63); var_1_19 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_19 >= 0); assume_abort_if_not(var_1_19 <= 63); var_1_25 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_25 >= -128); assume_abort_if_not(var_1_25 <= 127); var_1_26 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_26 >= -128); assume_abort_if_not(var_1_26 <= 127); var_1_27 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_27 >= -2147483648); assume_abort_if_not(var_1_27 <= 2147483647); var_1_28 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_28 >= 0); assume_abort_if_not(var_1_28 <= 1); var_1_29 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_29 >= 2147483647); assume_abort_if_not(var_1_29 <= 4294967295); var_1_30 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_30 >= 0); assume_abort_if_not(var_1_30 <= 0); var_1_31 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_31 >= 0); assume_abort_if_not(var_1_31 <= 0); var_1_32 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_32 >= 0); assume_abort_if_not(var_1_32 <= 0); var_1_33 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_33 >= 0); assume_abort_if_not(var_1_33 <= 0); var_1_35 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_35 >= -922337.2036854776000e+13F && var_1_35 <= -1.0e-20F) || (var_1_35 <= 9223372.036854776000e+12F && var_1_35 >= 1.0e-20F )); var_1_36 = __VERIFIER_nondet_short(); assume_abort_if_not(var_1_36 >= -32767); assume_abort_if_not(var_1_36 <= 32766); var_1_38 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_38 >= 0); assume_abort_if_not(var_1_38 <= 254); var_1_39 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_39 >= 0); assume_abort_if_not(var_1_39 <= 254); var_1_42 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_42 >= -922337.2036854776000e+13F && var_1_42 <= -1.0e-20F) || (var_1_42 <= 9223372.036854776000e+12F && var_1_42 >= 1.0e-20F )); assume_abort_if_not(var_1_42 != 0.0F); var_1_43 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_43 >= -922337.2036854776000e+13F && var_1_43 <= -1.0e-20F) || (var_1_43 <= 9223372.036854776000e+12F && var_1_43 >= 1.0e-20F )); var_1_44 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_44 >= -461168.6018427382800e+13F && var_1_44 <= -1.0e-20F) || (var_1_44 <= 4611686.018427382800e+12F && var_1_44 >= 1.0e-20F )); var_1_45 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_45 >= -461168.6018427382800e+13F && var_1_45 <= -1.0e-20F) || (var_1_45 <= 4611686.018427382800e+12F && var_1_45 >= 1.0e-20F )); var_1_46 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_46 >= -461168.6018427382800e+13F && var_1_46 <= -1.0e-20F) || (var_1_46 <= 4611686.018427382800e+12F && var_1_46 >= 1.0e-20F )); var_1_48 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_48 >= 0); assume_abort_if_not(var_1_48 <= 127); var_1_49 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_49 >= 0); assume_abort_if_not(var_1_49 <= 127); var_1_50 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_50 >= 127); assume_abort_if_not(var_1_50 <= 254); var_1_53 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_53 >= 0); assume_abort_if_not(var_1_53 <= 65534); var_1_55 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_55 >= -230584.3009213691390e+13F && var_1_55 <= -1.0e-20F) || (var_1_55 <= 2305843.009213691390e+12F && var_1_55 >= 1.0e-20F )); var_1_56 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_56 >= -230584.3009213691390e+13F && var_1_56 <= -1.0e-20F) || (var_1_56 <= 2305843.009213691390e+12F && var_1_56 >= 1.0e-20F )); var_1_58 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_58 >= -126); assume_abort_if_not(var_1_58 <= 126); var_1_62 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_62 >= 0.0F && var_1_62 <= -1.0e-20F) || (var_1_62 <= 9223372.036854776000e+12F && var_1_62 >= 1.0e-20F )); var_1_63 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_63 >= 0.0F && var_1_63 <= -1.0e-20F) || (var_1_63 <= 9223372.036854776000e+12F && var_1_63 >= 1.0e-20F )); var_1_64 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_64 >= 32767); assume_abort_if_not(var_1_64 <= 65534); var_1_66 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_66 >= 0); assume_abort_if_not(var_1_66 <= 65534); var_1_68 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_68 >= 1); assume_abort_if_not(var_1_68 <= 1); var_1_69 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_69 >= 1); assume_abort_if_not(var_1_69 <= 1); var_1_71 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_71 >= -126); assume_abort_if_not(var_1_71 <= 126); var_1_72 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_72 >= 63); assume_abort_if_not(var_1_72 <= 126); var_1_73 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_73 >= 0); assume_abort_if_not(var_1_73 <= 63); var_1_74 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_74 >= 0); assume_abort_if_not(var_1_74 <= 126); var_1_79 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_79 >= 0.0F && var_1_79 <= -1.0e-20F) || (var_1_79 <= 4611686.018427382800e+12F && var_1_79 >= 1.0e-20F )); var_1_80 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_80 >= 0.0F && var_1_80 <= -1.0e-20F) || (var_1_80 <= 4611686.018427382800e+12F && var_1_80 >= 1.0e-20F )); var_1_82 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_82 >= 0); assume_abort_if_not(var_1_82 <= 0); var_1_86 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_86 >= 1073741823); assume_abort_if_not(var_1_86 <= 2147483647); var_1_91 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_91 >= -461168.6018427382800e+13F && var_1_91 <= -1.0e-20F) || (var_1_91 <= 4611686.018427382800e+12F && var_1_91 >= 1.0e-20F )); var_1_97 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_97 >= -922337.2036854776000e+13F && var_1_97 <= -1.0e-20F) || (var_1_97 <= 9223372.036854776000e+12F && var_1_97 >= 1.0e-20F )); var_1_102 = __VERIFIER_nondet_short(); assume_abort_if_not(var_1_102 >= -16383); assume_abort_if_not(var_1_102 <= 16383); var_1_106 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_106 >= 0); assume_abort_if_not(var_1_106 <= 1); var_1_107 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_107 >= 0); assume_abort_if_not(var_1_107 <= 63); var_1_108 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_108 >= 0); assume_abort_if_not(var_1_108 <= 63); var_1_112 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_112 >= 1); assume_abort_if_not(var_1_112 <= 1); var_1_117 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_117 >= -31); assume_abort_if_not(var_1_117 <= 32); var_1_118 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_118 >= -31); assume_abort_if_not(var_1_118 <= 31); var_1_119 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_119 >= -31); assume_abort_if_not(var_1_119 <= 32); var_1_120 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_120 >= -31); assume_abort_if_not(var_1_120 <= 31); } void updateLastVariables() { } int property() { return (((((((var_1_2 - var_1_3) > (var_1_13 / var_1_5)) ? (var_1_1 == ((unsigned char) (128 - var_1_3))) : ((! var_1_6) ? (var_1_1 == ((unsigned char) var_1_3)) : (var_1_1 == ((unsigned char) var_1_3)))) && ((-256 <= var_1_2) ? (var_1_7 == ((double) (var_1_8 + ((max (var_1_9 , var_1_10)) + (var_1_11 + var_1_12))))) : ((var_1_11 == var_1_9) ? (var_1_7 == ((double) var_1_8)) : 1))) && ((var_1_11 <= var_1_9) ? (var_1_13 == ((unsigned char) ((max ((var_1_14 - var_1_15) , var_1_16)) - (var_1_17 + (max (var_1_18 , var_1_19)))))) : 1)) && ((var_1_3 < ((var_1_2 * var_1_13) & var_1_1)) ? (var_1_20 == ((unsigned long int) ((abs (var_1_18)) + var_1_14))) : 1)) && ((((max (var_1_1 , var_1_5)) + (var_1_1 / var_1_14)) <= (var_1_1 & var_1_3)) ? (var_1_6 ? (var_1_21 == ((float) var_1_12)) : (var_1_21 == ((float) var_1_10))) : (var_1_21 == ((float) var_1_12)))) && ((var_1_1 > var_1_20) ? ((! (! var_1_6)) ? (var_1_23 == ((double) var_1_8)) : 1) : 1) ; } int main(void) { isInitial = 1; initially(); while (1) { updateLastVariables(); updateVariables(); step(); __VERIFIER_assert(property()); isInitial = 0; } return 0; }