// 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_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(); } } unsigned char isInitial = 0; 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; void initially(void) { } void step(void) { 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); } if ((- var_1_35) <= (- 32.25f)) { var_1_34 = ((((var_1_36) > (((((var_1_26) < 0 ) ? -(var_1_26) : (var_1_26))))) ? (var_1_36) : (((((var_1_26) < 0 ) ? -(var_1_26) : (var_1_26)))))); } if (var_1_31) { var_1_37 = ((((var_1_38) > (var_1_39)) ? (var_1_38) : (var_1_39))); } if (var_1_34 < var_1_38) { var_1_40 = ((((var_1_37) < 0 ) ? -(var_1_37) : (var_1_37))); } if ((var_1_35 / ((((24.125) < (var_1_42)) ? (24.125) : (var_1_42)))) < var_1_43) { if (((((var_1_39) < 0 ) ? -(var_1_39) : (var_1_39))) > var_1_38) { var_1_41 = (((((((((var_1_44) < 0 ) ? -(var_1_44) : (var_1_44)))) < (var_1_45)) ? (((((var_1_44) < 0 ) ? -(var_1_44) : (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 = (((((((var_1_44) < (var_1_46)) ? (var_1_44) : (var_1_46))) < 0 ) ? -((((var_1_44) < (var_1_46)) ? (var_1_44) : (var_1_46))) : ((((var_1_44) < (var_1_46)) ? (var_1_44) : (var_1_46))))); } } else { var_1_41 = var_1_45; } } if (var_1_31) { if (var_1_44 <= ((((var_1_42) < ((- var_1_45))) ? (var_1_42) : ((- var_1_45))))) { var_1_47 = (var_1_48 + var_1_49); } else { var_1_47 = ((((var_1_49) < ((var_1_50 - 32))) ? (var_1_49) : ((var_1_50 - 32)))); } } if (var_1_32) { if (var_1_25 > var_1_37) { var_1_51 = ((((var_1_38) < 0 ) ? -(var_1_38) : (var_1_38))); } else { var_1_51 = ((((5) < (((((var_1_50 - var_1_48) < 0 ) ? -(var_1_50 - var_1_48) : (var_1_50 - var_1_48))))) ? (5) : (((((var_1_50 - var_1_48) < 0 ) ? -(var_1_50 - var_1_48) : (var_1_50 - var_1_48)))))); } } else { var_1_51 = (var_1_50 - var_1_49); } if (64 >= (var_1_39 - var_1_50)) { var_1_52 = ((((((((var_1_50) > (var_1_51)) ? (var_1_50) : (var_1_51)))) > (var_1_53)) ? (((((var_1_50) > (var_1_51)) ? (var_1_50) : (var_1_51)))) : (var_1_53))); } else { var_1_52 = ((((var_1_39) < 0 ) ? -(var_1_39) : (var_1_39))); } if ((((((var_1_47) > (-256)) ? (var_1_47) : (-256))) >> var_1_26) > var_1_34) { var_1_54 = ((var_1_55 + var_1_56) + ((((var_1_44) > (((((var_1_45) < (var_1_46)) ? (var_1_45) : (var_1_46))))) ? (var_1_44) : (((((var_1_45) < (var_1_46)) ? (var_1_45) : (var_1_46))))))); } else { var_1_54 = (99999.6f - 9.999999999999925E13f); } if (var_1_31 && var_1_24) { if (var_1_32) { var_1_57 = ((((var_1_58) < 0 ) ? -(var_1_58) : (var_1_58))); } } if ((var_1_58 * (var_1_40 | var_1_36)) > var_1_39) { var_1_59 = ((((var_1_55) < 0 ) ? -(var_1_55) : (var_1_55))); } if (var_1_29 >= ((((var_1_37) > (var_1_50)) ? (var_1_37) : (var_1_50)))) { var_1_60 = var_1_58; } if (((var_1_41 + var_1_46) * (var_1_62 - var_1_63)) > var_1_43) { if (((((var_1_38) > (var_1_39)) ? (var_1_38) : (var_1_39))) <= var_1_57) { var_1_61 = (((((((((((var_1_49) < (var_1_50)) ? (var_1_49) : (var_1_50))) < 0 ) ? -((((var_1_49) < (var_1_50)) ? (var_1_49) : (var_1_50))) : ((((var_1_49) < (var_1_50)) ? (var_1_49) : (var_1_50)))))) < (((((((((var_1_53) < 0 ) ? -(var_1_53) : (var_1_53)))) > (var_1_39)) ? (((((var_1_53) < 0 ) ? -(var_1_53) : (var_1_53)))) : (var_1_39))))) ? ((((((((var_1_49) < (var_1_50)) ? (var_1_49) : (var_1_50))) < 0 ) ? -((((var_1_49) < (var_1_50)) ? (var_1_49) : (var_1_50))) : ((((var_1_49) < (var_1_50)) ? (var_1_49) : (var_1_50)))))) : (((((((((var_1_53) < 0 ) ? -(var_1_53) : (var_1_53)))) > (var_1_39)) ? (((((var_1_53) < 0 ) ? -(var_1_53) : (var_1_53)))) : (var_1_39)))))); } else { var_1_61 = (var_1_64 - var_1_48); } } 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 = (((((((((var_1_39) < 0 ) ? -(var_1_39) : (var_1_39))) + var_1_38)) > (((((var_1_64) < (var_1_51)) ? (var_1_64) : (var_1_51))))) ? ((((((var_1_39) < 0 ) ? -(var_1_39) : (var_1_39))) + var_1_38)) : (((((var_1_64) < (var_1_51)) ? (var_1_64) : (var_1_51)))))); } if (var_1_24) { var_1_67 = ((((((var_1_40) < (var_1_49)) ? (var_1_40) : (var_1_49))) == var_1_65) || (var_1_68 && var_1_69)); } else { var_1_67 = var_1_33; } if (var_1_49 > (var_1_52 & (var_1_36 % var_1_50))) { if ((((((var_1_54) < 0 ) ? -(var_1_54) : (var_1_54))) - var_1_62) <= var_1_63) { var_1_70 = ((((var_1_58) < 0 ) ? -(var_1_58) : (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 / ((((var_1_42) < 0 ) ? -(var_1_42) : (var_1_42))))) { var_1_70 = ((((((((((var_1_58) > (var_1_71)) ? (var_1_58) : (var_1_71))) < 0 ) ? -((((var_1_58) > (var_1_71)) ? (var_1_58) : (var_1_71))) : ((((var_1_58) > (var_1_71)) ? (var_1_58) : (var_1_71))))) < 0 ) ? -(((((((var_1_58) > (var_1_71)) ? (var_1_58) : (var_1_71))) < 0 ) ? -((((var_1_58) > (var_1_71)) ? (var_1_58) : (var_1_71))) : ((((var_1_58) > (var_1_71)) ? (var_1_58) : (var_1_71))))) : (((((((var_1_58) > (var_1_71)) ? (var_1_58) : (var_1_71))) < 0 ) ? -((((var_1_58) > (var_1_71)) ? (var_1_58) : (var_1_71))) : ((((var_1_58) > (var_1_71)) ? (var_1_58) : (var_1_71))))))); } } else { var_1_70 = (((((var_1_72 - var_1_73) - var_1_74) < 0 ) ? -((var_1_72 - var_1_73) - var_1_74) : ((var_1_72 - var_1_73) - var_1_74))); } } else { var_1_70 = ((((var_1_71) < 0 ) ? -(var_1_71) : (var_1_71))); } } if ((var_1_29 % var_1_72) >= var_1_37) { if (var_1_44 <= (((((var_1_42) > (var_1_46)) ? (var_1_42) : (var_1_46))) * (- var_1_35))) { if (var_1_52 < var_1_73) { var_1_75 = (((((var_1_74) < 0 ) ? -(var_1_74) : (var_1_74))) + var_1_49); } } } else { var_1_75 = (10 + (var_1_37 + var_1_47)); } if (var_1_34 == (~ var_1_74)) { if (10 >= (var_1_48 & var_1_66)) { if (((((var_1_39 / var_1_64) < 0 ) ? -(var_1_39 / var_1_64) : (var_1_39 / var_1_64))) < (~ var_1_25)) { var_1_76 = ((((var_1_37) > (var_1_58)) ? (var_1_37) : (var_1_58))); } } } if (((((((((var_1_35) < 0 ) ? -(var_1_35) : (var_1_35)))) < ((var_1_62 - var_1_63))) ? (((((var_1_35) < 0 ) ? -(var_1_35) : (var_1_35)))) : ((var_1_62 - var_1_63)))) >= 2.5f) { var_1_77 = (var_1_47 + ((((var_1_60) > (var_1_57)) ? (var_1_60) : (var_1_57)))); } if (var_1_76 >= var_1_34) { var_1_78 = ((var_1_55 + var_1_56) + (var_1_79 - var_1_80)); } if (((var_1_70 + var_1_65) > (var_1_71 | var_1_26)) || var_1_69) { if (((((var_1_80) > (((((64.6f) > (var_1_55)) ? (64.6f) : (var_1_55))))) ? (var_1_80) : (((((64.6f) > (var_1_55)) ? (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))); } } if (((var_1_73 & var_1_40) / var_1_50) >= (var_1_60 ^ var_1_49)) { var_1_83 = ((((((((((var_1_36) < 0 ) ? -(var_1_36) : (var_1_36))) < 0 ) ? -((((var_1_36) < 0 ) ? -(var_1_36) : (var_1_36))) : ((((var_1_36) < 0 ) ? -(var_1_36) : (var_1_36))))) < 0 ) ? -(((((((var_1_36) < 0 ) ? -(var_1_36) : (var_1_36))) < 0 ) ? -((((var_1_36) < 0 ) ? -(var_1_36) : (var_1_36))) : ((((var_1_36) < 0 ) ? -(var_1_36) : (var_1_36))))) : (((((((var_1_36) < 0 ) ? -(var_1_36) : (var_1_36))) < 0 ) ? -((((var_1_36) < 0 ) ? -(var_1_36) : (var_1_36))) : ((((var_1_36) < 0 ) ? -(var_1_36) : (var_1_36))))))); } if (var_1_24 || (var_1_27 > var_1_53)) { var_1_84 = ((((4 + var_1_73) < 0 ) ? -(4 + var_1_73) : (4 + var_1_73))); } else { var_1_84 = ((((var_1_72) < (var_1_73)) ? (var_1_72) : (var_1_73))); } if ((((((var_1_61) < (var_1_48)) ? (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 = ((((((var_1_39) < 0 ) ? -(var_1_39) : (var_1_39))) + var_1_70) + (var_1_48 - var_1_72)); } if (var_1_85 <= var_1_65) { var_1_87 = ((((var_1_85) > (((((var_1_25) < (var_1_60)) ? (var_1_25) : (var_1_60))))) ? (var_1_85) : (((((var_1_25) < (var_1_60)) ? (var_1_25) : (var_1_60)))))); } if (var_1_66 <= var_1_27) { var_1_88 = ((((var_1_44) > ((((((var_1_55 + 63.25f)) > (var_1_46)) ? ((var_1_55 + 63.25f)) : (var_1_46))))) ? (var_1_44) : ((((((var_1_55 + 63.25f)) > (var_1_46)) ? ((var_1_55 + 63.25f)) : (var_1_46)))))); } if (var_1_28 || var_1_82) { var_1_89 = ((((var_1_45) < 0 ) ? -(var_1_45) : (var_1_45))); } else { if (var_1_67) { var_1_89 = (((((((1.000000075E7f) < 0 ) ? -(1.000000075E7f) : (1.000000075E7f))) < 0 ) ? -((((1.000000075E7f) < 0 ) ? -(1.000000075E7f) : (1.000000075E7f))) : ((((1.000000075E7f) < 0 ) ? -(1.000000075E7f) : (1.000000075E7f))))); } } if ((var_1_61 ^ (var_1_74 * var_1_39)) <= var_1_58) { var_1_90 = (var_1_91 + 127.912); } if (var_1_82) { var_1_92 = (var_1_80 - var_1_79); } if (var_1_83 > ((((var_1_26) < (var_1_72)) ? (var_1_26) : (var_1_72)))) { if (var_1_56 > ((((var_1_43) < 0 ) ? -(var_1_43) : (var_1_43)))) { if (var_1_68) { var_1_93 = var_1_45; } } } if (var_1_46 >= var_1_93) { var_1_94 = (var_1_80 - var_1_79); } else { var_1_94 = (((((var_1_46) < (var_1_80)) ? (var_1_46) : (var_1_80))) + var_1_45); } if ((((((((var_1_64) > (var_1_38)) ? (var_1_64) : (var_1_38))) < 0 ) ? -((((var_1_64) > (var_1_38)) ? (var_1_64) : (var_1_38))) : ((((var_1_64) > (var_1_38)) ? (var_1_64) : (var_1_38))))) > (var_1_60 | (~ -128))) { if (var_1_88 != var_1_94) { if (((((var_1_62) < 0 ) ? -(var_1_62) : (var_1_62))) <= var_1_94) { var_1_95 = ((((var_1_48) < (var_1_74)) ? (var_1_48) : (var_1_74))); } else { var_1_95 = var_1_74; } } } else { var_1_95 = ((((var_1_50) < 0 ) ? -(var_1_50) : (var_1_50))); } if (var_1_90 <= ((((var_1_97) < 0 ) ? -(var_1_97) : (var_1_97)))) { var_1_96 = (((((var_1_91) < 0 ) ? -(var_1_91) : (var_1_91))) + var_1_56); } if ((~ (var_1_66 & 1)) >= (var_1_27 ^ ((((var_1_25) < (var_1_64)) ? (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 = ((((var_1_55) < 0 ) ? -(var_1_55) : (var_1_55))); } else { var_1_98 = (((((var_1_79) < 0 ) ? -(var_1_79) : (var_1_79))) - var_1_80); } } if ((((((128) < 0 ) ? -(128) : (128))) << var_1_74) <= var_1_61) { if (var_1_90 >= 9.75) { var_1_99 = -10; } } else { var_1_99 = ((((var_1_58) < 0 ) ? -(var_1_58) : (var_1_58))); } var_1_100 = ((((var_1_72 - ((((var_1_73) < (var_1_74)) ? (var_1_73) : (var_1_74)))) < 0 ) ? -(var_1_72 - ((((var_1_73) < (var_1_74)) ? (var_1_73) : (var_1_74)))) : (var_1_72 - ((((var_1_73) < (var_1_74)) ? (var_1_73) : (var_1_74)))))); if (var_1_30) { var_1_101 = ((((var_1_102 + var_1_51) < 0 ) ? -(var_1_102 + var_1_51) : (var_1_102 + var_1_51))); } else { var_1_101 = ((((var_1_26) < 0 ) ? -(var_1_26) : (var_1_26))); } if ((~ (var_1_49 ^ var_1_83)) <= var_1_72) { var_1_103 = ((((var_1_46) < 0 ) ? -(var_1_46) : (var_1_46))); } if (var_1_75 <= ((((var_1_37) < 0 ) ? -(var_1_37) : (var_1_37)))) { if (var_1_58 <= var_1_73) { if ((~ var_1_36) <= var_1_102) { var_1_104 = (((((var_1_45) < 0 ) ? -(var_1_45) : (var_1_45))) - var_1_79); } } else { var_1_104 = (var_1_79 + var_1_46); } } if (var_1_106) { var_1_105 = (((((var_1_58) < 0 ) ? -(var_1_58) : (var_1_58))) - ((((var_1_73) < ((var_1_107 + var_1_108))) ? (var_1_73) : ((var_1_107 + var_1_108))))); } else { var_1_105 = ((var_1_108 - var_1_107) + -5); } if (((((var_1_88) < 0 ) ? -(var_1_88) : (var_1_88))) >= var_1_93) { var_1_109 = ((((((((var_1_38) > (var_1_107)) ? (var_1_38) : (var_1_107)))) < (var_1_73)) ? (((((var_1_38) > (var_1_107)) ? (var_1_38) : (var_1_107)))) : (var_1_73))); } else { if (var_1_69 && (0 < var_1_86)) { var_1_109 = ((((var_1_108) < 0 ) ? -(var_1_108) : (var_1_108))); } } if (var_1_109 <= ((((var_1_66) < (var_1_60)) ? (var_1_66) : (var_1_60)))) { if (var_1_34 > var_1_40) { var_1_110 = ((((var_1_58) > (var_1_107)) ? (var_1_58) : (var_1_107))); } else { var_1_110 = ((((var_1_58) < 0 ) ? -(var_1_58) : (var_1_58))); } } else { var_1_110 = -2; } if ((((((255.4) > (var_1_63)) ? (255.4) : (var_1_63))) - var_1_62) >= var_1_89) { if (((((var_1_104) < 0 ) ? -(var_1_104) : (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)); } } if (! (var_1_40 > var_1_105)) { var_1_113 = ((((var_1_38) < 0 ) ? -(var_1_38) : (var_1_38))); } else { var_1_113 = ((((var_1_49) < (var_1_50)) ? (var_1_49) : (var_1_50))); } if (var_1_66 > var_1_76) { if (var_1_90 < var_1_103) { var_1_114 = (var_1_56 + ((((var_1_45) < 0 ) ? -(var_1_45) : (var_1_45)))); } else { var_1_114 = ((((10.9) < (var_1_55)) ? (10.9) : (var_1_55))); } } var_1_115 = ((((((((var_1_113) < 0 ) ? -(var_1_113) : (var_1_113)))) > (var_1_48)) ? (((((var_1_113) < 0 ) ? -(var_1_113) : (var_1_113)))) : (var_1_48))); if (var_1_29 < var_1_27) { if (var_1_81) { var_1_116 = ((((var_1_73) < 0 ) ? -(var_1_73) : (var_1_73))); } } else { if (((((((((var_1_96) < 0 ) ? -(var_1_96) : (var_1_96)))) > (var_1_114)) ? (((((var_1_96) < 0 ) ? -(var_1_96) : (var_1_96)))) : (var_1_114))) >= var_1_88) { var_1_116 = (((((((var_1_71) < (var_1_73)) ? (var_1_71) : (var_1_73))) < 0 ) ? -((((var_1_71) < (var_1_73)) ? (var_1_71) : (var_1_73))) : ((((var_1_71) < (var_1_73)) ? (var_1_71) : (var_1_73))))); } else { var_1_116 = (var_1_107 + (((((var_1_117 + var_1_118)) < ((var_1_119 + var_1_120))) ? ((var_1_117 + var_1_118)) : ((var_1_119 + var_1_120))))); } } if ((- var_1_104) <= var_1_79) { var_1_121 = 0; } else { var_1_121 = var_1_108; } if (var_1_69) { var_1_122 = 1; } if (var_1_106) { var_1_123 = var_1_49; } if (var_1_67) { var_1_124 = 1; } else { var_1_124 = 16; } var_1_125 = -50; if (var_1_30) { var_1_126 = var_1_108; } var_1_127 = var_1_33; if (var_1_68) { var_1_128 = 1.4; } else { var_1_128 = var_1_45; } if (var_1_127) { var_1_129 = var_1_30; } else { var_1_129 = var_1_33; } var_1_130 = var_1_72; var_1_131 = var_1_45; var_1_132 = 4u; if (var_1_33) { var_1_133 = var_1_48; } var_1_134 = var_1_50; if (var_1_111) { var_1_135 = var_1_46; } if (var_1_30) { var_1_136 = var_1_55; } else { var_1_136 = var_1_44; } if (var_1_91 > var_1_135) { var_1_137 = (var_1_79 - (var_1_80 + ((((var_1_46) < 0 ) ? -(var_1_46) : (var_1_46))))); } var_1_138 = var_1_44; var_1_139 = var_1_38; var_1_140 = var_1_70; signed char stepLocal_0 = var_1_2; if (-256 <= stepLocal_0) { var_1_7 = (var_1_8 + (((((var_1_9) > (var_1_10)) ? (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; } } if (var_1_11 <= var_1_9) { var_1_13 = ((((((var_1_14 - var_1_15)) > (var_1_16)) ? ((var_1_14 - var_1_15)) : (var_1_16))) - (var_1_17 + ((((var_1_18) > (var_1_19)) ? (var_1_18) : (var_1_19))))); } 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; } } signed long int stepLocal_1 = (var_1_2 * var_1_13) & var_1_1; if (var_1_3 < stepLocal_1) { var_1_20 = (((((var_1_18) < 0 ) ? -(var_1_18) : (var_1_18))) + var_1_14); } signed long int stepLocal_2 = var_1_1 & var_1_3; if ((((((var_1_1) > (var_1_5)) ? (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; } 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 + (((((var_1_9) > (var_1_10)) ? (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) ((((((var_1_14 - var_1_15)) > (var_1_16)) ? ((var_1_14 - var_1_15)) : (var_1_16))) - (var_1_17 + ((((var_1_18) > (var_1_19)) ? (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) (((((var_1_18) < 0 ) ? -(var_1_18) : (var_1_18))) + var_1_14))) : 1)) && (((((((var_1_1) > (var_1_5)) ? (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; }