// 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_Batch24Amount500.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; float var_1_1 = 0.8; float var_1_5 = 10000000000.75; float var_1_6 = 50.5; float var_1_7 = 3.875; unsigned long int var_1_8 = 256; unsigned long int var_1_12 = 64; float var_1_13 = 199.5; float var_1_15 = -0.554; unsigned char var_1_16 = 25; unsigned char var_1_17 = 5; unsigned char var_1_18 = 32; unsigned char var_1_19 = 1; signed short int var_1_20 = -4; float var_1_21 = 256.8; float var_1_22 = 50.8; float var_1_24 = 127.3; float var_1_25 = 64.375; float var_1_26 = 5.6; unsigned char var_1_28 = 16; unsigned char var_1_29 = 2; double var_1_30 = 255.6; unsigned long int var_1_31 = 3622524486; unsigned long int var_1_32 = 3726811193; unsigned char var_1_33 = 4; unsigned char var_1_34 = 200; float var_1_35 = 256.5; unsigned short int var_1_36 = 53245; float var_1_37 = 1.3; float var_1_38 = 15.8; float var_1_39 = 15.8; signed short int var_1_40 = -100; signed char var_1_42 = -32; signed char var_1_43 = 10; signed char var_1_44 = 64; signed char var_1_45 = 10; signed char var_1_46 = 1; signed short int var_1_47 = -100; unsigned long int var_1_49 = 16; unsigned long int var_1_50 = 3055675291; unsigned long int var_1_51 = 3730780545; unsigned long int var_1_52 = 64; float var_1_53 = 15.25; unsigned long int var_1_54 = 10; double var_1_55 = 1.5; unsigned char var_1_56 = 1; unsigned char var_1_57 = 0; unsigned char var_1_58 = 0; unsigned char var_1_59 = 64; unsigned char var_1_60 = 5; signed long int var_1_61 = -128; signed char var_1_62 = 5; unsigned char var_1_63 = 1; unsigned char var_1_64 = 0; unsigned short int var_1_65 = 10; unsigned char var_1_66 = 0; unsigned long int var_1_67 = 1437123530; unsigned long int var_1_68 = 1631082099; unsigned char var_1_69 = 32; unsigned char var_1_70 = 200; double var_1_71 = 999999999999.5; double var_1_72 = 0.2; double var_1_73 = 9.5; double var_1_74 = 24.6; signed char var_1_75 = 25; unsigned short int var_1_76 = 10; unsigned short int var_1_78 = 44240; unsigned short int var_1_79 = 10000; unsigned short int var_1_80 = 60213; unsigned short int var_1_81 = 30811; signed long int var_1_82 = 16; signed long int var_1_86 = 1992720715; unsigned char var_1_88 = 0; unsigned char var_1_90 = 4; unsigned char var_1_91 = 5; double var_1_92 = 24.25; unsigned long int var_1_93 = 0; unsigned long int var_1_94 = 4278741392; float var_1_95 = 100.8; signed char var_1_96 = 1; signed char var_1_97 = 50; signed short int var_1_98 = 4; signed short int var_1_99 = 23530; double var_1_100 = 7.3; signed long int var_1_101 = 200; double var_1_102 = 15.3; signed long int var_1_103 = -8; signed short int var_1_104 = 32; signed long int var_1_105 = 8; signed char var_1_106 = -8; signed char var_1_107 = 1; unsigned char var_1_108 = 64; unsigned char var_1_109 = 0; unsigned char var_1_110 = 1; unsigned long int var_1_111 = 16; unsigned long int var_1_112 = 10; unsigned short int var_1_113 = 1; double var_1_114 = -0.625; signed char var_1_115 = -10; signed short int var_1_116 = 4; float last_1_var_1_1 = 0.8; unsigned long int last_1_var_1_8 = 256; float last_1_var_1_13 = 199.5; signed short int last_1_var_1_20 = -4; signed short int last_1_var_1_40 = -100; signed short int last_1_var_1_47 = -100; unsigned long int last_1_var_1_49 = 16; unsigned long int last_1_var_1_52 = 64; unsigned char last_1_var_1_56 = 1; unsigned char last_1_var_1_59 = 64; unsigned char last_1_var_1_63 = 1; unsigned short int last_1_var_1_76 = 10; signed long int last_1_var_1_82 = 16; unsigned char last_1_var_1_88 = 0; signed short int last_1_var_1_98 = 4; signed long int last_1_var_1_101 = 200; unsigned long int last_1_var_1_111 = 16; void initially(void) { } void step(void) { if (last_1_var_1_13 < var_1_15) { var_1_90 = (var_1_70 - (var_1_19 + (var_1_46 + var_1_91))); } if (var_1_6 <= last_1_var_1_13) { var_1_76 = (var_1_78 - (last_1_var_1_20 + (var_1_79 - 4))); } else { var_1_76 = ((var_1_80 - var_1_46) - (var_1_81 - 10)); } if (last_1_var_1_1 > ((((var_1_5) > (var_1_38)) ? (var_1_5) : (var_1_38)))) { var_1_56 = var_1_57; } else { if (((last_1_var_1_52 * var_1_54) / (var_1_44 + var_1_18)) <= last_1_var_1_101) { var_1_56 = var_1_57; } else { var_1_56 = (var_1_57 && var_1_58); } } unsigned char stepLocal_9 = var_1_19; if (! last_1_var_1_88) { if (var_1_15 == (var_1_5 + last_1_var_1_1)) { var_1_28 = (var_1_29 + ((((var_1_17) > ((64 - var_1_19))) ? (var_1_17) : ((64 - var_1_19))))); } else { var_1_28 = var_1_29; } } else { if (((((last_1_var_1_111) > (last_1_var_1_49)) ? (last_1_var_1_111) : (last_1_var_1_49))) >= stepLocal_9) { var_1_28 = ((((var_1_17) < 0 ) ? -(var_1_17) : (var_1_17))); } else { var_1_28 = (var_1_29 + var_1_17); } } unsigned char stepLocal_30 = ! var_1_58; if (stepLocal_30 && var_1_56) { var_1_88 = (var_1_57 && var_1_58); } if (var_1_88) { var_1_100 = (((((var_1_6 - var_1_5)) < (((((var_1_73) < (var_1_39)) ? (var_1_73) : (var_1_39))))) ? ((var_1_6 - var_1_5)) : (((((var_1_73) < (var_1_39)) ? (var_1_73) : (var_1_39)))))); } signed long int stepLocal_22 = last_1_var_1_76; unsigned char stepLocal_21 = last_1_var_1_56; unsigned char stepLocal_20 = var_1_17; if (stepLocal_22 <= var_1_36) { if (last_1_var_1_63 || stepLocal_21) { var_1_59 = ((((var_1_60) > (((((var_1_29) < (0)) ? (var_1_29) : (0))))) ? (var_1_60) : (((((var_1_29) < (0)) ? (var_1_29) : (0)))))); } else { if (stepLocal_20 >= last_1_var_1_59) { var_1_59 = ((((var_1_46) > (var_1_17)) ? (var_1_46) : (var_1_17))); } } } else { var_1_59 = (var_1_46 + var_1_18); } var_1_21 = (var_1_15 + var_1_7); unsigned char stepLocal_13 = var_1_18; if ((10 / var_1_12) == stepLocal_13) { var_1_33 = (var_1_29 + var_1_19); } if (var_1_56) { var_1_55 = (var_1_37 + ((((var_1_24) < (var_1_15)) ? (var_1_24) : (var_1_15)))); } var_1_62 = (var_1_19 - var_1_17); var_1_65 = (var_1_17 + 1); if (var_1_65 > (var_1_18 * var_1_67)) { var_1_69 = (((((var_1_70 - var_1_17)) > (var_1_46)) ? ((var_1_70 - var_1_17)) : (var_1_46))); } else { var_1_69 = ((((var_1_46) > ((var_1_70 - var_1_17))) ? (var_1_46) : ((var_1_70 - var_1_17)))); } unsigned char stepLocal_25 = var_1_69; if (var_1_33 < stepLocal_25) { var_1_71 = ((var_1_72 + var_1_73) + var_1_39); } else { var_1_71 = (var_1_24 + var_1_7); } if (var_1_39 != (var_1_38 - 4.25f)) { var_1_75 = ((((((((var_1_46) > (var_1_17)) ? (var_1_46) : (var_1_17)))) < (((var_1_45 + var_1_18) - var_1_19))) ? (((((var_1_46) > (var_1_17)) ? (var_1_46) : (var_1_17)))) : (((var_1_45 + var_1_18) - var_1_19)))); } var_1_93 = (((((var_1_94 - var_1_80) - var_1_78) < 0 ) ? -((var_1_94 - var_1_80) - var_1_78) : ((var_1_94 - var_1_80) - var_1_78))); if (! ((var_1_51 / var_1_44) > (~ var_1_68))) { var_1_95 = (((((var_1_26 - var_1_38)) < (var_1_7)) ? ((var_1_26 - var_1_38)) : (var_1_7))); } if (var_1_69 > var_1_19) { var_1_96 = ((((var_1_18) > ((var_1_97 - (var_1_44 - var_1_19)))) ? (var_1_18) : ((var_1_97 - (var_1_44 - var_1_19))))); } else { if (var_1_33 > var_1_51) { if (var_1_91 < var_1_94) { var_1_96 = ((((((((var_1_45) < (var_1_91)) ? (var_1_45) : (var_1_91)))) < ((((((var_1_46 - var_1_17)) < (var_1_19)) ? ((var_1_46 - var_1_17)) : (var_1_19))))) ? (((((var_1_45) < (var_1_91)) ? (var_1_45) : (var_1_91)))) : ((((((var_1_46 - var_1_17)) < (var_1_19)) ? ((var_1_46 - var_1_17)) : (var_1_19)))))); } else { var_1_96 = (((((((((-8) < (10)) ? (-8) : (10)))) < (var_1_46)) ? (((((-8) < (10)) ? (-8) : (10)))) : (var_1_46))) + var_1_19); } } else { var_1_96 = (var_1_45 + var_1_91); } } var_1_102 = var_1_5; var_1_105 = var_1_86; var_1_108 = var_1_18; var_1_109 = var_1_58; if (var_1_64) { var_1_112 = 5u; } var_1_113 = var_1_99; var_1_114 = var_1_72; if (var_1_109) { var_1_115 = var_1_18; } unsigned char stepLocal_2 = var_1_59; signed char stepLocal_1 = var_1_96; if (var_1_5 >= var_1_6) { if (last_1_var_1_8 < stepLocal_1) { var_1_8 = (((((var_1_96 + ((((last_1_var_1_8) > (var_1_28)) ? (last_1_var_1_8) : (var_1_28))))) > ((var_1_90 + var_1_59))) ? ((var_1_96 + ((((last_1_var_1_8) > (var_1_28)) ? (last_1_var_1_8) : (var_1_28))))) : ((var_1_90 + var_1_59)))); } else { var_1_8 = (var_1_59 + var_1_28); } } else { if (stepLocal_2 > (var_1_96 / var_1_12)) { var_1_8 = last_1_var_1_8; } else { var_1_8 = (last_1_var_1_8 + ((((var_1_90) < 0 ) ? -(var_1_90) : (var_1_90)))); } } unsigned long int stepLocal_6 = (((var_1_12) < (var_1_76)) ? (var_1_12) : (var_1_76)); if (stepLocal_6 < var_1_59) { if (var_1_109) { var_1_20 = var_1_19; } } else { var_1_20 = ((((var_1_18) < (var_1_17)) ? (var_1_18) : (var_1_17))); } unsigned char stepLocal_0 = var_1_90; if (var_1_75 <= stepLocal_0) { var_1_1 = (var_1_5 - var_1_6); } else { var_1_1 = (10.5f + var_1_7); } if (var_1_88) { if ((var_1_33 * var_1_69) == var_1_69) { if ((! (var_1_114 > var_1_7)) || (var_1_64 || var_1_58)) { var_1_74 = 31.65; } } } else { var_1_74 = ((((31.75) > (0.25)) ? (31.75) : (0.25))); } if ((- var_1_28) < last_1_var_1_47) { if (((var_1_29 - var_1_19) + -5) > (var_1_65 - var_1_45)) { var_1_47 = var_1_45; } else { if (! var_1_56) { var_1_47 = (var_1_18 - var_1_46); } else { var_1_47 = (((((var_1_17 + ((((var_1_115) < (var_1_115)) ? (var_1_115) : (var_1_115))))) < (var_1_45)) ? ((var_1_17 + ((((var_1_115) < (var_1_115)) ? (var_1_115) : (var_1_115))))) : (var_1_45))); } } } if (var_1_112 < var_1_68) { var_1_92 = ((((var_1_25) < (var_1_24)) ? (var_1_25) : (var_1_24))); } else { var_1_92 = ((((9999999.2) > (var_1_26)) ? (9999999.2) : (var_1_26))); } unsigned char stepLocal_31 = var_1_17; if ((var_1_69 / ((((var_1_68) > (var_1_79)) ? (var_1_68) : (var_1_79)))) == stepLocal_31) { var_1_98 = var_1_79; } else { if (var_1_109) { var_1_98 = ((((last_1_var_1_98) > (((var_1_99 - 128) - var_1_70))) ? (last_1_var_1_98) : (((var_1_99 - 128) - var_1_70)))); } else { var_1_98 = ((((-32) < ((var_1_60 + var_1_79))) ? (-32) : ((var_1_60 + var_1_79)))); } } if (var_1_109) { var_1_103 = var_1_96; } else { var_1_103 = -256; } if (var_1_109) { var_1_104 = 5; } else { var_1_104 = var_1_36; } unsigned char stepLocal_4 = var_1_28; unsigned char stepLocal_3 = var_1_28; if (stepLocal_3 >= (10u / var_1_12)) { if (stepLocal_4 < ((((var_1_8) < (var_1_28)) ? (var_1_8) : (var_1_28)))) { var_1_13 = var_1_7; } else { var_1_13 = (var_1_7 + var_1_15); } } else { var_1_13 = var_1_15; } signed long int stepLocal_8 = (var_1_59 * var_1_19) * var_1_69; unsigned char stepLocal_7 = var_1_56; if (var_1_92 >= var_1_92) { if (var_1_109) { var_1_22 = (((((var_1_15) < (var_1_7)) ? (var_1_15) : (var_1_7))) + ((((((((var_1_24) < (9.125f)) ? (var_1_24) : (9.125f)))) > (var_1_25)) ? (((((var_1_24) < (9.125f)) ? (var_1_24) : (9.125f)))) : (var_1_25)))); } else { var_1_22 = (((((var_1_15 + var_1_7)) > (((((0.4f) > ((var_1_5 - var_1_26))) ? (0.4f) : ((var_1_5 - var_1_26)))))) ? ((var_1_15 + var_1_7)) : (((((0.4f) > ((var_1_5 - var_1_26))) ? (0.4f) : ((var_1_5 - var_1_26))))))); } } else { if ((- var_1_112) > stepLocal_8) { if ((var_1_28 < var_1_69) && stepLocal_7) { var_1_22 = ((((var_1_7) < (var_1_26)) ? (var_1_7) : (var_1_26))); } else { if (var_1_26 >= (var_1_6 - var_1_5)) { var_1_22 = var_1_15; } else { if (var_1_56) { var_1_22 = var_1_24; } else { var_1_22 = 4.625f; } } } } } signed long int stepLocal_18 = ~ var_1_44; if (var_1_6 != var_1_22) { var_1_52 = var_1_36; } else { if (stepLocal_18 < (var_1_12 & var_1_45)) { var_1_52 = ((((var_1_44) > (var_1_96)) ? (var_1_44) : (var_1_96))); } } if (var_1_46 < ((-50 + var_1_115) + ((((var_1_29) < 0 ) ? -(var_1_29) : (var_1_29))))) { var_1_61 = (var_1_34 - var_1_93); } else { if ((var_1_69 >> var_1_46) > (var_1_18 + ((((var_1_54) < (var_1_60)) ? (var_1_54) : (var_1_60))))) { var_1_61 = (((((((((var_1_18 - 4)) > (var_1_104)) ? ((var_1_18 - 4)) : (var_1_104)))) < (var_1_19)) ? ((((((var_1_18 - 4)) > (var_1_104)) ? ((var_1_18 - 4)) : (var_1_104)))) : (var_1_19))); } else { var_1_61 = ((((var_1_65) < (var_1_46)) ? (var_1_65) : (var_1_46))); } } var_1_101 = (var_1_61 - var_1_36); signed long int stepLocal_23 = var_1_17 * var_1_96; if (var_1_56) { var_1_63 = (! var_1_58); } else { if ((((((var_1_101) > (32u)) ? (var_1_101) : (32u))) | var_1_76) > stepLocal_23) { var_1_63 = (! var_1_64); } } if (var_1_63) { var_1_106 = var_1_107; } else { var_1_106 = var_1_46; } if (var_1_63) { var_1_110 = var_1_46; } if (var_1_63) { var_1_111 = var_1_98; } else { var_1_111 = var_1_103; } unsigned long int stepLocal_12 = (((var_1_8) > (var_1_32)) ? (var_1_8) : (var_1_32)); unsigned char stepLocal_11 = var_1_109; unsigned long int stepLocal_10 = var_1_31 - ((((var_1_59) < 0 ) ? -(var_1_59) : (var_1_59))); if (stepLocal_10 <= (var_1_32 - ((((var_1_19) > (200u)) ? (var_1_19) : (200u))))) { if (((((var_1_33) > (var_1_69)) ? (var_1_33) : (var_1_69))) >= stepLocal_12) { if (stepLocal_11 && var_1_63) { var_1_30 = var_1_5; } } else { var_1_30 = var_1_15; } } else { var_1_30 = var_1_5; } if (var_1_5 >= ((var_1_38 * var_1_15) + var_1_6)) { var_1_42 = ((((((((((((var_1_17) < (var_1_19)) ? (var_1_17) : (var_1_19)))) > (var_1_18)) ? (((((var_1_17) < (var_1_19)) ? (var_1_17) : (var_1_19)))) : (var_1_18)))) > (((-10 + 8) + var_1_43))) ? (((((((((var_1_17) < (var_1_19)) ? (var_1_17) : (var_1_19)))) > (var_1_18)) ? (((((var_1_17) < (var_1_19)) ? (var_1_17) : (var_1_19)))) : (var_1_18)))) : (((-10 + 8) + var_1_43)))); } else { if (var_1_88) { if (var_1_22 != var_1_30) { if ((var_1_26 + var_1_92) <= var_1_38) { if (var_1_88) { var_1_42 = (((((var_1_18) > (var_1_17)) ? (var_1_18) : (var_1_17))) - (var_1_44 - ((((var_1_19) > (var_1_45)) ? (var_1_19) : (var_1_45))))); } } } else { var_1_42 = ((var_1_44 - var_1_19) - ((var_1_18 - var_1_46) + var_1_45)); } } else { var_1_42 = var_1_44; } } signed long int stepLocal_19 = var_1_28 ^ var_1_17; if (stepLocal_19 > ((var_1_31 * var_1_110) / ((((var_1_54) < (var_1_12)) ? (var_1_54) : (var_1_12))))) { var_1_53 = var_1_38; } signed long int stepLocal_24 = var_1_101; if (stepLocal_24 > ((var_1_67 + var_1_68) - var_1_59)) { var_1_66 = var_1_17; } signed long int stepLocal_32 = -10 + var_1_61; if (var_1_1 > ((- var_1_26) * 7.75)) { if (! var_1_58) { if (var_1_66 > stepLocal_32) { var_1_116 = ((((var_1_34) < (var_1_43)) ? (var_1_34) : (var_1_43))); } else { var_1_116 = var_1_99; } } else { var_1_116 = var_1_36; } } signed long int stepLocal_5 = (((var_1_106) < (var_1_90)) ? (var_1_106) : (var_1_90)); if (stepLocal_5 > 8u) { var_1_16 = (10 + (var_1_17 + (var_1_18 - var_1_19))); } signed long int stepLocal_15 = ((((var_1_110 ^ var_1_18)) < (var_1_16)) ? ((var_1_110 ^ var_1_18)) : (var_1_16)); unsigned char stepLocal_14 = var_1_24 != var_1_74; if (var_1_6 > (- var_1_100)) { var_1_40 = (var_1_29 - 2); } else { if (stepLocal_15 < (last_1_var_1_40 / var_1_36)) { var_1_40 = (((((var_1_19 - var_1_34)) > (var_1_17)) ? ((var_1_19 - var_1_34)) : (var_1_17))); } else { if (stepLocal_14 && (var_1_109 && var_1_109)) { var_1_40 = ((((var_1_19) > (var_1_17)) ? (var_1_19) : (var_1_17))); } else { var_1_40 = var_1_18; } } } signed char stepLocal_29 = var_1_44; signed char stepLocal_28 = var_1_44; signed long int stepLocal_27 = var_1_61; unsigned short int stepLocal_26 = var_1_76; if (10.8 <= var_1_74) { if ((((((var_1_92 + var_1_25)) < ((var_1_100 + var_1_39))) ? ((var_1_92 + var_1_25)) : ((var_1_100 + var_1_39)))) < ((((var_1_37) > (var_1_74)) ? (var_1_37) : (var_1_74)))) { if ((var_1_112 - (var_1_110 + last_1_var_1_82)) != stepLocal_28) { if ((var_1_18 * var_1_65) < stepLocal_27) { if (stepLocal_29 >= (16 << last_1_var_1_82)) { var_1_82 = (((var_1_60 + var_1_81) - var_1_76) + var_1_43); } } else { if (var_1_22 <= var_1_74) { var_1_82 = var_1_62; } else { if (stepLocal_26 < (var_1_59 & var_1_113)) { if (! var_1_64) { var_1_82 = (((((var_1_60) > (var_1_19)) ? (var_1_60) : (var_1_19))) - 64); } else { var_1_82 = (var_1_70 - (var_1_86 - var_1_112)); } } else { var_1_82 = (var_1_80 - var_1_78); } } } } else { var_1_82 = ((32 + ((((var_1_106) < 0 ) ? -(var_1_106) : (var_1_106)))) + (last_1_var_1_82 - 100)); } } else { var_1_82 = var_1_98; } } else { var_1_82 = (((((var_1_79 - var_1_98)) > (var_1_40)) ? ((var_1_79 - var_1_98)) : (var_1_40))); } if (((var_1_36 - var_1_18) - var_1_19) <= var_1_34) { if (var_1_29 < ((16 * var_1_52) & var_1_66)) { var_1_35 = (var_1_26 - 25.25f); } else { var_1_35 = (var_1_15 + var_1_25); } } else { var_1_35 = (var_1_25 + (((((var_1_37) < (var_1_38)) ? (var_1_37) : (var_1_38))) - var_1_39)); } signed long int stepLocal_17 = (var_1_82 * var_1_29) * (var_1_16 + var_1_19); unsigned char stepLocal_16 = var_1_88; if ((64 << var_1_28) <= stepLocal_17) { if (var_1_88 || stepLocal_16) { if (var_1_88) { var_1_49 = (((((var_1_50 - var_1_46)) < ((var_1_51 - var_1_59))) ? ((var_1_50 - var_1_46)) : ((var_1_51 - var_1_59)))); } else { if (255.875f <= (var_1_38 - var_1_26)) { var_1_49 = (3362325572u - var_1_19); } } } else { var_1_49 = var_1_103; } } else { var_1_49 = (var_1_51 - var_1_103); } } void updateVariables() { 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.036854765600e+12F && var_1_5 >= 1.0e-20F )); var_1_6 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_6 >= 0.0F && var_1_6 <= -1.0e-20F) || (var_1_6 <= 9223372.036854765600e+12F && var_1_6 >= 1.0e-20F )); var_1_7 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_7 >= -461168.6018427382800e+13F && var_1_7 <= -1.0e-20F) || (var_1_7 <= 4611686.018427382800e+12F && var_1_7 >= 1.0e-20F )); var_1_12 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_12 >= 0); assume_abort_if_not(var_1_12 <= 4294967295); assume_abort_if_not(var_1_12 != 0); 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_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 >= 31); 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 <= 31); var_1_24 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_24 >= -461168.6018427382800e+13F && var_1_24 <= -1.0e-20F) || (var_1_24 <= 4611686.018427382800e+12F && var_1_24 >= 1.0e-20F )); var_1_25 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_25 >= -461168.6018427382800e+13F && var_1_25 <= -1.0e-20F) || (var_1_25 <= 4611686.018427382800e+12F && var_1_25 >= 1.0e-20F )); var_1_26 = __VERIFIER_nondet_float(); assume_abort_if_not((var_1_26 >= 0.0F && var_1_26 <= -1.0e-20F) || (var_1_26 <= 9223372.036854765600e+12F && var_1_26 >= 1.0e-20F )); var_1_29 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_29 >= 0); assume_abort_if_not(var_1_29 <= 127); var_1_31 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_31 >= 2147483647); assume_abort_if_not(var_1_31 <= 4294967295); var_1_32 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_32 >= 2147483647); assume_abort_if_not(var_1_32 <= 4294967295); var_1_34 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_34 >= 127); assume_abort_if_not(var_1_34 <= 255); var_1_36 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_36 >= 49151); assume_abort_if_not(var_1_36 <= 65535); var_1_37 = __VERIFIER_nondet_float(); 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_float(); 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_float(); 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_43 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_43 >= -63); assume_abort_if_not(var_1_43 <= 63); var_1_44 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_44 >= 63); assume_abort_if_not(var_1_44 <= 126); var_1_45 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_45 >= 0); assume_abort_if_not(var_1_45 <= 63); var_1_46 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_46 >= 0); assume_abort_if_not(var_1_46 <= 31); var_1_50 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_50 >= 2147483647); assume_abort_if_not(var_1_50 <= 4294967294); var_1_51 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_51 >= 2147483647); assume_abort_if_not(var_1_51 <= 4294967294); var_1_54 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_54 >= 0); assume_abort_if_not(var_1_54 <= 4294967295); assume_abort_if_not(var_1_54 != 0); var_1_57 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_57 >= 1); assume_abort_if_not(var_1_57 <= 1); var_1_58 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_58 >= 1); assume_abort_if_not(var_1_58 <= 1); var_1_60 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_60 >= 0); assume_abort_if_not(var_1_60 <= 254); var_1_64 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_64 >= 0); assume_abort_if_not(var_1_64 <= 0); var_1_67 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_67 >= 1073741823); assume_abort_if_not(var_1_67 <= 2147483648); var_1_68 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_68 >= 1073741824); assume_abort_if_not(var_1_68 <= 2147483647); var_1_70 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_70 >= 127); assume_abort_if_not(var_1_70 <= 254); var_1_72 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_72 >= -230584.3009213691390e+13F && var_1_72 <= -1.0e-20F) || (var_1_72 <= 2305843.009213691390e+12F && var_1_72 >= 1.0e-20F )); var_1_73 = __VERIFIER_nondet_double(); assume_abort_if_not((var_1_73 >= -230584.3009213691390e+13F && var_1_73 <= -1.0e-20F) || (var_1_73 <= 2305843.009213691390e+12F && var_1_73 >= 1.0e-20F )); var_1_78 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_78 >= 32767); assume_abort_if_not(var_1_78 <= 65534); var_1_79 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_79 >= 8191); assume_abort_if_not(var_1_79 <= 16383); var_1_80 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_80 >= 49150); assume_abort_if_not(var_1_80 <= 65534); var_1_81 = __VERIFIER_nondet_ushort(); assume_abort_if_not(var_1_81 >= 16383); assume_abort_if_not(var_1_81 <= 32767); var_1_86 = __VERIFIER_nondet_long(); assume_abort_if_not(var_1_86 >= 1073741823); assume_abort_if_not(var_1_86 <= 2147483646); var_1_91 = __VERIFIER_nondet_uchar(); assume_abort_if_not(var_1_91 >= 0); assume_abort_if_not(var_1_91 <= 31); var_1_94 = __VERIFIER_nondet_ulong(); assume_abort_if_not(var_1_94 >= 3221225470); assume_abort_if_not(var_1_94 <= 4294967294); var_1_97 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_97 >= -1); assume_abort_if_not(var_1_97 <= 126); var_1_99 = __VERIFIER_nondet_short(); assume_abort_if_not(var_1_99 >= 16382); assume_abort_if_not(var_1_99 <= 32766); var_1_107 = __VERIFIER_nondet_char(); assume_abort_if_not(var_1_107 >= -127); assume_abort_if_not(var_1_107 <= 126); } void updateLastVariables() { last_1_var_1_1 = var_1_1; last_1_var_1_8 = var_1_8; last_1_var_1_13 = var_1_13; last_1_var_1_20 = var_1_20; last_1_var_1_40 = var_1_40; last_1_var_1_47 = var_1_47; last_1_var_1_49 = var_1_49; last_1_var_1_52 = var_1_52; last_1_var_1_56 = var_1_56; last_1_var_1_59 = var_1_59; last_1_var_1_63 = var_1_63; last_1_var_1_76 = var_1_76; last_1_var_1_82 = var_1_82; last_1_var_1_88 = var_1_88; last_1_var_1_98 = var_1_98; last_1_var_1_101 = var_1_101; last_1_var_1_111 = var_1_111; } int property() { return ((((((((((((((((((((((((((((((((((((((((((((((((((((((var_1_75 <= var_1_90) ? (var_1_1 == ((float) (var_1_5 - var_1_6))) : (var_1_1 == ((float) (10.5f + var_1_7)))) && ((var_1_5 >= var_1_6) ? ((last_1_var_1_8 < var_1_96) ? (var_1_8 == ((unsigned long int) (((((var_1_96 + ((((last_1_var_1_8) > (var_1_28)) ? (last_1_var_1_8) : (var_1_28))))) > ((var_1_90 + var_1_59))) ? ((var_1_96 + ((((last_1_var_1_8) > (var_1_28)) ? (last_1_var_1_8) : (var_1_28))))) : ((var_1_90 + var_1_59)))))) : (var_1_8 == ((unsigned long int) (var_1_59 + var_1_28)))) : ((var_1_59 > (var_1_96 / var_1_12)) ? (var_1_8 == ((unsigned long int) last_1_var_1_8)) : (var_1_8 == ((unsigned long int) (last_1_var_1_8 + ((((var_1_90) < 0 ) ? -(var_1_90) : (var_1_90))))))))) && ((var_1_28 >= (10u / var_1_12)) ? ((var_1_28 < ((((var_1_8) < (var_1_28)) ? (var_1_8) : (var_1_28)))) ? (var_1_13 == ((float) var_1_7)) : (var_1_13 == ((float) (var_1_7 + var_1_15)))) : (var_1_13 == ((float) var_1_15)))) && ((((((var_1_106) < (var_1_90)) ? (var_1_106) : (var_1_90))) > 8u) ? (var_1_16 == ((unsigned char) (10 + (var_1_17 + (var_1_18 - var_1_19))))) : 1)) && ((((((var_1_12) < (var_1_76)) ? (var_1_12) : (var_1_76))) < var_1_59) ? (var_1_109 ? (var_1_20 == ((signed short int) var_1_19)) : 1) : (var_1_20 == ((signed short int) ((((var_1_18) < (var_1_17)) ? (var_1_18) : (var_1_17))))))) && (var_1_21 == ((float) (var_1_15 + var_1_7)))) && ((var_1_92 >= var_1_92) ? (var_1_109 ? (var_1_22 == ((float) (((((var_1_15) < (var_1_7)) ? (var_1_15) : (var_1_7))) + ((((((((var_1_24) < (9.125f)) ? (var_1_24) : (9.125f)))) > (var_1_25)) ? (((((var_1_24) < (9.125f)) ? (var_1_24) : (9.125f)))) : (var_1_25)))))) : (var_1_22 == ((float) (((((var_1_15 + var_1_7)) > (((((0.4f) > ((var_1_5 - var_1_26))) ? (0.4f) : ((var_1_5 - var_1_26)))))) ? ((var_1_15 + var_1_7)) : (((((0.4f) > ((var_1_5 - var_1_26))) ? (0.4f) : ((var_1_5 - var_1_26)))))))))) : (((- var_1_112) > ((var_1_59 * var_1_19) * var_1_69)) ? (((var_1_28 < var_1_69) && var_1_56) ? (var_1_22 == ((float) ((((var_1_7) < (var_1_26)) ? (var_1_7) : (var_1_26))))) : ((var_1_26 >= (var_1_6 - var_1_5)) ? (var_1_22 == ((float) var_1_15)) : (var_1_56 ? (var_1_22 == ((float) var_1_24)) : (var_1_22 == ((float) 4.625f))))) : 1))) && ((! last_1_var_1_88) ? ((var_1_15 == (var_1_5 + last_1_var_1_1)) ? (var_1_28 == ((unsigned char) (var_1_29 + ((((var_1_17) > ((64 - var_1_19))) ? (var_1_17) : ((64 - var_1_19))))))) : (var_1_28 == ((unsigned char) var_1_29))) : ((((((last_1_var_1_111) > (last_1_var_1_49)) ? (last_1_var_1_111) : (last_1_var_1_49))) >= var_1_19) ? (var_1_28 == ((unsigned char) ((((var_1_17) < 0 ) ? -(var_1_17) : (var_1_17))))) : (var_1_28 == ((unsigned char) (var_1_29 + var_1_17)))))) && (((var_1_31 - ((((var_1_59) < 0 ) ? -(var_1_59) : (var_1_59)))) <= (var_1_32 - ((((var_1_19) > (200u)) ? (var_1_19) : (200u))))) ? ((((((var_1_33) > (var_1_69)) ? (var_1_33) : (var_1_69))) >= ((((var_1_8) > (var_1_32)) ? (var_1_8) : (var_1_32)))) ? ((var_1_109 && var_1_63) ? (var_1_30 == ((double) var_1_5)) : 1) : (var_1_30 == ((double) var_1_15))) : (var_1_30 == ((double) var_1_5)))) && (((10 / var_1_12) == var_1_18) ? (var_1_33 == ((unsigned char) (var_1_29 + var_1_19))) : 1)) && ((((var_1_36 - var_1_18) - var_1_19) <= var_1_34) ? ((var_1_29 < ((16 * var_1_52) & var_1_66)) ? (var_1_35 == ((float) (var_1_26 - 25.25f))) : (var_1_35 == ((float) (var_1_15 + var_1_25)))) : (var_1_35 == ((float) (var_1_25 + (((((var_1_37) < (var_1_38)) ? (var_1_37) : (var_1_38))) - var_1_39)))))) && ((var_1_6 > (- var_1_100)) ? (var_1_40 == ((signed short int) (var_1_29 - 2))) : (((((((var_1_110 ^ var_1_18)) < (var_1_16)) ? ((var_1_110 ^ var_1_18)) : (var_1_16))) < (last_1_var_1_40 / var_1_36)) ? (var_1_40 == ((signed short int) (((((var_1_19 - var_1_34)) > (var_1_17)) ? ((var_1_19 - var_1_34)) : (var_1_17))))) : (((var_1_24 != var_1_74) && (var_1_109 && var_1_109)) ? (var_1_40 == ((signed short int) ((((var_1_19) > (var_1_17)) ? (var_1_19) : (var_1_17))))) : (var_1_40 == ((signed short int) var_1_18)))))) && ((var_1_5 >= ((var_1_38 * var_1_15) + var_1_6)) ? (var_1_42 == ((signed char) ((((((((((((var_1_17) < (var_1_19)) ? (var_1_17) : (var_1_19)))) > (var_1_18)) ? (((((var_1_17) < (var_1_19)) ? (var_1_17) : (var_1_19)))) : (var_1_18)))) > (((-10 + 8) + var_1_43))) ? (((((((((var_1_17) < (var_1_19)) ? (var_1_17) : (var_1_19)))) > (var_1_18)) ? (((((var_1_17) < (var_1_19)) ? (var_1_17) : (var_1_19)))) : (var_1_18)))) : (((-10 + 8) + var_1_43)))))) : (var_1_88 ? ((var_1_22 != var_1_30) ? (((var_1_26 + var_1_92) <= var_1_38) ? (var_1_88 ? (var_1_42 == ((signed char) (((((var_1_18) > (var_1_17)) ? (var_1_18) : (var_1_17))) - (var_1_44 - ((((var_1_19) > (var_1_45)) ? (var_1_19) : (var_1_45))))))) : 1) : 1) : (var_1_42 == ((signed char) ((var_1_44 - var_1_19) - ((var_1_18 - var_1_46) + var_1_45))))) : (var_1_42 == ((signed char) var_1_44))))) && (((- var_1_28) < last_1_var_1_47) ? ((((var_1_29 - var_1_19) + -5) > (var_1_65 - var_1_45)) ? (var_1_47 == ((signed short int) var_1_45)) : ((! var_1_56) ? (var_1_47 == ((signed short int) (var_1_18 - var_1_46))) : (var_1_47 == ((signed short int) (((((var_1_17 + ((((var_1_115) < (var_1_115)) ? (var_1_115) : (var_1_115))))) < (var_1_45)) ? ((var_1_17 + ((((var_1_115) < (var_1_115)) ? (var_1_115) : (var_1_115))))) : (var_1_45))))))) : 1)) && (((64 << var_1_28) <= ((var_1_82 * var_1_29) * (var_1_16 + var_1_19))) ? ((var_1_88 || var_1_88) ? (var_1_88 ? (var_1_49 == ((unsigned long int) (((((var_1_50 - var_1_46)) < ((var_1_51 - var_1_59))) ? ((var_1_50 - var_1_46)) : ((var_1_51 - var_1_59)))))) : ((255.875f <= (var_1_38 - var_1_26)) ? (var_1_49 == ((unsigned long int) (3362325572u - var_1_19))) : 1)) : (var_1_49 == ((unsigned long int) var_1_103))) : (var_1_49 == ((unsigned long int) (var_1_51 - var_1_103))))) && ((var_1_6 != var_1_22) ? (var_1_52 == ((unsigned long int) var_1_36)) : (((~ var_1_44) < (var_1_12 & var_1_45)) ? (var_1_52 == ((unsigned long int) ((((var_1_44) > (var_1_96)) ? (var_1_44) : (var_1_96))))) : 1))) && (((var_1_28 ^ var_1_17) > ((var_1_31 * var_1_110) / ((((var_1_54) < (var_1_12)) ? (var_1_54) : (var_1_12))))) ? (var_1_53 == ((float) var_1_38)) : 1)) && (var_1_56 ? (var_1_55 == ((double) (var_1_37 + ((((var_1_24) < (var_1_15)) ? (var_1_24) : (var_1_15)))))) : 1)) && ((last_1_var_1_1 > ((((var_1_5) > (var_1_38)) ? (var_1_5) : (var_1_38)))) ? (var_1_56 == ((unsigned char) var_1_57)) : ((((last_1_var_1_52 * var_1_54) / (var_1_44 + var_1_18)) <= last_1_var_1_101) ? (var_1_56 == ((unsigned char) var_1_57)) : (var_1_56 == ((unsigned char) (var_1_57 && var_1_58)))))) && ((last_1_var_1_76 <= var_1_36) ? ((last_1_var_1_63 || last_1_var_1_56) ? (var_1_59 == ((unsigned char) ((((var_1_60) > (((((var_1_29) < (0)) ? (var_1_29) : (0))))) ? (var_1_60) : (((((var_1_29) < (0)) ? (var_1_29) : (0)))))))) : ((var_1_17 >= last_1_var_1_59) ? (var_1_59 == ((unsigned char) ((((var_1_46) > (var_1_17)) ? (var_1_46) : (var_1_17))))) : 1)) : (var_1_59 == ((unsigned char) (var_1_46 + var_1_18))))) && ((var_1_46 < ((-50 + var_1_115) + ((((var_1_29) < 0 ) ? -(var_1_29) : (var_1_29))))) ? (var_1_61 == ((signed long int) (var_1_34 - var_1_93))) : (((var_1_69 >> var_1_46) > (var_1_18 + ((((var_1_54) < (var_1_60)) ? (var_1_54) : (var_1_60))))) ? (var_1_61 == ((signed long int) (((((((((var_1_18 - 4)) > (var_1_104)) ? ((var_1_18 - 4)) : (var_1_104)))) < (var_1_19)) ? ((((((var_1_18 - 4)) > (var_1_104)) ? ((var_1_18 - 4)) : (var_1_104)))) : (var_1_19))))) : (var_1_61 == ((signed long int) ((((var_1_65) < (var_1_46)) ? (var_1_65) : (var_1_46)))))))) && (var_1_62 == ((signed char) (var_1_19 - var_1_17)))) && (var_1_56 ? (var_1_63 == ((unsigned char) (! var_1_58))) : (((((((var_1_101) > (32u)) ? (var_1_101) : (32u))) | var_1_76) > (var_1_17 * var_1_96)) ? (var_1_63 == ((unsigned char) (! var_1_64))) : 1))) && (var_1_65 == ((unsigned short int) (var_1_17 + 1)))) && ((var_1_101 > ((var_1_67 + var_1_68) - var_1_59)) ? (var_1_66 == ((unsigned char) var_1_17)) : 1)) && ((var_1_65 > (var_1_18 * var_1_67)) ? (var_1_69 == ((unsigned char) (((((var_1_70 - var_1_17)) > (var_1_46)) ? ((var_1_70 - var_1_17)) : (var_1_46))))) : (var_1_69 == ((unsigned char) ((((var_1_46) > ((var_1_70 - var_1_17))) ? (var_1_46) : ((var_1_70 - var_1_17)))))))) && ((var_1_33 < var_1_69) ? (var_1_71 == ((double) ((var_1_72 + var_1_73) + var_1_39))) : (var_1_71 == ((double) (var_1_24 + var_1_7))))) && (var_1_88 ? (((var_1_33 * var_1_69) == var_1_69) ? (((! (var_1_114 > var_1_7)) || (var_1_64 || var_1_58)) ? (var_1_74 == ((double) 31.65)) : 1) : 1) : (var_1_74 == ((double) ((((31.75) > (0.25)) ? (31.75) : (0.25))))))) && ((var_1_39 != (var_1_38 - 4.25f)) ? (var_1_75 == ((signed char) ((((((((var_1_46) > (var_1_17)) ? (var_1_46) : (var_1_17)))) < (((var_1_45 + var_1_18) - var_1_19))) ? (((((var_1_46) > (var_1_17)) ? (var_1_46) : (var_1_17)))) : (((var_1_45 + var_1_18) - var_1_19)))))) : 1)) && ((var_1_6 <= last_1_var_1_13) ? (var_1_76 == ((unsigned short int) (var_1_78 - (last_1_var_1_20 + (var_1_79 - 4))))) : (var_1_76 == ((unsigned short int) ((var_1_80 - var_1_46) - (var_1_81 - 10)))))) && ((10.8 <= var_1_74) ? (((((((var_1_92 + var_1_25)) < ((var_1_100 + var_1_39))) ? ((var_1_92 + var_1_25)) : ((var_1_100 + var_1_39)))) < ((((var_1_37) > (var_1_74)) ? (var_1_37) : (var_1_74)))) ? (((var_1_112 - (var_1_110 + last_1_var_1_82)) != var_1_44) ? (((var_1_18 * var_1_65) < var_1_61) ? ((var_1_44 >= (16 << last_1_var_1_82)) ? (var_1_82 == ((signed long int) (((var_1_60 + var_1_81) - var_1_76) + var_1_43))) : 1) : ((var_1_22 <= var_1_74) ? (var_1_82 == ((signed long int) var_1_62)) : ((var_1_76 < (var_1_59 & var_1_113)) ? ((! var_1_64) ? (var_1_82 == ((signed long int) (((((var_1_60) > (var_1_19)) ? (var_1_60) : (var_1_19))) - 64))) : (var_1_82 == ((signed long int) (var_1_70 - (var_1_86 - var_1_112))))) : (var_1_82 == ((signed long int) (var_1_80 - var_1_78)))))) : (var_1_82 == ((signed long int) ((32 + ((((var_1_106) < 0 ) ? -(var_1_106) : (var_1_106)))) + (last_1_var_1_82 - 100))))) : (var_1_82 == ((signed long int) var_1_98))) : (var_1_82 == ((signed long int) (((((var_1_79 - var_1_98)) > (var_1_40)) ? ((var_1_79 - var_1_98)) : (var_1_40))))))) && (((! var_1_58) && var_1_56) ? (var_1_88 == ((unsigned char) (var_1_57 && var_1_58))) : 1)) && ((last_1_var_1_13 < var_1_15) ? (var_1_90 == ((unsigned char) (var_1_70 - (var_1_19 + (var_1_46 + var_1_91))))) : 1)) && ((var_1_112 < var_1_68) ? (var_1_92 == ((double) ((((var_1_25) < (var_1_24)) ? (var_1_25) : (var_1_24))))) : (var_1_92 == ((double) ((((9999999.2) > (var_1_26)) ? (9999999.2) : (var_1_26))))))) && (var_1_93 == ((unsigned long int) (((((var_1_94 - var_1_80) - var_1_78) < 0 ) ? -((var_1_94 - var_1_80) - var_1_78) : ((var_1_94 - var_1_80) - var_1_78)))))) && ((! ((var_1_51 / var_1_44) > (~ var_1_68))) ? (var_1_95 == ((float) (((((var_1_26 - var_1_38)) < (var_1_7)) ? ((var_1_26 - var_1_38)) : (var_1_7))))) : 1)) && ((var_1_69 > var_1_19) ? (var_1_96 == ((signed char) ((((var_1_18) > ((var_1_97 - (var_1_44 - var_1_19)))) ? (var_1_18) : ((var_1_97 - (var_1_44 - var_1_19))))))) : ((var_1_33 > var_1_51) ? ((var_1_91 < var_1_94) ? (var_1_96 == ((signed char) ((((((((var_1_45) < (var_1_91)) ? (var_1_45) : (var_1_91)))) < ((((((var_1_46 - var_1_17)) < (var_1_19)) ? ((var_1_46 - var_1_17)) : (var_1_19))))) ? (((((var_1_45) < (var_1_91)) ? (var_1_45) : (var_1_91)))) : ((((((var_1_46 - var_1_17)) < (var_1_19)) ? ((var_1_46 - var_1_17)) : (var_1_19)))))))) : (var_1_96 == ((signed char) (((((((((-8) < (10)) ? (-8) : (10)))) < (var_1_46)) ? (((((-8) < (10)) ? (-8) : (10)))) : (var_1_46))) + var_1_19)))) : (var_1_96 == ((signed char) (var_1_45 + var_1_91)))))) && (((var_1_69 / ((((var_1_68) > (var_1_79)) ? (var_1_68) : (var_1_79)))) == var_1_17) ? (var_1_98 == ((signed short int) var_1_79)) : (var_1_109 ? (var_1_98 == ((signed short int) ((((last_1_var_1_98) > (((var_1_99 - 128) - var_1_70))) ? (last_1_var_1_98) : (((var_1_99 - 128) - var_1_70)))))) : (var_1_98 == ((signed short int) ((((-32) < ((var_1_60 + var_1_79))) ? (-32) : ((var_1_60 + var_1_79))))))))) && (var_1_88 ? (var_1_100 == ((double) (((((var_1_6 - var_1_5)) < (((((var_1_73) < (var_1_39)) ? (var_1_73) : (var_1_39))))) ? ((var_1_6 - var_1_5)) : (((((var_1_73) < (var_1_39)) ? (var_1_73) : (var_1_39)))))))) : 1)) && (var_1_101 == ((signed long int) (var_1_61 - var_1_36)))) && (var_1_102 == ((double) var_1_5))) && (var_1_109 ? (var_1_103 == ((signed long int) var_1_96)) : (var_1_103 == ((signed long int) -256)))) && (var_1_109 ? (var_1_104 == ((signed short int) 5)) : (var_1_104 == ((signed short int) var_1_36)))) && (var_1_105 == ((signed long int) var_1_86))) && (var_1_63 ? (var_1_106 == ((signed char) var_1_107)) : (var_1_106 == ((signed char) var_1_46)))) && (var_1_108 == ((unsigned char) var_1_18))) && (var_1_109 == ((unsigned char) var_1_58))) && (var_1_63 ? (var_1_110 == ((unsigned char) var_1_46)) : 1)) && (var_1_63 ? (var_1_111 == ((unsigned long int) var_1_98)) : (var_1_111 == ((unsigned long int) var_1_103)))) && (var_1_64 ? (var_1_112 == ((unsigned long int) 5u)) : 1)) && (var_1_113 == ((unsigned short int) var_1_99))) && (var_1_114 == ((double) var_1_72))) && (var_1_109 ? (var_1_115 == ((signed char) var_1_18)) : 1)) && ((var_1_1 > ((- var_1_26) * 7.75)) ? ((! var_1_58) ? ((var_1_66 > (-10 + var_1_61)) ? (var_1_116 == ((signed short int) ((((var_1_34) < (var_1_43)) ? (var_1_34) : (var_1_43))))) : (var_1_116 == ((signed short int) var_1_99))) : (var_1_116 == ((signed short int) var_1_36))) : 1) ; } int main(void) { isInitial = 1; initially(); while (1) { updateLastVariables(); updateVariables(); step(); __VERIFIER_assert(property()); isInitial = 0; } return 0; }