// This file is part of the SV-Benchmarks collection of verification tasks: // https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks // // SPDX-FileCopyrightText: 2022 Jana (Philipp) Berger // // SPDX-License-Identifier: GPL-3.0-or-later extern unsigned long __VERIFIER_nondet_ulong(); extern long __VERIFIER_nondet_long(); extern unsigned char __VERIFIER_nondet_uchar(); extern char __VERIFIER_nondet_char(); extern unsigned short __VERIFIER_nondet_ushort(); extern short __VERIFIER_nondet_short(); extern float __VERIFIER_nondet_float(); extern double __VERIFIER_nondet_double(); extern void abort(void); extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); void reach_error() { __assert_fail("0", "Req1_Prop1_Batch18PS_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(); } } unsigned char isInitial = 0; signed char var_1_1 = -1; float var_1_3 = 32.4; float var_1_4 = 5.5; float var_1_5 = 255.475; unsigned char var_1_7 = 0; signed char var_1_8 = -5; signed char var_1_9 = 2; unsigned char var_1_10 = 16; unsigned char var_1_11 = 16; float var_1_12 = 10000000.8; float var_1_13 = 127.7; float var_1_14 = 199.2; float var_1_15 = 999999.5; signed long int var_1_16 = -8; signed short int var_1_18 = -8; double var_1_19 = 5.4; unsigned char var_1_20 = 0; float var_1_21 = 100.5; float var_1_22 = -0.5; unsigned char var_1_23 = 1; float var_1_24 = 10000000000000.6; float var_1_25 = -0.4; float var_1_26 = 10.5; signed char var_1_27 = -10; unsigned long int var_1_28 = 64; unsigned long int var_1_29 = 8; unsigned long int var_1_30 = 5; signed char var_1_31 = -1; float var_1_32 = 199.7; float var_1_33 = 0.0; float var_1_34 = 0.0; float var_1_35 = 7.8; float var_1_36 = 1.25; signed long int var_1_37 = -1; double var_1_38 = 256.1; double var_1_39 = 999999.56; double var_1_40 = 0.9; signed long int var_1_41 = 16; signed char var_1_42 = 2; signed char var_1_43 = -4; unsigned char var_1_44 = 32; unsigned char var_1_45 = 25; unsigned char var_1_46 = 4; double var_1_47 = 8.25; double var_1_48 = 5.663; unsigned char var_1_49 = 5; float var_1_50 = 0.0; unsigned long int var_1_51 = 25; unsigned short int var_1_52 = 200; unsigned short int var_1_53 = 128; unsigned long int var_1_54 = 256; unsigned long int var_1_55 = 100; unsigned char var_1_56 = 0; unsigned char var_1_57 = 0; unsigned char var_1_58 = 0; unsigned char var_1_59 = 0; unsigned char var_1_60 = 0; double var_1_61 = 64.2; double var_1_62 = 7.75; unsigned char var_1_63 = 1; unsigned char var_1_64 = 128; unsigned char var_1_65 = 0; double var_1_66 = 8.5; unsigned long int var_1_67 = 64; unsigned long int var_1_68 = 4063372736; float var_1_69 = 99999999.5; unsigned short int var_1_70 = 25; unsigned short int var_1_71 = 25481; unsigned short int var_1_72 = 22265; unsigned short int var_1_73 = 65511; unsigned long int var_1_74 = 25; signed char var_1_75 = 10; signed char var_1_76 = 25; signed char var_1_77 = 10; signed long int var_1_78 = -32; double var_1_79 = 10.5; unsigned char var_1_80 = 2; signed short int var_1_81 = -5; unsigned long int var_1_82 = 128; signed long int var_1_83 = 2; float var_1_84 = 999999999.4; unsigned char var_1_85 = 4; unsigned short int var_1_86 = 16; float var_1_87 = 9.625; signed long int var_1_88 = -2; double var_1_89 = 15.75; float var_1_90 = 15.4; unsigned char var_1_91 = 16; signed long int var_1_92 = 100; unsigned char var_1_93 = 25; unsigned char var_1_94 = 200; unsigned char var_1_95 = 0; signed long int var_1_96 = 0; float var_1_97 = 9999999999999.5; unsigned short int var_1_98 = 10; unsigned long int var_1_99 = 256; unsigned long int var_1_100 = 64; signed char var_1_101 = -16; unsigned long int var_1_102 = 3325529739; unsigned char var_1_103 = 0; float var_1_104 = 15.2; unsigned long int var_1_105 = 4; signed long int var_1_106 = -64; unsigned short int var_1_107 = 16; unsigned char var_1_108 = 1; signed short int var_1_109 = 0; signed short int var_1_110 = 500; unsigned short int var_1_111 = 16; signed char var_1_112 = -128; signed char var_1_113 = 10; signed char var_1_114 = 2; signed char var_1_115 = 8; unsigned short int var_1_116 = 0; unsigned char var_1_117 = 1; unsigned short int var_1_118 = 50; signed char var_1_119 = -64; float var_1_120 = 99.9; double var_1_121 = 127.8; float var_1_122 = 200.25; unsigned char var_1_123 = 100; unsigned short int var_1_124 = 256; unsigned short int var_1_125 = 500; unsigned char var_1_126 = 0; unsigned char var_1_127 = 4; unsigned long int var_1_128 = 16; unsigned char var_1_129 = 0; double var_1_130 = 49.5; unsigned char var_1_131 = 1; unsigned char var_1_132 = 1; signed char last_1_var_1_1 = -1; unsigned char last_1_var_1_10 = 16; signed long int last_1_var_1_16 = -8; void initially(void) { } void step(void) { if (var_1_21 < (- var_1_22)) { if (var_1_22 <= var_1_21) { var_1_20 = var_1_23; } } if (var_1_20 || (-100 > -4)) { if (var_1_20) { var_1_24 = ((((var_1_25) > (var_1_26)) ? (var_1_25) : (var_1_26))); } else { var_1_24 = ((((var_1_26) < (var_1_25)) ? (var_1_26) : (var_1_25))); } } if (((((var_1_28) < (var_1_29)) ? (var_1_28) : (var_1_29))) < var_1_30) { var_1_27 = var_1_31; } if (var_1_21 > var_1_22) { var_1_32 = ((((((var_1_33) > (var_1_34)) ? (var_1_33) : (var_1_34))) - (3.5600648937963013E18f - var_1_35)) - 100.5f); } else { var_1_32 = (var_1_35 + var_1_36); } if (var_1_23) { var_1_37 = var_1_27; } var_1_38 = (127.2 + (var_1_35 - var_1_39)); if ((var_1_31 * -1) != (var_1_30 / var_1_41)) { var_1_40 = ((((var_1_39) > (((((var_1_26) < 0 ) ? -(var_1_26) : (var_1_26))))) ? (var_1_39) : (((((var_1_26) < 0 ) ? -(var_1_26) : (var_1_26)))))); } else { var_1_40 = ((((var_1_34) < 0 ) ? -(var_1_34) : (var_1_34))); } if (var_1_23) { var_1_42 = ((((var_1_43) < 0 ) ? -(var_1_43) : (var_1_43))); } if (var_1_20) { var_1_44 = ((((var_1_45) > (var_1_46)) ? (var_1_45) : (var_1_46))); } if (var_1_33 < var_1_21) { var_1_47 = (var_1_39 - ((((var_1_33) < ((var_1_35 + var_1_48))) ? (var_1_33) : ((var_1_35 + var_1_48))))); } if (((((var_1_35) < 0 ) ? -(var_1_35) : (var_1_35))) <= (var_1_34 - (var_1_50 - var_1_48))) { var_1_49 = ((((var_1_45) > (var_1_46)) ? (var_1_45) : (var_1_46))); } var_1_51 = ((((var_1_44) < 0 ) ? -(var_1_44) : (var_1_44))); if (((((var_1_51) < ((var_1_30 ^ var_1_45))) ? (var_1_51) : ((var_1_30 ^ var_1_45)))) >= var_1_41) { var_1_52 = ((((var_1_49) < 0 ) ? -(var_1_49) : (var_1_49))); } else { if (var_1_45 >= (((((64) > (var_1_49)) ? (64) : (var_1_49))) & var_1_46)) { var_1_52 = ((((var_1_53) > (var_1_45)) ? (var_1_53) : (var_1_45))); } } if ((var_1_51 * var_1_53) <= var_1_45) { var_1_54 = ((((var_1_53) < 0 ) ? -(var_1_53) : (var_1_53))); } if (((32 << 5) / 100) >= (((((var_1_42 & var_1_28)) > (var_1_46)) ? ((var_1_42 & var_1_28)) : (var_1_46)))) { if ((~ var_1_41) > 1) { var_1_55 = ((((var_1_52) < 0 ) ? -(var_1_52) : (var_1_52))); } } if (var_1_20) { var_1_56 = (! var_1_57); } else { var_1_56 = ((var_1_28 == var_1_55) && var_1_57); } if ((5 & (var_1_53 / var_1_41)) <= var_1_54) { if (var_1_20) { var_1_58 = (! (var_1_23 && (var_1_59 && var_1_60))); } } else { var_1_58 = (! var_1_57); } if (! var_1_20) { if (var_1_44 <= var_1_52) { if (var_1_58) { if (50 >= var_1_54) { var_1_61 = ((((var_1_33) < ((var_1_35 - ((((var_1_62) > (var_1_48)) ? (var_1_62) : (var_1_48)))))) ? (var_1_33) : ((var_1_35 - ((((var_1_62) > (var_1_48)) ? (var_1_62) : (var_1_48))))))); } else { var_1_61 = ((((var_1_34) > (50.5)) ? (var_1_34) : (50.5))); } } } else { var_1_61 = var_1_26; } } var_1_63 = (var_1_64 - ((((var_1_65) < 0 ) ? -(var_1_65) : (var_1_65)))); if (((var_1_65 % var_1_64) | var_1_54) > (((((var_1_63) < 0 ) ? -(var_1_63) : (var_1_63))) | 8u)) { if (var_1_67 <= (var_1_68 - ((((var_1_46) > (100u)) ? (var_1_46) : (100u))))) { var_1_66 = (((((var_1_48) < (((((var_1_36) < 0 ) ? -(var_1_36) : (var_1_36))))) ? (var_1_48) : (((((var_1_36) < 0 ) ? -(var_1_36) : (var_1_36)))))) + var_1_35); } else { if (var_1_47 >= var_1_34) { var_1_66 = ((((var_1_48) < (var_1_35)) ? (var_1_48) : (var_1_35))); } else { var_1_66 = ((((var_1_33) < 0 ) ? -(var_1_33) : (var_1_33))); } } } else { var_1_66 = (((((var_1_48 + var_1_36)) < ((var_1_35 - var_1_62))) ? ((var_1_48 + var_1_36)) : ((var_1_35 - var_1_62)))); } if (var_1_22 >= (var_1_35 + (var_1_21 / var_1_33))) { if (var_1_48 < (var_1_66 * var_1_39)) { var_1_69 = ((((var_1_25) < (var_1_48)) ? (var_1_25) : (var_1_48))); } else { var_1_69 = (((((var_1_36) < 0 ) ? -(var_1_36) : (var_1_36))) - ((((var_1_26) < 0 ) ? -(var_1_26) : (var_1_26)))); } } else { var_1_69 = ((((((((var_1_33) < (var_1_48)) ? (var_1_33) : (var_1_48))) - var_1_34) < 0 ) ? -(((((var_1_33) < (var_1_48)) ? (var_1_33) : (var_1_48))) - var_1_34) : (((((var_1_33) < (var_1_48)) ? (var_1_33) : (var_1_48))) - var_1_34))); } if ((var_1_45 > var_1_42) || (var_1_68 > var_1_53)) { if (((((var_1_64) < 0 ) ? -(var_1_64) : (var_1_64))) <= var_1_49) { var_1_70 = ((var_1_71 + ((((var_1_72) < 0 ) ? -(var_1_72) : (var_1_72)))) - (var_1_64 + var_1_46)); } else { if ((~ var_1_27) <= var_1_37) { var_1_70 = (((((((var_1_71) > (((((var_1_64) < (var_1_65)) ? (var_1_64) : (var_1_65))))) ? (var_1_71) : (((((var_1_64) < (var_1_65)) ? (var_1_64) : (var_1_65)))))) < 0 ) ? -((((var_1_71) > (((((var_1_64) < (var_1_65)) ? (var_1_64) : (var_1_65))))) ? (var_1_71) : (((((var_1_64) < (var_1_65)) ? (var_1_64) : (var_1_65)))))) : ((((var_1_71) > (((((var_1_64) < (var_1_65)) ? (var_1_64) : (var_1_65))))) ? (var_1_71) : (((((var_1_64) < (var_1_65)) ? (var_1_64) : (var_1_65)))))))); } else { var_1_70 = (((((var_1_73) < 0 ) ? -(var_1_73) : (var_1_73))) - (((((((var_1_44) < 0 ) ? -(var_1_44) : (var_1_44))) < 0 ) ? -((((var_1_44) < 0 ) ? -(var_1_44) : (var_1_44))) : ((((var_1_44) < 0 ) ? -(var_1_44) : (var_1_44)))))); } } } if (var_1_60 && (var_1_53 >= (var_1_49 % var_1_41))) { var_1_74 = (((((((var_1_71 + var_1_49) < 0 ) ? -(var_1_71 + var_1_49) : (var_1_71 + var_1_49))) < 0 ) ? -((((var_1_71 + var_1_49) < 0 ) ? -(var_1_71 + var_1_49) : (var_1_71 + var_1_49))) : ((((var_1_71 + var_1_49) < 0 ) ? -(var_1_71 + var_1_49) : (var_1_71 + var_1_49))))); } else { var_1_74 = ((((var_1_71) < 0 ) ? -(var_1_71) : (var_1_71))); } if (var_1_60 || var_1_56) { var_1_75 = ((((var_1_43) > (var_1_31)) ? (var_1_43) : (var_1_31))); } else { if (var_1_60) { var_1_75 = (var_1_76 + var_1_77); } } if (var_1_21 < ((((var_1_35) < 0 ) ? -(var_1_35) : (var_1_35)))) { if (var_1_74 <= (var_1_49 / var_1_41)) { var_1_78 = ((((200) < 0 ) ? -(200) : (200))); } else { if (((((var_1_26) > ((var_1_39 - var_1_33))) ? (var_1_26) : ((var_1_39 - var_1_33)))) > var_1_79) { var_1_78 = (((((((var_1_31) < 0 ) ? -(var_1_31) : (var_1_31))) < 0 ) ? -((((var_1_31) < 0 ) ? -(var_1_31) : (var_1_31))) : ((((var_1_31) < 0 ) ? -(var_1_31) : (var_1_31))))); } } } if ((-10000 >> var_1_54) <= (32 << var_1_27)) { var_1_80 = (((((((var_1_46) < (((((var_1_65) < 0 ) ? -(var_1_65) : (var_1_65))))) ? (var_1_46) : (((((var_1_65) < 0 ) ? -(var_1_65) : (var_1_65)))))) < 0 ) ? -((((var_1_46) < (((((var_1_65) < 0 ) ? -(var_1_65) : (var_1_65))))) ? (var_1_46) : (((((var_1_65) < 0 ) ? -(var_1_65) : (var_1_65)))))) : ((((var_1_46) < (((((var_1_65) < 0 ) ? -(var_1_65) : (var_1_65))))) ? (var_1_46) : (((((var_1_65) < 0 ) ? -(var_1_65) : (var_1_65)))))))); } if (var_1_37 > var_1_54) { if (var_1_50 < var_1_32) { var_1_81 = ((((var_1_76) > (var_1_75)) ? (var_1_76) : (var_1_75))); } else { var_1_81 = (var_1_64 - ((((var_1_46) < 0 ) ? -(var_1_46) : (var_1_46)))); } } if (var_1_30 > var_1_28) { if (var_1_60 || (var_1_74 != var_1_52)) { var_1_82 = var_1_73; } else { if (var_1_34 < var_1_39) { if ((var_1_31 | var_1_73) == (((((var_1_83) < (4)) ? (var_1_83) : (4))) - 10)) { var_1_82 = ((((var_1_72) > (var_1_80)) ? (var_1_72) : (var_1_80))); } else { var_1_82 = var_1_64; } } } } else { var_1_82 = ((((var_1_70) > (var_1_71)) ? (var_1_70) : (var_1_71))); } if (var_1_50 != var_1_40) { var_1_84 = 9.5f; } else { var_1_84 = var_1_36; } if (var_1_59) { var_1_85 = var_1_45; } else { var_1_85 = var_1_64; } var_1_86 = var_1_44; if (var_1_57) { var_1_87 = var_1_39; } if (var_1_59) { var_1_88 = var_1_31; } if (var_1_57) { var_1_89 = var_1_35; } else { var_1_89 = var_1_36; } var_1_90 = var_1_39; if (var_1_56) { var_1_91 = var_1_64; } var_1_92 = var_1_91; if (var_1_83 > var_1_64) { var_1_93 = ((((var_1_46) < 0 ) ? -(var_1_46) : (var_1_46))); } if ((var_1_49 | var_1_31) < var_1_77) { if (((8 / var_1_64) & (var_1_51 >> var_1_42)) < ((var_1_93 >> var_1_43) * var_1_53)) { if (var_1_73 >= var_1_72) { var_1_94 = var_1_46; } else { var_1_94 = var_1_46; } } } if ((var_1_41 * var_1_88) > (var_1_65 - var_1_96)) { if (var_1_20) { if (((((49.6f) < ((var_1_97 * var_1_40))) ? (49.6f) : ((var_1_97 * var_1_40)))) <= var_1_90) { var_1_95 = ((var_1_52 != var_1_65) && var_1_57); } } } if (var_1_57) { var_1_98 = ((((var_1_53) > ((((((var_1_45) < 0 ) ? -(var_1_45) : (var_1_45))) + 16))) ? (var_1_53) : ((((((var_1_45) < 0 ) ? -(var_1_45) : (var_1_45))) + 16)))); } else { var_1_98 = ((((var_1_46) > (((((4) > (25)) ? (4) : (25))))) ? (var_1_46) : (((((4) > (25)) ? (4) : (25)))))); } if (var_1_66 <= var_1_25) { if (var_1_29 > var_1_96) { var_1_99 = ((((var_1_72) < 0 ) ? -(var_1_72) : (var_1_72))); } } else { var_1_99 = ((((var_1_71) < (var_1_44)) ? (var_1_71) : (var_1_44))); } if (4u < var_1_72) { if (var_1_42 < (var_1_63 ^ var_1_101)) { var_1_100 = ((((var_1_93 + var_1_49) < 0 ) ? -(var_1_93 + var_1_49) : (var_1_93 + var_1_49))); } else { var_1_100 = ((((((((var_1_102) < 0 ) ? -(var_1_102) : (var_1_102))) - var_1_80) < 0 ) ? -(((((var_1_102) < 0 ) ? -(var_1_102) : (var_1_102))) - var_1_80) : (((((var_1_102) < 0 ) ? -(var_1_102) : (var_1_102))) - var_1_80))); } } if (var_1_81 <= ((((var_1_65 - var_1_80) < 0 ) ? -(var_1_65 - var_1_80) : (var_1_65 - var_1_80)))) { var_1_103 = (var_1_56 || (! var_1_57)); } else { var_1_103 = (! var_1_57); } if (((((var_1_102) < (var_1_88)) ? (var_1_102) : (var_1_88))) == (var_1_105 * ((((var_1_67) < 0 ) ? -(var_1_67) : (var_1_67))))) { if (var_1_37 == ((((var_1_72) < 0 ) ? -(var_1_72) : (var_1_72)))) { var_1_104 = (((((((((var_1_62) < (var_1_48)) ? (var_1_62) : (var_1_48))) - ((((var_1_35) < 0 ) ? -(var_1_35) : (var_1_35))))) < (var_1_33)) ? ((((((var_1_62) < (var_1_48)) ? (var_1_62) : (var_1_48))) - ((((var_1_35) < 0 ) ? -(var_1_35) : (var_1_35))))) : (var_1_33))); } } if ((var_1_50 == 128.66f) && (! var_1_95)) { if (((var_1_50 - var_1_39) - var_1_48) >= 16.5) { var_1_106 = (var_1_70 + ((((var_1_94) < (((((var_1_73) < 0 ) ? -(var_1_73) : (var_1_73))))) ? (var_1_94) : (((((var_1_73) < 0 ) ? -(var_1_73) : (var_1_73))))))); } else { var_1_106 = (((((((((var_1_45 + 4)) > (var_1_63)) ? ((var_1_45 + 4)) : (var_1_63)))) > (var_1_53)) ? ((((((var_1_45 + 4)) > (var_1_63)) ? ((var_1_45 + 4)) : (var_1_63)))) : (var_1_53))); } } var_1_107 = ((((var_1_80) < 0 ) ? -(var_1_80) : (var_1_80))); if (var_1_51 >= var_1_94) { if (32u == var_1_86) { if (var_1_95) { var_1_108 = (! var_1_57); } } else { var_1_108 = (! 0); } } if ((var_1_88 | (var_1_41 >> var_1_29)) < var_1_31) { if (var_1_60) { var_1_109 = ((var_1_75 + var_1_46) + -128); } else { var_1_109 = (((((((var_1_64) < 0 ) ? -(var_1_64) : (var_1_64))) < 0 ) ? -((((var_1_64) < 0 ) ? -(var_1_64) : (var_1_64))) : ((((var_1_64) < 0 ) ? -(var_1_64) : (var_1_64))))); } } if ((var_1_73 - ((((var_1_72) < (var_1_64)) ? (var_1_72) : (var_1_64)))) < ((10 << var_1_68) & -8)) { var_1_110 = (var_1_44 - var_1_49); } if (var_1_58) { if ((-25 * var_1_37) < (var_1_43 % var_1_41)) { var_1_111 = (((((((var_1_73 - var_1_45) < 0 ) ? -(var_1_73 - var_1_45) : (var_1_73 - var_1_45))) < 0 ) ? -((((var_1_73 - var_1_45) < 0 ) ? -(var_1_73 - var_1_45) : (var_1_73 - var_1_45))) : ((((var_1_73 - var_1_45) < 0 ) ? -(var_1_73 - var_1_45) : (var_1_73 - var_1_45))))); } } if ((var_1_105 > var_1_96) || (((((var_1_33) < 0 ) ? -(var_1_33) : (var_1_33))) == var_1_48)) { var_1_112 = ((var_1_113 - (var_1_114 + var_1_115)) + var_1_77); } if (var_1_40 >= var_1_34) { var_1_116 = var_1_71; } else { if ((((((((var_1_93) < 0 ) ? -(var_1_93) : (var_1_93))) < 0 ) ? -((((var_1_93) < 0 ) ? -(var_1_93) : (var_1_93))) : ((((var_1_93) < 0 ) ? -(var_1_93) : (var_1_93))))) >= var_1_74) { var_1_116 = (((((((25) > (((((var_1_53) < (var_1_113)) ? (var_1_53) : (var_1_113))))) ? (25) : (((((var_1_53) < (var_1_113)) ? (var_1_53) : (var_1_113)))))) < 0 ) ? -((((25) > (((((var_1_53) < (var_1_113)) ? (var_1_53) : (var_1_113))))) ? (25) : (((((var_1_53) < (var_1_113)) ? (var_1_53) : (var_1_113)))))) : ((((25) > (((((var_1_53) < (var_1_113)) ? (var_1_53) : (var_1_113))))) ? (25) : (((((var_1_53) < (var_1_113)) ? (var_1_53) : (var_1_113)))))))); } else { var_1_116 = (((((var_1_73) > (56453)) ? (var_1_73) : (56453))) - var_1_46); } } if (((var_1_98 ^ var_1_92) | var_1_82) < var_1_106) { var_1_117 = (! (var_1_95 || (var_1_23 || var_1_59))); } if ((var_1_81 + var_1_113) <= var_1_80) { var_1_118 = (((((var_1_73) < 0 ) ? -(var_1_73) : (var_1_73))) - var_1_114); } if (var_1_23) { var_1_119 = (var_1_76 + ((((var_1_77) < (var_1_113)) ? (var_1_77) : (var_1_113)))); } if (var_1_57 && var_1_23) { if (((((var_1_74) < (var_1_98)) ? (var_1_74) : (var_1_98))) > var_1_45) { var_1_120 = (var_1_62 - var_1_34); } } else { var_1_120 = (128.5f + var_1_36); } if (var_1_54 > ((((var_1_99) < (var_1_85)) ? (var_1_99) : (var_1_85)))) { var_1_121 = var_1_26; } else { if (((((var_1_80) < 0 ) ? -(var_1_80) : (var_1_80))) > var_1_73) { if (var_1_90 >= (((((1.25f) > (var_1_48)) ? (1.25f) : (var_1_48))) - ((((var_1_34) > (var_1_122)) ? (var_1_34) : (var_1_122))))) { var_1_121 = var_1_48; } else { var_1_121 = ((((var_1_35) < 0 ) ? -(var_1_35) : (var_1_35))); } } else { var_1_121 = (((((((var_1_62) < (var_1_48)) ? (var_1_62) : (var_1_48))) < 0 ) ? -((((var_1_62) < (var_1_48)) ? (var_1_62) : (var_1_48))) : ((((var_1_62) < (var_1_48)) ? (var_1_62) : (var_1_48))))); } } var_1_123 = var_1_64; var_1_124 = 2; if (var_1_108) { var_1_125 = var_1_65; } else { var_1_125 = var_1_72; } var_1_126 = var_1_23; if (var_1_58) { var_1_127 = 5; } else { var_1_127 = var_1_114; } var_1_128 = var_1_46; var_1_129 = var_1_57; var_1_130 = var_1_33; if (var_1_111 < var_1_74) { var_1_131 = (var_1_60 && var_1_57); } else { var_1_131 = (! var_1_23); } if (var_1_117) { if (var_1_71 < var_1_96) { var_1_132 = var_1_113; } } signed long int stepLocal_0 = last_1_var_1_16; if (var_1_9 < stepLocal_0) { if ((var_1_4 - var_1_5) > var_1_3) { var_1_10 = 8; } } else { var_1_10 = var_1_11; } if (var_1_7) { var_1_16 = var_1_8; } else { var_1_16 = (var_1_11 - ((((var_1_10 - var_1_10) < 0 ) ? -(var_1_10 - var_1_10) : (var_1_10 - var_1_10)))); } signed long int stepLocal_2 = last_1_var_1_10; if (! (last_1_var_1_1 > last_1_var_1_10)) { var_1_19 = ((((var_1_13) > ((((((0.05 + var_1_15)) < (var_1_14)) ? ((0.05 + var_1_15)) : (var_1_14))))) ? (var_1_13) : ((((((0.05 + var_1_15)) < (var_1_14)) ? ((0.05 + var_1_15)) : (var_1_14)))))); } else { if (stepLocal_2 > var_1_9) { var_1_19 = var_1_15; } } if (var_1_5 <= (var_1_19 / var_1_3)) { var_1_12 = ((((var_1_13) > ((var_1_14 + var_1_15))) ? (var_1_13) : ((var_1_14 + var_1_15)))); } else { var_1_12 = var_1_14; } if ((var_1_12 / var_1_3) > ((var_1_4 - var_1_5) * var_1_19)) { if (var_1_7) { var_1_1 = var_1_8; } else { var_1_1 = var_1_9; } } else { var_1_1 = var_1_8; } signed char stepLocal_1 = var_1_1; if (stepLocal_1 >= (var_1_16 + var_1_10)) { if (var_1_5 < 999.5f) { if (var_1_7) { var_1_18 = (var_1_16 + var_1_16); } else { var_1_18 = var_1_8; } } else { var_1_18 = var_1_9; } } else { var_1_18 = var_1_8; } } void updateVariables() { var_1_3 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_3 >= -922337.2036854776000e+13F && var_1_3 <= -1.0e-20F) || (var_1_3 <= 9223372.036854776000e+12F && var_1_3 >= 1.0e-20F )); assume_abort_if_not(var_1_3 != 0.0F); var_1_4 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_4 >= 0.0F && var_1_4 <= -1.0e-20F) || (var_1_4 <= 9223372.036854776000e+12F && var_1_4 >= 1.0e-20F )); var_1_5 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_5 >= 0.0F && var_1_5 <= -1.0e-20F) || (var_1_5 <= 9223372.036854776000e+12F && var_1_5 >= 1.0e-20F )); var_1_7 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_7 >= 0); assume_abort_if_not(var_1_7 <= 1); var_1_8 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_8 >= -127); assume_abort_if_not(var_1_8 <= 126); var_1_9 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_9 >= -127); assume_abort_if_not(var_1_9 <= 126); var_1_11 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_11 >= 0); assume_abort_if_not(var_1_11 <= 254); var_1_13 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_13 >= -922337.2036854765600e+13F && var_1_13 <= -1.0e-20F) || (var_1_13 <= 9223372.036854765600e+12F && var_1_13 >= 1.0e-20F )); var_1_14 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_14 >= -461168.6018427382800e+13F && var_1_14 <= -1.0e-20F) || (var_1_14 <= 4611686.018427382800e+12F && var_1_14 >= 1.0e-20F )); var_1_15 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_15 >= -461168.6018427382800e+13F && var_1_15 <= -1.0e-20F) || (var_1_15 <= 4611686.018427382800e+12F && var_1_15 >= 1.0e-20F )); var_1_21 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_21 >= -922337.2036854776000e+13F && var_1_21 <= -1.0e-20F) || (var_1_21 <= 9223372.036854776000e+12F && var_1_21 >= 1.0e-20F )); var_1_22 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_22 >= -922337.2036854776000e+13F && var_1_22 <= -1.0e-20F) || (var_1_22 <= 9223372.036854776000e+12F && var_1_22 >= 1.0e-20F )); var_1_23 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_23 >= 1); assume_abort_if_not(var_1_23 <= 1); var_1_25 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_25 >= -922337.2036854765600e+13F && var_1_25 <= -1.0e-20F) || (var_1_25 <= 9223372.036854765600e+12F && var_1_25 >= 1.0e-20F )); var_1_26 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_26 >= -922337.2036854765600e+13F && var_1_26 <= -1.0e-20F) || (var_1_26 <= 9223372.036854765600e+12F && var_1_26 >= 1.0e-20F )); var_1_28 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_28 >= 0); assume_abort_if_not(var_1_28 <= 4294967295); var_1_29 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_29 >= 0); assume_abort_if_not(var_1_29 <= 4294967295); var_1_30 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_30 >= 0); assume_abort_if_not(var_1_30 <= 4294967295); var_1_31 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_31 >= -127); assume_abort_if_not(var_1_31 <= 126); var_1_33 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_33 >= 4611686.018427382800e+12F && var_1_33 <= -1.0e-20F) || (var_1_33 <= 9223372.036854765600e+12F && var_1_33 >= 1.0e-20F )); var_1_34 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_34 >= 4611686.018427382800e+12F && var_1_34 <= -1.0e-20F) || (var_1_34 <= 9223372.036854765600e+12F && var_1_34 >= 1.0e-20F )); var_1_35 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_35 >= 0.0F && var_1_35 <= -1.0e-20F) || (var_1_35 <= 2305843.009213691390e+12F && var_1_35 >= 1.0e-20F )); var_1_36 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_36 >= -461168.6018427382800e+13F && var_1_36 <= -1.0e-20F) || (var_1_36 <= 4611686.018427382800e+12F && var_1_36 >= 1.0e-20F )); var_1_39 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_39 >= 0.0F && var_1_39 <= -1.0e-20F) || (var_1_39 <= 4611686.018427382800e+12F && var_1_39 >= 1.0e-20F )); var_1_41 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_41 >= -2147483648); assume_abort_if_not(var_1_41 <= 2147483647); assume_abort_if_not(var_1_41 != 0); var_1_43 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_43 >= -126); assume_abort_if_not(var_1_43 <= 126); var_1_45 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_45 >= 0); assume_abort_if_not(var_1_45 <= 254); var_1_46 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_46 >= 0); assume_abort_if_not(var_1_46 <= 254); var_1_48 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_48 >= 0.0F && var_1_48 <= -1.0e-20F) || (var_1_48 <= 4611686.018427382800e+12F && var_1_48 >= 1.0e-20F )); var_1_50 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_50 >= 4611686.018427387900e+12F && var_1_50 <= -1.0e-20F) || (var_1_50 <= 9223372.036854776000e+12F && var_1_50 >= 1.0e-20F )); var_1_53 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_53 >= 0); assume_abort_if_not(var_1_53 <= 65534); var_1_57 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_57 >= 0); assume_abort_if_not(var_1_57 <= 0); var_1_59 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_59 >= 1); assume_abort_if_not(var_1_59 <= 1); var_1_60 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_60 >= 1); assume_abort_if_not(var_1_60 <= 1); var_1_62 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_62 >= 0.0F && var_1_62 <= -1.0e-20F) || (var_1_62 <= 9223372.036854765600e+12F && var_1_62 >= 1.0e-20F )); var_1_64 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_64 >= 127); assume_abort_if_not(var_1_64 <= 254); var_1_65 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_65 >= 0); assume_abort_if_not(var_1_65 <= 127); var_1_67 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_67 >= 0); assume_abort_if_not(var_1_67 <= 4294967295); var_1_68 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_68 >= 2147483647); assume_abort_if_not(var_1_68 <= 4294967295); var_1_71 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_71 >= 16383); assume_abort_if_not(var_1_71 <= 32767); var_1_72 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_72 >= 16384); assume_abort_if_not(var_1_72 <= 32767); var_1_73 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_73 >= 32767); assume_abort_if_not(var_1_73 <= 65534); var_1_76 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_76 >= -63); assume_abort_if_not(var_1_76 <= 63); var_1_77 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_77 >= -63); assume_abort_if_not(var_1_77 <= 63); var_1_79 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_79 >= -922337.2036854776000e+13F && var_1_79 <= -1.0e-20F) || (var_1_79 <= 9223372.036854776000e+12F && var_1_79 >= 1.0e-20F )); var_1_83 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_83 >= -1); assume_abort_if_not(var_1_83 <= 2147483647); var_1_96 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_96 >= 0); assume_abort_if_not(var_1_96 <= 2147483647); var_1_97 = __VERIFIER_nondet_float(); 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_101 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_101 >= -128); assume_abort_if_not(var_1_101 <= 127); var_1_102 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_102 >= 2147483647); assume_abort_if_not(var_1_102 <= 4294967294); var_1_105 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_105 >= 0); assume_abort_if_not(var_1_105 <= 4294967295); var_1_113 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_113 >= 0); assume_abort_if_not(var_1_113 <= 63); var_1_114 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_114 >= 0); assume_abort_if_not(var_1_114 <= 32); var_1_115 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_115 >= 0); assume_abort_if_not(var_1_115 <= 31); var_1_122 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_122 >= 0.0F && var_1_122 <= -1.0e-20F) || (var_1_122 <= 9223372.036854776000e+12F && var_1_122 >= 1.0e-20F )); } void updateLastVariables() { last_1_var_1_1 = var_1_1; last_1_var_1_10 = var_1_10; last_1_var_1_16 = var_1_16; } int property() { return (((((((var_1_12 / var_1_3) > ((var_1_4 - var_1_5) * var_1_19)) ? (var_1_7 ? (var_1_1 == ((signed char) var_1_8)) : (var_1_1 == ((signed char) var_1_9))) : (var_1_1 == ((signed char) var_1_8))) && ((var_1_9 < last_1_var_1_16) ? (((var_1_4 - var_1_5) > var_1_3) ? (var_1_10 == ((unsigned char) 8)) : 1) : (var_1_10 == ((unsigned char) var_1_11)))) && ((var_1_5 <= (var_1_19 / var_1_3)) ? (var_1_12 == ((float) ((((var_1_13) > ((var_1_14 + var_1_15))) ? (var_1_13) : ((var_1_14 + var_1_15)))))) : (var_1_12 == ((float) var_1_14)))) && (var_1_7 ? (var_1_16 == ((signed long int) var_1_8)) : (var_1_16 == ((signed long int) (var_1_11 - ((((var_1_10 - var_1_10) < 0 ) ? -(var_1_10 - var_1_10) : (var_1_10 - var_1_10)))))))) && ((var_1_1 >= (var_1_16 + var_1_10)) ? ((var_1_5 < 999.5f) ? (var_1_7 ? (var_1_18 == ((signed short int) (var_1_16 + var_1_16))) : (var_1_18 == ((signed short int) var_1_8))) : (var_1_18 == ((signed short int) var_1_9))) : (var_1_18 == ((signed short int) var_1_8)))) && ((! (last_1_var_1_1 > last_1_var_1_10)) ? (var_1_19 == ((double) ((((var_1_13) > ((((((0.05 + var_1_15)) < (var_1_14)) ? ((0.05 + var_1_15)) : (var_1_14))))) ? (var_1_13) : ((((((0.05 + var_1_15)) < (var_1_14)) ? ((0.05 + var_1_15)) : (var_1_14)))))))) : ((last_1_var_1_10 > var_1_9) ? (var_1_19 == ((double) var_1_15)) : 1)) ; } int main(void) { isInitial = 1; initially(); while (1) { updateLastVariables(); updateVariables(); step(); __VERIFIER_assert(property()); isInitial = 0; } return 0; }