// 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_Batch11Amount500.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;
double var_1_1 = 4.75;
signed long int var_1_6 = -4;
double var_1_7 = 49.8;
double var_1_8 = 255.625;
unsigned short int var_1_9 = 10;
double var_1_11 = 127.35;
double var_1_18 = 25.5;
double var_1_19 = 128.2;
double var_1_20 = 10.5;
double var_1_21 = 200.25;
unsigned char var_1_22 = 128;
unsigned char var_1_23 = 32;
unsigned char var_1_24 = 128;
unsigned char var_1_25 = 1;
unsigned char var_1_26 = 2;
unsigned short int var_1_27 = 128;
unsigned char var_1_28 = 8;
unsigned short int var_1_29 = 46798;
unsigned char var_1_30 = 5;
unsigned char var_1_32 = 1;
unsigned char var_1_33 = 0;
unsigned long int var_1_34 = 16;
unsigned long int var_1_35 = 3176649101;
unsigned long int var_1_36 = 2158140991;
float var_1_37 = 49.375;
float var_1_38 = 255.9;
float var_1_39 = 7.55;
float var_1_40 = 10.875;
float var_1_41 = 15.3;
float var_1_42 = 1.5;
float var_1_43 = 199.5;
unsigned long int var_1_44 = 2;
unsigned char var_1_45 = 0;
unsigned char var_1_47 = 0;
signed char var_1_48 = 10;
signed char var_1_49 = -16;
signed char var_1_50 = 5;
signed short int var_1_51 = 25;
signed short int var_1_52 = 64;
unsigned short int var_1_53 = 1;
unsigned char var_1_54 = 2;
unsigned short int var_1_56 = 10000;
unsigned short int var_1_57 = 4;
float var_1_58 = 64.3;
float var_1_59 = 0.0;
unsigned short int var_1_60 = 25;
unsigned short int var_1_61 = 63259;
unsigned short int var_1_62 = 50628;
signed long int var_1_63 = 1000000000;
unsigned char var_1_64 = 1;
unsigned char var_1_65 = 0;
float var_1_66 = 0.4;
float var_1_67 = 0.0;
float var_1_68 = 0.0;
float var_1_69 = 99.25;
unsigned short int var_1_70 = 25;
unsigned short int var_1_71 = 19833;
signed short int var_1_72 = -1;
unsigned long int var_1_73 = 25;
unsigned long int var_1_74 = 1116524111;
unsigned long int var_1_75 = 1659880762;
double var_1_76 = 63.2;
float var_1_77 = 63.6;
double var_1_78 = 1000.8;
signed long int var_1_80 = 0;
signed char var_1_81 = 25;
signed char var_1_82 = 4;
signed char var_1_83 = -8;
signed char var_1_84 = -32;
signed short int var_1_85 = -25;
double var_1_86 = 64.25;
signed short int var_1_87 = 16;
unsigned char var_1_88 = 1;
unsigned char var_1_91 = 5;
unsigned char var_1_93 = 0;
double var_1_94 = 31.5;
double var_1_95 = 3.75;
unsigned char var_1_96 = 8;
unsigned char var_1_97 = 1;
double var_1_98 = 1000000000000000.6;
unsigned long int var_1_99 = 8;
signed char var_1_100 = -128;
unsigned char var_1_101 = 1;
double var_1_102 = 31.25;
float var_1_103 = 31.75;
unsigned char var_1_104 = 5;
unsigned char var_1_105 = 1;
unsigned char var_1_106 = 128;
unsigned char var_1_107 = 0;
signed long int var_1_108 = -5;
signed char var_1_109 = 0;
signed long int var_1_110 = -25;
float var_1_111 = 127.8;
unsigned short int var_1_112 = 256;
signed char var_1_114 = 4;
float var_1_115 = 4.4;
unsigned short int last_1_var_1_9 = 10;
double last_1_var_1_18 = 25.5;
unsigned char last_1_var_1_22 = 128;
unsigned short int last_1_var_1_27 = 128;
unsigned char last_1_var_1_30 = 5;
unsigned char last_1_var_1_32 = 1;
unsigned long int last_1_var_1_44 = 2;
signed short int last_1_var_1_51 = 25;
unsigned char last_1_var_1_54 = 2;
unsigned short int last_1_var_1_57 = 4;
unsigned short int last_1_var_1_70 = 25;
double last_1_var_1_78 = 1000.8;
signed short int last_1_var_1_87 = 16;
unsigned char last_1_var_1_91 = 5;
double last_1_var_1_94 = 31.5;
double last_1_var_1_95 = 3.75;
unsigned char last_1_var_1_104 = 5;
unsigned char last_1_var_1_106 = 128;
signed long int last_1_var_1_108 = -5;
signed long int last_1_var_1_110 = -25;
void initially(void) {
}
void step(void) {
 if (last_1_var_1_91 > last_1_var_1_9) {
  if (last_1_var_1_18 < var_1_7) {
   var_1_9 = last_1_var_1_104;
  }
 } else {
  if (var_1_7 == ((- last_1_var_1_18) / var_1_11)) {
   if ((last_1_var_1_104 / var_1_6) == last_1_var_1_9) {
    if (((((- var_1_6) < 0 ) ? -(- var_1_6) : (- var_1_6))) <= -200) {
     var_1_9 = ((((((last_1_var_1_30 + last_1_var_1_30) + last_1_var_1_54)) < (last_1_var_1_104)) ? (((last_1_var_1_30 + last_1_var_1_30) + last_1_var_1_54)) : (last_1_var_1_104)));
    } else {
     var_1_9 = (48910 - (((((((last_1_var_1_30) < (last_1_var_1_54)) ? (last_1_var_1_30) : (last_1_var_1_54))) < 0 ) ? -((((last_1_var_1_30) < (last_1_var_1_54)) ? (last_1_var_1_30) : (last_1_var_1_54))) : ((((last_1_var_1_30) < (last_1_var_1_54)) ? (last_1_var_1_30) : (last_1_var_1_54))))));
    }
   } else {
    var_1_9 = (((((last_1_var_1_30) < ((last_1_var_1_30 + last_1_var_1_91))) ? (last_1_var_1_30) : ((last_1_var_1_30 + last_1_var_1_91)))) + ((((last_1_var_1_54) > (last_1_var_1_104)) ? (last_1_var_1_54) : (last_1_var_1_104))));
   }
  }
 }
 unsigned char stepLocal_5 = var_1_28;
 if ((var_1_25 - var_1_24) >= stepLocal_5) {
  var_1_48 = (((((var_1_49) < 0 ) ? -(var_1_49) : (var_1_49))) - var_1_50);
 } else {
  if (! (var_1_9 == var_1_24)) {
   var_1_48 = ((((var_1_49) > (var_1_50)) ? (var_1_49) : (var_1_50)));
  } else {
   var_1_48 = var_1_50;
  }
 }
 if (last_1_var_1_87 >= ((((10) < 0 ) ? -(10) : (10)))) {
  var_1_63 = ((((last_1_var_1_110) > (last_1_var_1_27)) ? (last_1_var_1_110) : (last_1_var_1_27)));
 }
 if (last_1_var_1_94 > (var_1_42 * var_1_43)) {
  var_1_45 = var_1_47;
 } else {
  var_1_45 = (! (last_1_var_1_32 && (! var_1_33)));
 }
 if (var_1_45) {
  var_1_105 = var_1_65;
 } else {
  var_1_105 = var_1_33;
 }
 if (var_1_105) {
  var_1_111 = 3.75f;
 } else {
  var_1_111 = var_1_42;
 }
 signed long int stepLocal_4 = last_1_var_1_104;
 signed long int stepLocal_3 = (50929 - last_1_var_1_30) * last_1_var_1_106;
 signed long int stepLocal_2 = last_1_var_1_91;
 if (stepLocal_2 < (var_1_23 / (var_1_29 - var_1_24))) {
  if (stepLocal_4 < last_1_var_1_54) {
   if (stepLocal_3 > 500) {
    var_1_32 = (! var_1_33);
   }
  }
 } else {
  var_1_32 = ((last_1_var_1_70 >= last_1_var_1_91) || var_1_33);
 }
 if (var_1_32) {
  var_1_102 = var_1_43;
 } else {
  var_1_102 = var_1_8;
 }
 signed long int stepLocal_11 = last_1_var_1_91;
 signed long int stepLocal_10 = last_1_var_1_108;
 unsigned char stepLocal_9 = var_1_33;
 unsigned long int stepLocal_8 = (- var_1_36) + last_1_var_1_104;
 if ((var_1_38 == var_1_43) && stepLocal_9) {
  var_1_54 = var_1_24;
 } else {
  if (stepLocal_11 <= last_1_var_1_57) {
   if ((last_1_var_1_22 / ((((var_1_6) > (var_1_28)) ? (var_1_6) : (var_1_28)))) < stepLocal_10) {
    var_1_54 = (var_1_25 + var_1_50);
   } else {
    if (stepLocal_8 < last_1_var_1_22) {
     var_1_54 = ((((var_1_24) > (var_1_50)) ? (var_1_24) : (var_1_50)));
    } else {
     var_1_54 = (var_1_25 + var_1_50);
    }
   }
  } else {
   var_1_54 = (var_1_24 - var_1_50);
  }
 }
 signed long int stepLocal_29 = -1;
 if ((last_1_var_1_30 << last_1_var_1_22) <= stepLocal_29) {
  if ((last_1_var_1_95 / 5.2) < var_1_11) {
   var_1_91 = (var_1_50 + ((((var_1_82 + var_1_93) < 0 ) ? -(var_1_82 + var_1_93) : (var_1_82 + var_1_93))));
  } else {
   var_1_91 = ((((var_1_23) < (var_1_25)) ? (var_1_23) : (var_1_25)));
  }
 } else {
  var_1_91 = ((((((((var_1_26) < 0 ) ? -(var_1_26) : (var_1_26)))) < (var_1_50)) ? (((((var_1_26) < 0 ) ? -(var_1_26) : (var_1_26)))) : (var_1_50)));
 }
 signed long int stepLocal_1 = last_1_var_1_104;
 if ((last_1_var_1_44 | last_1_var_1_51) >= stepLocal_1) {
  var_1_30 = var_1_25;
 } else {
  var_1_30 = var_1_25;
 }
 if (var_1_39 <= (var_1_38 / var_1_11)) {
  var_1_40 = (var_1_41 - ((3.0717073020876769E18f - var_1_42) + (4.372261890791681E18f - var_1_43)));
 }
 if (var_1_6 < var_1_9) {
  if (var_1_24 > var_1_35) {
   var_1_53 = (var_1_29 - var_1_28);
  }
 } else {
  var_1_53 = ((((var_1_29 - (25162 - var_1_23)) < 0 ) ? -(var_1_29 - (25162 - var_1_23)) : (var_1_29 - (25162 - var_1_23))));
 }
 var_1_100 = var_1_49;
 if (var_1_65) {
  var_1_101 = var_1_33;
 } else {
  var_1_101 = var_1_33;
 }
 var_1_103 = var_1_43;
 var_1_104 = 10;
 if (var_1_65) {
  var_1_106 = var_1_96;
 }
 var_1_107 = var_1_33;
 if (var_1_47) {
  var_1_109 = var_1_84;
 } else {
  var_1_109 = var_1_50;
 }
 var_1_114 = var_1_50;
 var_1_115 = var_1_41;
 if (var_1_105) {
  var_1_99 = var_1_23;
 } else {
  var_1_99 = var_1_29;
 }
 if (var_1_36 > var_1_104) {
  var_1_44 = var_1_30;
 } else {
  var_1_44 = (((((var_1_36) > (var_1_35)) ? (var_1_36) : (var_1_35))) - var_1_54);
 }
 if (var_1_24 < (var_1_25 / ((((var_1_6) > (var_1_28)) ? (var_1_6) : (var_1_28))))) {
  if ((var_1_25 - var_1_26) <= var_1_54) {
   var_1_27 = (var_1_29 - ((((var_1_104) < 0 ) ? -(var_1_104) : (var_1_104))));
  }
 } else {
  var_1_27 = ((((var_1_91) > (var_1_26)) ? (var_1_91) : (var_1_26)));
 }
 unsigned char stepLocal_18 = var_1_47;
 if (var_1_101 || stepLocal_18) {
  var_1_66 = (((var_1_67 + var_1_68) - var_1_43) - (var_1_42 + var_1_69));
 }
 var_1_108 = var_1_44;
 signed long int stepLocal_27 = (((4) < 0 ) ? -(4) : (4));
 signed long int stepLocal_26 = var_1_25 / var_1_29;
 if (stepLocal_26 < (1 - var_1_91)) {
  if (stepLocal_27 <= var_1_27) {
   var_1_81 = ((var_1_82 - 4) + var_1_83);
  } else {
   var_1_81 = (var_1_83 + var_1_82);
  }
 } else {
  var_1_81 = (((((var_1_83) < (var_1_82)) ? (var_1_83) : (var_1_82))) + var_1_84);
 }
 var_1_56 = (var_1_104 + var_1_108);
 if (var_1_104 > var_1_24) {
  var_1_87 = ((var_1_83 + var_1_23) + var_1_108);
 } else {
  var_1_87 = (((((((var_1_9) < (var_1_100)) ? (var_1_9) : (var_1_100))) < 0 ) ? -((((var_1_9) < (var_1_100)) ? (var_1_9) : (var_1_100))) : ((((var_1_9) < (var_1_100)) ? (var_1_9) : (var_1_100)))));
 }
 signed long int stepLocal_17 = (- var_1_81) >> var_1_63;
 if (stepLocal_17 != var_1_30) {
  var_1_64 = (var_1_107 && var_1_47);
 } else {
  var_1_64 = (var_1_101 && (var_1_47 || var_1_65));
 }
 if ((var_1_59 > var_1_19) || var_1_45) {
  var_1_88 = (var_1_47 && var_1_65);
 } else {
  if (var_1_54 <= var_1_56) {
   var_1_88 = ((2.4 < var_1_59) || var_1_33);
  }
 }
 unsigned char stepLocal_12 = var_1_104;
 if (stepLocal_12 >= (last_1_var_1_57 + var_1_87)) {
  var_1_57 = var_1_50;
 } else {
  var_1_57 = (((((var_1_50 + var_1_104)) > (var_1_91)) ? ((var_1_50 + var_1_104)) : (var_1_91)));
 }
 signed long int stepLocal_0 = var_1_6 & 10000;
 if (((var_1_63 + var_1_57) | var_1_44) < stepLocal_0) {
  var_1_1 = var_1_7;
 } else {
  var_1_1 = ((((var_1_7) > (var_1_8)) ? (var_1_7) : (var_1_8)));
 }
 if (var_1_1 >= (var_1_102 + (var_1_67 + var_1_66))) {
  if (var_1_54 <= var_1_104) {
   var_1_86 = ((var_1_43 + var_1_42) + var_1_68);
  } else {
   var_1_86 = ((var_1_43 + var_1_39) + var_1_68);
  }
 }
 signed long int stepLocal_16 = ((((var_1_87) < (var_1_30)) ? (var_1_87) : (var_1_30))) / var_1_28;
 unsigned long int stepLocal_15 = ~ var_1_99;
 unsigned char stepLocal_14 = var_1_54;
 unsigned char stepLocal_13 = var_1_101;
 if (var_1_48 > stepLocal_14) {
  if (var_1_6 != stepLocal_16) {
   var_1_60 = (((((var_1_29) > (var_1_61)) ? (var_1_29) : (var_1_61))) - var_1_28);
  } else {
   if (stepLocal_15 < var_1_54) {
    var_1_60 = ((var_1_62 - ((((var_1_23) < 0 ) ? -(var_1_23) : (var_1_23)))) - var_1_91);
   } else {
    if (var_1_64 || stepLocal_13) {
     var_1_60 = (var_1_62 - 16);
    } else {
     var_1_60 = ((((var_1_54 + 32) < 0 ) ? -(var_1_54 + 32) : (var_1_54 + 32)));
    }
   }
  }
 }
 if (var_1_8 != var_1_102) {
  var_1_72 = (((((var_1_30 - var_1_26)) > (var_1_48)) ? ((var_1_30 - var_1_26)) : (var_1_48)));
 } else {
  if ((var_1_23 != (- var_1_48)) || (var_1_88 || var_1_33)) {
   var_1_72 = var_1_60;
  }
 }
 if (var_1_33) {
  var_1_80 = ((((var_1_63) > ((var_1_72 - var_1_24))) ? (var_1_63) : ((var_1_72 - var_1_24))));
 } else {
  var_1_80 = (var_1_63 + var_1_71);
 }
 signed long int stepLocal_22 = var_1_30 ^ var_1_80;
 if (var_1_111 <= var_1_68) {
  if (stepLocal_22 != var_1_108) {
   var_1_76 = var_1_68;
  }
 }
 if (var_1_32) {
  var_1_110 = var_1_99;
 } else {
  var_1_110 = var_1_60;
 }
 signed short int stepLocal_30 = var_1_72;
 if (var_1_32) {
  if (stepLocal_30 >= (var_1_74 & var_1_30)) {
   var_1_94 = (var_1_69 + var_1_39);
  }
 } else {
  var_1_94 = ((((var_1_67) < (var_1_19)) ? (var_1_67) : (var_1_19)));
 }
 if (var_1_47) {
  var_1_73 = ((((var_1_80) < 0 ) ? -(var_1_80) : (var_1_80)));
 } else {
  var_1_73 = ((((((var_1_74 + var_1_75)) < (var_1_35)) ? ((var_1_74 + var_1_75)) : (var_1_35))) - var_1_50);
 }
 if (var_1_73 >= ((var_1_30 % var_1_24) + var_1_91)) {
  if (var_1_88 || var_1_33) {
   var_1_37 = ((10.2f + ((((99999.75f) < 0 ) ? -(99999.75f) : (99999.75f)))) + (((((var_1_38 + var_1_39)) < (var_1_20)) ? ((var_1_38 + var_1_39)) : (var_1_20))));
  } else {
   var_1_37 = var_1_7;
  }
 }
 if (var_1_24 <= (var_1_110 / var_1_28)) {
  var_1_112 = var_1_104;
 } else {
  var_1_112 = (var_1_61 - var_1_44);
 }
 unsigned long int stepLocal_31 = var_1_73;
 if (! var_1_32) {
  var_1_95 = ((4.75 - var_1_68) + ((((99999.875) < 0 ) ? -(99999.875) : (99999.875))));
 } else {
  if ((var_1_25 >> (var_1_96 - var_1_97)) <= stepLocal_31) {
   var_1_95 = (((((var_1_42) < (var_1_98)) ? (var_1_42) : (var_1_98))) + var_1_39);
  } else {
   var_1_95 = ((var_1_68 + 3.75) - var_1_59);
  }
 }
 if (! var_1_32) {
  if (var_1_19 <= var_1_86) {
   var_1_58 = (var_1_39 + var_1_42);
  }
 } else {
  var_1_58 = ((((((var_1_59 - 255.5f) - var_1_43)) < ((((((25.5f - var_1_42)) < (var_1_41)) ? ((25.5f - var_1_42)) : (var_1_41))))) ? (((var_1_59 - 255.5f) - var_1_43)) : ((((((25.5f - var_1_42)) < (var_1_41)) ? ((25.5f - var_1_42)) : (var_1_41))))));
 }
 if (var_1_76 < (var_1_7 * var_1_11)) {
  var_1_18 = (var_1_19 + var_1_20);
 } else {
  var_1_18 = ((((var_1_21) > (var_1_8)) ? (var_1_21) : (var_1_8)));
 }
 if (var_1_11 <= ((((var_1_115) < (var_1_7)) ? (var_1_115) : (var_1_7)))) {
  if (var_1_45) {
   var_1_22 = ((((var_1_23) < ((var_1_24 - 10))) ? (var_1_23) : ((var_1_24 - 10))));
  } else {
   var_1_22 = ((((((((var_1_23) > ((var_1_24 - var_1_25))) ? (var_1_23) : ((var_1_24 - var_1_25))))) > (var_1_26)) ? (((((var_1_23) > ((var_1_24 - var_1_25))) ? (var_1_23) : ((var_1_24 - var_1_25))))) : (var_1_26)));
  }
 } else {
  if (var_1_8 > var_1_37) {
   var_1_22 = (((((var_1_24 - var_1_25)) > (var_1_23)) ? ((var_1_24 - var_1_25)) : (var_1_23)));
  }
 }
 if (! var_1_45) {
  var_1_34 = (var_1_112 + var_1_29);
 } else {
  var_1_34 = (((((var_1_35) < (var_1_36)) ? (var_1_35) : (var_1_36))) - ((((50u) < (var_1_112)) ? (50u) : (var_1_112))));
 }
 unsigned char stepLocal_7 = var_1_26;
 unsigned char stepLocal_6 = var_1_91;
 if ((var_1_108 / var_1_29) != stepLocal_6) {
  if ((var_1_34 * 32) <= stepLocal_7) {
   if (var_1_88) {
    var_1_52 = (((((var_1_34) < (var_1_106)) ? (var_1_34) : (var_1_106))) - var_1_22);
   } else {
    var_1_52 = (var_1_25 - var_1_23);
   }
  }
 }
 unsigned char stepLocal_21 = var_1_33;
 signed long int stepLocal_20 = 16;
 signed long int stepLocal_19 = var_1_80;
 if (stepLocal_20 < var_1_6) {
  var_1_70 = var_1_50;
 } else {
  if ((var_1_63 * var_1_104) <= stepLocal_19) {
   var_1_70 = ((((((((var_1_54) > (((((var_1_23) < (var_1_61)) ? (var_1_23) : (var_1_61))))) ? (var_1_54) : (((((var_1_23) < (var_1_61)) ? (var_1_23) : (var_1_61))))))) < ((((((62088) > (var_1_29)) ? (62088) : (var_1_29))) - var_1_104))) ? (((((var_1_54) > (((((var_1_23) < (var_1_61)) ? (var_1_23) : (var_1_61))))) ? (var_1_54) : (((((var_1_23) < (var_1_61)) ? (var_1_23) : (var_1_61))))))) : ((((((62088) > (var_1_29)) ? (62088) : (var_1_29))) - var_1_104))));
  } else {
   if (var_1_65) {
    if (var_1_38 > (- (- var_1_19))) {
     var_1_70 = (var_1_104 + (var_1_71 - (var_1_25 + 10)));
    }
   } else {
    if (stepLocal_21 || (var_1_52 > var_1_44)) {
     var_1_70 = ((((var_1_81) > (50)) ? (var_1_81) : (50)));
    } else {
     if (var_1_101) {
      var_1_70 = ((((var_1_106) < 0 ) ? -(var_1_106) : (var_1_106)));
     }
    }
   }
  }
 }
 if (var_1_60 <= var_1_28) {
  if (var_1_88) {
   if (var_1_64) {
    var_1_51 = (((((1000 - var_1_25)) > ((var_1_24 - var_1_22))) ? ((1000 - var_1_25)) : ((var_1_24 - var_1_22))));
   }
  } else {
   var_1_51 = (var_1_23 + var_1_54);
  }
 } else {
  var_1_51 = (((var_1_81 + var_1_28) + -5) + (var_1_104 - var_1_23));
 }
 if ((var_1_21 * var_1_20) <= last_1_var_1_78) {
  if (((var_1_62 * var_1_48) << var_1_70) != var_1_70) {
   var_1_78 = (16.25 - ((((((((var_1_59) < (var_1_43)) ? (var_1_59) : (var_1_43)))) > (var_1_42)) ? (((((var_1_59) < (var_1_43)) ? (var_1_59) : (var_1_43)))) : (var_1_42))));
  } else {
   var_1_78 = ((((var_1_68) > (((((var_1_67) > (((((var_1_69) < 0 ) ? -(var_1_69) : (var_1_69))))) ? (var_1_67) : (((((var_1_69) < 0 ) ? -(var_1_69) : (var_1_69)))))))) ? (var_1_68) : (((((var_1_67) > (((((var_1_69) < 0 ) ? -(var_1_69) : (var_1_69))))) ? (var_1_67) : (((((var_1_69) < 0 ) ? -(var_1_69) : (var_1_69)))))))));
  }
 } else {
  if ((var_1_19 * var_1_1) == var_1_11) {
   var_1_78 = (((((127.75) < 0 ) ? -(127.75) : (127.75))) + var_1_20);
  }
 }
 unsigned char stepLocal_28 = (var_1_8 >= var_1_76) || var_1_32;
 if (stepLocal_28 || var_1_88) {
  var_1_85 = (var_1_28 + var_1_51);
 } else {
  var_1_85 = var_1_82;
 }
 unsigned char stepLocal_25 = var_1_107;
 signed long int stepLocal_24 = var_1_110;
 signed long int stepLocal_23 = ~ var_1_56;
 if ((10u * var_1_85) == stepLocal_24) {
  var_1_77 = (((((var_1_19) < (var_1_67)) ? (var_1_19) : (var_1_67))) + (((((var_1_43) > (var_1_38)) ? (var_1_43) : (var_1_38))) + ((((var_1_42) < (var_1_39)) ? (var_1_42) : (var_1_39)))));
 } else {
  if ((var_1_40 == var_1_86) && stepLocal_25) {
   if (-256 > stepLocal_23) {
    var_1_77 = (var_1_19 + (var_1_43 + ((((var_1_42) < 0 ) ? -(var_1_42) : (var_1_42)))));
   } else {
    var_1_77 = var_1_21;
   }
  } else {
   var_1_77 = ((((var_1_7) < 0 ) ? -(var_1_7) : (var_1_7)));
  }
 }
}
void updateVariables() {
 var_1_6 = __VERIFIER_nondet_long();
 assume_abort_if_not(var_1_6 >= -2147483648);
 assume_abort_if_not(var_1_6 <= 2147483647);
 assume_abort_if_not(var_1_6 != 0);
 var_1_7 = __VERIFIER_nondet_double();
 assume_abort_if_not((var_1_7 >= -922337.2036854765600e+13F && var_1_7 <= -1.0e-20F) || (var_1_7 <= 9223372.036854765600e+12F && var_1_7 >= 1.0e-20F ));
 var_1_8 = __VERIFIER_nondet_double();
 assume_abort_if_not((var_1_8 >= -922337.2036854765600e+13F && var_1_8 <= -1.0e-20F) || (var_1_8 <= 9223372.036854765600e+12F && var_1_8 >= 1.0e-20F ));
 var_1_11 = __VERIFIER_nondet_double();
 assume_abort_if_not((var_1_11 >= -922337.2036854776000e+13F && var_1_11 <= -1.0e-20F) || (var_1_11 <= 9223372.036854776000e+12F && var_1_11 >= 1.0e-20F ));
 assume_abort_if_not(var_1_11 != 0.0F);
 var_1_19 = __VERIFIER_nondet_double();
 assume_abort_if_not((var_1_19 >= -461168.6018427382800e+13F && var_1_19 <= -1.0e-20F) || (var_1_19 <= 4611686.018427382800e+12F && var_1_19 >= 1.0e-20F ));
 var_1_20 = __VERIFIER_nondet_double();
 assume_abort_if_not((var_1_20 >= -461168.6018427382800e+13F && var_1_20 <= -1.0e-20F) || (var_1_20 <= 4611686.018427382800e+12F && var_1_20 >= 1.0e-20F ));
 var_1_21 = __VERIFIER_nondet_double();
 assume_abort_if_not((var_1_21 >= -922337.2036854765600e+13F && var_1_21 <= -1.0e-20F) || (var_1_21 <= 9223372.036854765600e+12F && var_1_21 >= 1.0e-20F ));
 var_1_23 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_23 >= 0);
 assume_abort_if_not(var_1_23 <= 254);
 var_1_24 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_24 >= 127);
 assume_abort_if_not(var_1_24 <= 254);
 var_1_25 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_25 >= 0);
 assume_abort_if_not(var_1_25 <= 127);
 var_1_26 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_26 >= 0);
 assume_abort_if_not(var_1_26 <= 254);
 var_1_28 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_28 >= 0);
 assume_abort_if_not(var_1_28 <= 255);
 assume_abort_if_not(var_1_28 != 0);
 var_1_29 = __VERIFIER_nondet_ushort();
 assume_abort_if_not(var_1_29 >= 32767);
 assume_abort_if_not(var_1_29 <= 65534);
 var_1_33 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_33 >= 1);
 assume_abort_if_not(var_1_33 <= 1);
 var_1_35 = __VERIFIER_nondet_ulong();
 assume_abort_if_not(var_1_35 >= 2147483647);
 assume_abort_if_not(var_1_35 <= 4294967294);
 var_1_36 = __VERIFIER_nondet_ulong();
 assume_abort_if_not(var_1_36 >= 2147483647);
 assume_abort_if_not(var_1_36 <= 4294967294);
 var_1_38 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_38 >= -230584.3009213691390e+13F && var_1_38 <= -1.0e-20F) || (var_1_38 <= 2305843.009213691390e+12F && var_1_38 >= 1.0e-20F ));
 var_1_39 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_39 >= -230584.3009213691390e+13F && var_1_39 <= -1.0e-20F) || (var_1_39 <= 2305843.009213691390e+12F && var_1_39 >= 1.0e-20F ));
 var_1_41 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_41 >= 0.0F && var_1_41 <= -1.0e-20F) || (var_1_41 <= 9223372.036854765600e+12F && var_1_41 >= 1.0e-20F ));
 var_1_42 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_42 >= 0.0F && var_1_42 <= -1.0e-20F) || (var_1_42 <= 2305843.009213691390e+12F && var_1_42 >= 1.0e-20F ));
 var_1_43 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_43 >= 0.0F && var_1_43 <= -1.0e-20F) || (var_1_43 <= 2305843.009213691390e+12F && var_1_43 >= 1.0e-20F ));
 var_1_47 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_47 >= 0);
 assume_abort_if_not(var_1_47 <= 0);
 var_1_49 = __VERIFIER_nondet_char();
 assume_abort_if_not(var_1_49 >= -126);
 assume_abort_if_not(var_1_49 <= 126);
 var_1_50 = __VERIFIER_nondet_char();
 assume_abort_if_not(var_1_50 >= 0);
 assume_abort_if_not(var_1_50 <= 126);
 var_1_59 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_59 >= 4611686.018427382800e+12F && var_1_59 <= -1.0e-20F) || (var_1_59 <= 9223372.036854765600e+12F && var_1_59 >= 1.0e-20F ));
 var_1_61 = __VERIFIER_nondet_ushort();
 assume_abort_if_not(var_1_61 >= 32767);
 assume_abort_if_not(var_1_61 <= 65534);
 var_1_62 = __VERIFIER_nondet_ushort();
 assume_abort_if_not(var_1_62 >= 49150);
 assume_abort_if_not(var_1_62 <= 65534);
 var_1_65 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_65 >= 0);
 assume_abort_if_not(var_1_65 <= 0);
 var_1_67 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_67 >= 2305843.009213691390e+12F && var_1_67 <= -1.0e-20F) || (var_1_67 <= 4611686.018427382800e+12F && var_1_67 >= 1.0e-20F ));
 var_1_68 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_68 >= 2305843.009213691390e+12F && var_1_68 <= -1.0e-20F) || (var_1_68 <= 4611686.018427382800e+12F && var_1_68 >= 1.0e-20F ));
 var_1_69 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_69 >= 0.0F && var_1_69 <= -1.0e-20F) || (var_1_69 <= 4611686.018427382800e+12F && var_1_69 >= 1.0e-20F ));
 var_1_71 = __VERIFIER_nondet_ushort();
 assume_abort_if_not(var_1_71 >= 16383);
 assume_abort_if_not(var_1_71 <= 32767);
 var_1_74 = __VERIFIER_nondet_ulong();
 assume_abort_if_not(var_1_74 >= 1073741823);
 assume_abort_if_not(var_1_74 <= 2147483647);
 var_1_75 = __VERIFIER_nondet_ulong();
 assume_abort_if_not(var_1_75 >= 1073741824);
 assume_abort_if_not(var_1_75 <= 2147483647);
 var_1_82 = __VERIFIER_nondet_char();
 assume_abort_if_not(var_1_82 >= 0);
 assume_abort_if_not(var_1_82 <= 63);
 var_1_83 = __VERIFIER_nondet_char();
 assume_abort_if_not(var_1_83 >= -63);
 assume_abort_if_not(var_1_83 <= 63);
 var_1_84 = __VERIFIER_nondet_char();
 assume_abort_if_not(var_1_84 >= -63);
 assume_abort_if_not(var_1_84 <= 63);
 var_1_93 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_93 >= 0);
 assume_abort_if_not(var_1_93 <= 63);
 var_1_96 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_96 >= 4);
 assume_abort_if_not(var_1_96 <= 9);
 var_1_97 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_97 >= 0);
 assume_abort_if_not(var_1_97 <= 4);
 var_1_98 = __VERIFIER_nondet_double();
 assume_abort_if_not((var_1_98 >= -461168.6018427382800e+13F && var_1_98 <= -1.0e-20F) || (var_1_98 <= 4611686.018427382800e+12F && var_1_98 >= 1.0e-20F ));
}
void updateLastVariables() {
 last_1_var_1_9 = var_1_9;
 last_1_var_1_18 = var_1_18;
 last_1_var_1_22 = var_1_22;
 last_1_var_1_27 = var_1_27;
 last_1_var_1_30 = var_1_30;
 last_1_var_1_32 = var_1_32;
 last_1_var_1_44 = var_1_44;
 last_1_var_1_51 = var_1_51;
 last_1_var_1_54 = var_1_54;
 last_1_var_1_57 = var_1_57;
 last_1_var_1_70 = var_1_70;
 last_1_var_1_78 = var_1_78;
 last_1_var_1_87 = var_1_87;
 last_1_var_1_91 = var_1_91;
 last_1_var_1_94 = var_1_94;
 last_1_var_1_95 = var_1_95;
 last_1_var_1_104 = var_1_104;
 last_1_var_1_106 = var_1_106;
 last_1_var_1_108 = var_1_108;
 last_1_var_1_110 = var_1_110;
}
int property() {
 return (((((((((((((((((((((((((((((((((((((((((((((((((((((((((var_1_63 + var_1_57) | var_1_44) < (var_1_6 & 10000)) ? (var_1_1 == ((double) var_1_7)) : (var_1_1 == ((double) ((((var_1_7) > (var_1_8)) ? (var_1_7) : (var_1_8)))))) && ((last_1_var_1_91 > last_1_var_1_9) ? ((last_1_var_1_18 < var_1_7) ? (var_1_9 == ((unsigned short int) last_1_var_1_104)) : 1) : ((var_1_7 == ((- last_1_var_1_18) / var_1_11)) ? (((last_1_var_1_104 / var_1_6) == last_1_var_1_9) ? ((((((- var_1_6) < 0 ) ? -(- var_1_6) : (- var_1_6))) <= -200) ? (var_1_9 == ((unsigned short int) ((((((last_1_var_1_30 + last_1_var_1_30) + last_1_var_1_54)) < (last_1_var_1_104)) ? (((last_1_var_1_30 + last_1_var_1_30) + last_1_var_1_54)) : (last_1_var_1_104))))) : (var_1_9 == ((unsigned short int) (48910 - (((((((last_1_var_1_30) < (last_1_var_1_54)) ? (last_1_var_1_30) : (last_1_var_1_54))) < 0 ) ? -((((last_1_var_1_30) < (last_1_var_1_54)) ? (last_1_var_1_30) : (last_1_var_1_54))) : ((((last_1_var_1_30) < (last_1_var_1_54)) ? (last_1_var_1_30) : (last_1_var_1_54))))))))) : (var_1_9 == ((unsigned short int) (((((last_1_var_1_30) < ((last_1_var_1_30 + last_1_var_1_91))) ? (last_1_var_1_30) : ((last_1_var_1_30 + last_1_var_1_91)))) + ((((last_1_var_1_54) > (last_1_var_1_104)) ? (last_1_var_1_54) : (last_1_var_1_104))))))) : 1))) && ((var_1_76 < (var_1_7 * var_1_11)) ? (var_1_18 == ((double) (var_1_19 + var_1_20))) : (var_1_18 == ((double) ((((var_1_21) > (var_1_8)) ? (var_1_21) : (var_1_8))))))) && ((var_1_11 <= ((((var_1_115) < (var_1_7)) ? (var_1_115) : (var_1_7)))) ? (var_1_45 ? (var_1_22 == ((unsigned char) ((((var_1_23) < ((var_1_24 - 10))) ? (var_1_23) : ((var_1_24 - 10)))))) : (var_1_22 == ((unsigned char) ((((((((var_1_23) > ((var_1_24 - var_1_25))) ? (var_1_23) : ((var_1_24 - var_1_25))))) > (var_1_26)) ? (((((var_1_23) > ((var_1_24 - var_1_25))) ? (var_1_23) : ((var_1_24 - var_1_25))))) : (var_1_26)))))) : ((var_1_8 > var_1_37) ? (var_1_22 == ((unsigned char) (((((var_1_24 - var_1_25)) > (var_1_23)) ? ((var_1_24 - var_1_25)) : (var_1_23))))) : 1))) && ((var_1_24 < (var_1_25 / ((((var_1_6) > (var_1_28)) ? (var_1_6) : (var_1_28))))) ? (((var_1_25 - var_1_26) <= var_1_54) ? (var_1_27 == ((unsigned short int) (var_1_29 - ((((var_1_104) < 0 ) ? -(var_1_104) : (var_1_104)))))) : 1) : (var_1_27 == ((unsigned short int) ((((var_1_91) > (var_1_26)) ? (var_1_91) : (var_1_26))))))) && (((last_1_var_1_44 | last_1_var_1_51) >= last_1_var_1_104) ? (var_1_30 == ((unsigned char) var_1_25)) : (var_1_30 == ((unsigned char) var_1_25)))) && ((last_1_var_1_91 < (var_1_23 / (var_1_29 - var_1_24))) ? ((last_1_var_1_104 < last_1_var_1_54) ? ((((50929 - last_1_var_1_30) * last_1_var_1_106) > 500) ? (var_1_32 == ((unsigned char) (! var_1_33))) : 1) : 1) : (var_1_32 == ((unsigned char) ((last_1_var_1_70 >= last_1_var_1_91) || var_1_33))))) && ((! var_1_45) ? (var_1_34 == ((unsigned long int) (var_1_112 + var_1_29))) : (var_1_34 == ((unsigned long int) (((((var_1_35) < (var_1_36)) ? (var_1_35) : (var_1_36))) - ((((50u) < (var_1_112)) ? (50u) : (var_1_112)))))))) && ((var_1_73 >= ((var_1_30 % var_1_24) + var_1_91)) ? ((var_1_88 || var_1_33) ? (var_1_37 == ((float) ((10.2f + ((((99999.75f) < 0 ) ? -(99999.75f) : (99999.75f)))) + (((((var_1_38 + var_1_39)) < (var_1_20)) ? ((var_1_38 + var_1_39)) : (var_1_20)))))) : (var_1_37 == ((float) var_1_7))) : 1)) && ((var_1_39 <= (var_1_38 / var_1_11)) ? (var_1_40 == ((float) (var_1_41 - ((3.0717073020876769E18f - var_1_42) + (4.372261890791681E18f - var_1_43))))) : 1)) && ((var_1_36 > var_1_104) ? (var_1_44 == ((unsigned long int) var_1_30)) : (var_1_44 == ((unsigned long int) (((((var_1_36) > (var_1_35)) ? (var_1_36) : (var_1_35))) - var_1_54))))) && ((last_1_var_1_94 > (var_1_42 * var_1_43)) ? (var_1_45 == ((unsigned char) var_1_47)) : (var_1_45 == ((unsigned char) (! (last_1_var_1_32 && (! var_1_33))))))) && (((var_1_25 - var_1_24) >= var_1_28) ? (var_1_48 == ((signed char) (((((var_1_49) < 0 ) ? -(var_1_49) : (var_1_49))) - var_1_50))) : ((! (var_1_9 == var_1_24)) ? (var_1_48 == ((signed char) ((((var_1_49) > (var_1_50)) ? (var_1_49) : (var_1_50))))) : (var_1_48 == ((signed char) var_1_50))))) && ((var_1_60 <= var_1_28) ? (var_1_88 ? (var_1_64 ? (var_1_51 == ((signed short int) (((((1000 - var_1_25)) > ((var_1_24 - var_1_22))) ? ((1000 - var_1_25)) : ((var_1_24 - var_1_22)))))) : 1) : (var_1_51 == ((signed short int) (var_1_23 + var_1_54)))) : (var_1_51 == ((signed short int) (((var_1_81 + var_1_28) + -5) + (var_1_104 - var_1_23)))))) && (((var_1_108 / var_1_29) != var_1_91) ? (((var_1_34 * 32) <= var_1_26) ? (var_1_88 ? (var_1_52 == ((signed short int) (((((var_1_34) < (var_1_106)) ? (var_1_34) : (var_1_106))) - var_1_22))) : (var_1_52 == ((signed short int) (var_1_25 - var_1_23)))) : 1) : 1)) && ((var_1_6 < var_1_9) ? ((var_1_24 > var_1_35) ? (var_1_53 == ((unsigned short int) (var_1_29 - var_1_28))) : 1) : (var_1_53 == ((unsigned short int) ((((var_1_29 - (25162 - var_1_23)) < 0 ) ? -(var_1_29 - (25162 - var_1_23)) : (var_1_29 - (25162 - var_1_23)))))))) && (((var_1_38 == var_1_43) && var_1_33) ? (var_1_54 == ((unsigned char) var_1_24)) : ((last_1_var_1_91 <= last_1_var_1_57) ? (((last_1_var_1_22 / ((((var_1_6) > (var_1_28)) ? (var_1_6) : (var_1_28)))) < last_1_var_1_108) ? (var_1_54 == ((unsigned char) (var_1_25 + var_1_50))) : ((((- var_1_36) + last_1_var_1_104) < last_1_var_1_22) ? (var_1_54 == ((unsigned char) ((((var_1_24) > (var_1_50)) ? (var_1_24) : (var_1_50))))) : (var_1_54 == ((unsigned char) (var_1_25 + var_1_50))))) : (var_1_54 == ((unsigned char) (var_1_24 - var_1_50)))))) && (var_1_56 == ((unsigned short int) (var_1_104 + var_1_108)))) && ((var_1_104 >= (last_1_var_1_57 + var_1_87)) ? (var_1_57 == ((unsigned short int) var_1_50)) : (var_1_57 == ((unsigned short int) (((((var_1_50 + var_1_104)) > (var_1_91)) ? ((var_1_50 + var_1_104)) : (var_1_91))))))) && ((! var_1_32) ? ((var_1_19 <= var_1_86) ? (var_1_58 == ((float) (var_1_39 + var_1_42))) : 1) : (var_1_58 == ((float) ((((((var_1_59 - 255.5f) - var_1_43)) < ((((((25.5f - var_1_42)) < (var_1_41)) ? ((25.5f - var_1_42)) : (var_1_41))))) ? (((var_1_59 - 255.5f) - var_1_43)) : ((((((25.5f - var_1_42)) < (var_1_41)) ? ((25.5f - var_1_42)) : (var_1_41)))))))))) && ((var_1_48 > var_1_54) ? ((var_1_6 != (((((var_1_87) < (var_1_30)) ? (var_1_87) : (var_1_30))) / var_1_28)) ? (var_1_60 == ((unsigned short int) (((((var_1_29) > (var_1_61)) ? (var_1_29) : (var_1_61))) - var_1_28))) : (((~ var_1_99) < var_1_54) ? (var_1_60 == ((unsigned short int) ((var_1_62 - ((((var_1_23) < 0 ) ? -(var_1_23) : (var_1_23)))) - var_1_91))) : ((var_1_64 || var_1_101) ? (var_1_60 == ((unsigned short int) (var_1_62 - 16))) : (var_1_60 == ((unsigned short int) ((((var_1_54 + 32) < 0 ) ? -(var_1_54 + 32) : (var_1_54 + 32)))))))) : 1)) && ((last_1_var_1_87 >= ((((10) < 0 ) ? -(10) : (10)))) ? (var_1_63 == ((signed long int) ((((last_1_var_1_110) > (last_1_var_1_27)) ? (last_1_var_1_110) : (last_1_var_1_27))))) : 1)) && ((((- var_1_81) >> var_1_63) != var_1_30) ? (var_1_64 == ((unsigned char) (var_1_107 && var_1_47))) : (var_1_64 == ((unsigned char) (var_1_101 && (var_1_47 || var_1_65)))))) && ((var_1_101 || var_1_47) ? (var_1_66 == ((float) (((var_1_67 + var_1_68) - var_1_43) - (var_1_42 + var_1_69)))) : 1)) && ((16 < var_1_6) ? (var_1_70 == ((unsigned short int) var_1_50)) : (((var_1_63 * var_1_104) <= var_1_80) ? (var_1_70 == ((unsigned short int) ((((((((var_1_54) > (((((var_1_23) < (var_1_61)) ? (var_1_23) : (var_1_61))))) ? (var_1_54) : (((((var_1_23) < (var_1_61)) ? (var_1_23) : (var_1_61))))))) < ((((((62088) > (var_1_29)) ? (62088) : (var_1_29))) - var_1_104))) ? (((((var_1_54) > (((((var_1_23) < (var_1_61)) ? (var_1_23) : (var_1_61))))) ? (var_1_54) : (((((var_1_23) < (var_1_61)) ? (var_1_23) : (var_1_61))))))) : ((((((62088) > (var_1_29)) ? (62088) : (var_1_29))) - var_1_104)))))) : (var_1_65 ? ((var_1_38 > (- (- var_1_19))) ? (var_1_70 == ((unsigned short int) (var_1_104 + (var_1_71 - (var_1_25 + 10))))) : 1) : ((var_1_33 || (var_1_52 > var_1_44)) ? (var_1_70 == ((unsigned short int) ((((var_1_81) > (50)) ? (var_1_81) : (50))))) : (var_1_101 ? (var_1_70 == ((unsigned short int) ((((var_1_106) < 0 ) ? -(var_1_106) : (var_1_106))))) : 1)))))) && ((var_1_8 != var_1_102) ? (var_1_72 == ((signed short int) (((((var_1_30 - var_1_26)) > (var_1_48)) ? ((var_1_30 - var_1_26)) : (var_1_48))))) : (((var_1_23 != (- var_1_48)) || (var_1_88 || var_1_33)) ? (var_1_72 == ((signed short int) var_1_60)) : 1))) && (var_1_47 ? (var_1_73 == ((unsigned long int) ((((var_1_80) < 0 ) ? -(var_1_80) : (var_1_80))))) : (var_1_73 == ((unsigned long int) ((((((var_1_74 + var_1_75)) < (var_1_35)) ? ((var_1_74 + var_1_75)) : (var_1_35))) - var_1_50))))) && ((var_1_111 <= var_1_68) ? (((var_1_30 ^ var_1_80) != var_1_108) ? (var_1_76 == ((double) var_1_68)) : 1) : 1)) && (((10u * var_1_85) == var_1_110) ? (var_1_77 == ((float) (((((var_1_19) < (var_1_67)) ? (var_1_19) : (var_1_67))) + (((((var_1_43) > (var_1_38)) ? (var_1_43) : (var_1_38))) + ((((var_1_42) < (var_1_39)) ? (var_1_42) : (var_1_39))))))) : (((var_1_40 == var_1_86) && var_1_107) ? ((-256 > (~ var_1_56)) ? (var_1_77 == ((float) (var_1_19 + (var_1_43 + ((((var_1_42) < 0 ) ? -(var_1_42) : (var_1_42))))))) : (var_1_77 == ((float) var_1_21))) : (var_1_77 == ((float) ((((var_1_7) < 0 ) ? -(var_1_7) : (var_1_7)))))))) && (((var_1_21 * var_1_20) <= last_1_var_1_78) ? ((((var_1_62 * var_1_48) << var_1_70) != var_1_70) ? (var_1_78 == ((double) (16.25 - ((((((((var_1_59) < (var_1_43)) ? (var_1_59) : (var_1_43)))) > (var_1_42)) ? (((((var_1_59) < (var_1_43)) ? (var_1_59) : (var_1_43)))) : (var_1_42)))))) : (var_1_78 == ((double) ((((var_1_68) > (((((var_1_67) > (((((var_1_69) < 0 ) ? -(var_1_69) : (var_1_69))))) ? (var_1_67) : (((((var_1_69) < 0 ) ? -(var_1_69) : (var_1_69)))))))) ? (var_1_68) : (((((var_1_67) > (((((var_1_69) < 0 ) ? -(var_1_69) : (var_1_69))))) ? (var_1_67) : (((((var_1_69) < 0 ) ? -(var_1_69) : (var_1_69)))))))))))) : (((var_1_19 * var_1_1) == var_1_11) ? (var_1_78 == ((double) (((((127.75) < 0 ) ? -(127.75) : (127.75))) + var_1_20))) : 1))) && (var_1_33 ? (var_1_80 == ((signed long int) ((((var_1_63) > ((var_1_72 - var_1_24))) ? (var_1_63) : ((var_1_72 - var_1_24)))))) : (var_1_80 == ((signed long int) (var_1_63 + var_1_71))))) && (((var_1_25 / var_1_29) < (1 - var_1_91)) ? ((((((4) < 0 ) ? -(4) : (4))) <= var_1_27) ? (var_1_81 == ((signed char) ((var_1_82 - 4) + var_1_83))) : (var_1_81 == ((signed char) (var_1_83 + var_1_82)))) : (var_1_81 == ((signed char) (((((var_1_83) < (var_1_82)) ? (var_1_83) : (var_1_82))) + var_1_84))))) && ((((var_1_8 >= var_1_76) || var_1_32) || var_1_88) ? (var_1_85 == ((signed short int) (var_1_28 + var_1_51))) : (var_1_85 == ((signed short int) var_1_82)))) && ((var_1_1 >= (var_1_102 + (var_1_67 + var_1_66))) ? ((var_1_54 <= var_1_104) ? (var_1_86 == ((double) ((var_1_43 + var_1_42) + var_1_68))) : (var_1_86 == ((double) ((var_1_43 + var_1_39) + var_1_68)))) : 1)) && ((var_1_104 > var_1_24) ? (var_1_87 == ((signed short int) ((var_1_83 + var_1_23) + var_1_108))) : (var_1_87 == ((signed short int) (((((((var_1_9) < (var_1_100)) ? (var_1_9) : (var_1_100))) < 0 ) ? -((((var_1_9) < (var_1_100)) ? (var_1_9) : (var_1_100))) : ((((var_1_9) < (var_1_100)) ? (var_1_9) : (var_1_100))))))))) && (((var_1_59 > var_1_19) || var_1_45) ? (var_1_88 == ((unsigned char) (var_1_47 && var_1_65))) : ((var_1_54 <= var_1_56) ? (var_1_88 == ((unsigned char) ((2.4 < var_1_59) || var_1_33))) : 1))) && (((last_1_var_1_30 << last_1_var_1_22) <= -1) ? (((last_1_var_1_95 / 5.2) < var_1_11) ? (var_1_91 == ((unsigned char) (var_1_50 + ((((var_1_82 + var_1_93) < 0 ) ? -(var_1_82 + var_1_93) : (var_1_82 + var_1_93)))))) : (var_1_91 == ((unsigned char) ((((var_1_23) < (var_1_25)) ? (var_1_23) : (var_1_25)))))) : (var_1_91 == ((unsigned char) ((((((((var_1_26) < 0 ) ? -(var_1_26) : (var_1_26)))) < (var_1_50)) ? (((((var_1_26) < 0 ) ? -(var_1_26) : (var_1_26)))) : (var_1_50))))))) && (var_1_32 ? ((var_1_72 >= (var_1_74 & var_1_30)) ? (var_1_94 == ((double) (var_1_69 + var_1_39))) : 1) : (var_1_94 == ((double) ((((var_1_67) < (var_1_19)) ? (var_1_67) : (var_1_19))))))) && ((! var_1_32) ? (var_1_95 == ((double) ((4.75 - var_1_68) + ((((99999.875) < 0 ) ? -(99999.875) : (99999.875)))))) : (((var_1_25 >> (var_1_96 - var_1_97)) <= var_1_73) ? (var_1_95 == ((double) (((((var_1_42) < (var_1_98)) ? (var_1_42) : (var_1_98))) + var_1_39))) : (var_1_95 == ((double) ((var_1_68 + 3.75) - var_1_59)))))) && (var_1_105 ? (var_1_99 == ((unsigned long int) var_1_23)) : (var_1_99 == ((unsigned long int) var_1_29)))) && (var_1_100 == ((signed char) var_1_49))) && (var_1_65 ? (var_1_101 == ((unsigned char) var_1_33)) : (var_1_101 == ((unsigned char) var_1_33)))) && (var_1_32 ? (var_1_102 == ((double) var_1_43)) : (var_1_102 == ((double) var_1_8)))) && (var_1_103 == ((float) var_1_43))) && (var_1_104 == ((unsigned char) 10))) && (var_1_45 ? (var_1_105 == ((unsigned char) var_1_65)) : (var_1_105 == ((unsigned char) var_1_33)))) && (var_1_65 ? (var_1_106 == ((unsigned char) var_1_96)) : 1)) && (var_1_107 == ((unsigned char) var_1_33))) && (var_1_108 == ((signed long int) var_1_44))) && (var_1_47 ? (var_1_109 == ((signed char) var_1_84)) : (var_1_109 == ((signed char) var_1_50)))) && (var_1_32 ? (var_1_110 == ((signed long int) var_1_99)) : (var_1_110 == ((signed long int) var_1_60)))) && (var_1_105 ? (var_1_111 == ((float) 3.75f)) : (var_1_111 == ((float) var_1_42)))) && ((var_1_24 <= (var_1_110 / var_1_28)) ? (var_1_112 == ((unsigned short int) var_1_104)) : (var_1_112 == ((unsigned short int) (var_1_61 - var_1_44))))) && (var_1_114 == ((signed char) var_1_50))) && (var_1_115 == ((float) var_1_41))
;
}
int main(void) {
 isInitial = 1;
 initially();
 while (1) {
  updateLastVariables();
  updateVariables();
  step();
  __VERIFIER_assert(property());
  isInitial = 0;
 }
 return 0;
}