// 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_Batch53Amount500.c", 13, "reach_error"); }
void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } return; }
void assume_abort_if_not(int cond) { if(!cond) { abort(); } }
unsigned char isInitial = 0;
signed long int var_1_1 = -100;
unsigned char var_1_2 = 200;
unsigned char var_1_3 = 100;
unsigned char var_1_4 = 8;
signed long int var_1_8 = 1416054444;
signed long int var_1_9 = 1942252734;
unsigned long int var_1_10 = 128;
unsigned long int var_1_13 = 3014528178;
unsigned short int var_1_14 = 10000;
unsigned short int var_1_15 = 20328;
unsigned short int var_1_16 = 26363;
unsigned long int var_1_17 = 5;
unsigned long int var_1_18 = 2212503301;
unsigned long int var_1_19 = 0;
signed short int var_1_20 = -25;
float var_1_22 = 255.125;
unsigned char var_1_23 = 0;
unsigned long int var_1_24 = 5;
unsigned long int var_1_25 = 8;
unsigned char var_1_26 = 1;
unsigned char var_1_27 = 0;
unsigned char var_1_28 = 0;
unsigned char var_1_29 = 1;
unsigned char var_1_30 = 128;
signed char var_1_31 = 2;
double var_1_32 = 63.125;
unsigned char var_1_33 = 200;
double var_1_34 = 8.5;
double var_1_35 = 15.2;
signed long int var_1_36 = -256;
signed long int var_1_37 = 1420560553;
float var_1_39 = 5.5;
float var_1_40 = 31.4;
float var_1_41 = 0.0;
signed char var_1_42 = 10;
unsigned char var_1_43 = 5;
signed char var_1_44 = 5;
signed char var_1_45 = 4;
signed short int var_1_46 = 16;
unsigned char var_1_47 = 0;
unsigned char var_1_48 = 10;
unsigned char var_1_49 = 200;
unsigned long int var_1_50 = 500;
unsigned short int var_1_51 = 8;
float var_1_52 = 0.875;
float var_1_53 = 255.5;
unsigned long int var_1_54 = 256;
unsigned long int var_1_55 = 1000000000;
unsigned short int var_1_56 = 40802;
unsigned long int var_1_57 = 1429165116;
float var_1_58 = 128.75;
float var_1_59 = 1000000000000000.1;
float var_1_60 = 10.5;
float var_1_61 = 3.5;
float var_1_62 = 100000000000000.75;
signed char var_1_63 = -16;
unsigned short int var_1_64 = 256;
unsigned short int var_1_65 = 59465;
unsigned short int var_1_66 = 50385;
unsigned short int var_1_67 = 64756;
unsigned short int var_1_68 = 10000;
unsigned long int var_1_69 = 32;
signed short int var_1_71 = -8;
double var_1_73 = 8.4;
signed char var_1_74 = 16;
signed char var_1_75 = -5;
float var_1_76 = 7.5;
signed short int var_1_77 = -4;
signed short int var_1_79 = -1;
unsigned char var_1_80 = 1;
unsigned char var_1_81 = 1;
double var_1_82 = 1.78;
unsigned char var_1_83 = 0;
signed char var_1_84 = 16;
unsigned long int var_1_85 = 100000;
float var_1_86 = 5.5;
float var_1_87 = 16.5;
signed long int var_1_88 = -10;
signed char var_1_89 = 0;
unsigned char var_1_90 = 1;
float var_1_91 = 100.375;
signed long int var_1_92 = 8;
unsigned short int var_1_93 = 2;
unsigned long int var_1_94 = 128;
double var_1_95 = 1.9;
unsigned long int var_1_96 = 4;
unsigned long int var_1_97 = 10;
signed char var_1_99 = 0;
unsigned char var_1_100 = 2;
unsigned char var_1_101 = 32;
unsigned short int var_1_102 = 128;
signed long int last_1_var_1_1 = -100;
unsigned long int last_1_var_1_17 = 5;
unsigned char last_1_var_1_23 = 0;
unsigned char last_1_var_1_29 = 1;
signed char last_1_var_1_44 = 5;
signed short int last_1_var_1_46 = 16;
unsigned char last_1_var_1_47 = 0;
unsigned char last_1_var_1_48 = 10;
unsigned long int last_1_var_1_50 = 500;
unsigned long int last_1_var_1_69 = 32;
signed short int last_1_var_1_71 = -8;
double last_1_var_1_73 = 8.4;
float last_1_var_1_76 = 7.5;
signed short int last_1_var_1_77 = -4;
signed long int last_1_var_1_88 = -10;
unsigned char last_1_var_1_90 = 1;
signed long int last_1_var_1_92 = 8;
unsigned char last_1_var_1_100 = 2;
void initially(void) {
}
void step(void) {
 if (last_1_var_1_90) {
  var_1_54 = ((last_1_var_1_77 + (var_1_55 - var_1_16)) + ((((var_1_2) > (var_1_24)) ? (var_1_2) : (var_1_24))));
 } else {
  if ((var_1_56 - last_1_var_1_100) > var_1_8) {
   if (last_1_var_1_90) {
    if (var_1_26) {
     if (last_1_var_1_76 < last_1_var_1_73) {
      var_1_54 = last_1_var_1_100;
     } else {
      var_1_54 = ((((((var_1_57 - last_1_var_1_69)) > ((var_1_45 + 10u))) ? ((var_1_57 - last_1_var_1_69)) : ((var_1_45 + 10u)))) + var_1_8);
     }
    } else {
     var_1_54 = ((((var_1_15) > (last_1_var_1_77)) ? (var_1_15) : (last_1_var_1_77)));
    }
   } else {
    var_1_54 = (var_1_13 - var_1_55);
   }
  } else {
   var_1_54 = (var_1_8 + var_1_57);
  }
 }
 if (! (last_1_var_1_48 < last_1_var_1_1)) {
  var_1_80 = var_1_26;
 } else {
  var_1_80 = (var_1_26 && ((var_1_28 || var_1_81) && (! var_1_27)));
 }
 if (var_1_80) {
  var_1_101 = var_1_45;
 } else {
  var_1_101 = var_1_4;
 }
 if (last_1_var_1_47) {
  var_1_46 = ((((last_1_var_1_46) > (last_1_var_1_88)) ? (last_1_var_1_46) : (last_1_var_1_88)));
 } else {
  var_1_46 = (var_1_2 + last_1_var_1_46);
 }
 signed short int stepLocal_7 = var_1_46;
 if (stepLocal_7 <= var_1_3) {
  var_1_48 = ((var_1_49 - var_1_45) - ((((((((var_1_3) > (var_1_4)) ? (var_1_3) : (var_1_4)))) < (var_1_24)) ? (((((var_1_3) > (var_1_4)) ? (var_1_3) : (var_1_4)))) : (var_1_24))));
 }
 signed long int stepLocal_18 = last_1_var_1_88;
 if (stepLocal_18 >= (last_1_var_1_17 * last_1_var_1_69)) {
  var_1_102 = (var_1_66 - ((var_1_25 + var_1_30) + last_1_var_1_29));
 } else {
  var_1_102 = (last_1_var_1_29 + var_1_68);
 }
 if ((16u <= var_1_102) && var_1_28) {
  var_1_64 = (((((((((var_1_65) > (var_1_66)) ? (var_1_65) : (var_1_66)))) < (40384)) ? (((((var_1_65) > (var_1_66)) ? (var_1_65) : (var_1_66)))) : (40384))) - ((((var_1_16) > (var_1_3)) ? (var_1_16) : (var_1_3))));
 } else {
  var_1_64 = ((var_1_67 - (var_1_68 - var_1_45)) - var_1_30);
 }
 unsigned long int stepLocal_5 = var_1_37 / ((((var_1_13) > (var_1_33)) ? (var_1_13) : (var_1_33)));
 if (var_1_102 <= stepLocal_5) {
  var_1_43 = var_1_30;
 }
 if ((last_1_var_1_1 / var_1_30) > (((((last_1_var_1_88) > (var_1_9)) ? (last_1_var_1_88) : (var_1_9))) - (var_1_37 - 2))) {
  if (((((last_1_var_1_50) > (last_1_var_1_1)) ? (last_1_var_1_50) : (last_1_var_1_1))) > var_1_15) {
   var_1_36 = ((((200) < 0 ) ? -(200) : (200)));
  }
 } else {
  if (last_1_var_1_90) {
   if (256u >= var_1_18) {
    if (last_1_var_1_23) {
     var_1_36 = (50 - (1976409169 - var_1_25));
    }
   } else {
    if (var_1_28) {
     if (var_1_26) {
      var_1_36 = (-10 + last_1_var_1_71);
     } else {
      var_1_36 = var_1_16;
     }
    } else {
     var_1_36 = last_1_var_1_50;
    }
   }
  } else {
   var_1_36 = var_1_3;
  }
 }
 if (var_1_27) {
  if (var_1_43 == (var_1_45 / var_1_49)) {
   if (var_1_62 < (var_1_41 - var_1_53)) {
    if (var_1_62 <= (((((var_1_53) < 0 ) ? -(var_1_53) : (var_1_53))) - var_1_40)) {
     var_1_63 = (var_1_4 + var_1_24);
    }
   } else {
    var_1_63 = (var_1_4 + var_1_45);
   }
  }
 } else {
  var_1_63 = (var_1_24 + -2);
 }
 unsigned char stepLocal_6 = var_1_2;
 if (stepLocal_6 >= (last_1_var_1_92 + var_1_25)) {
  if (! (var_1_15 >= last_1_var_1_44)) {
   var_1_47 = ((! (var_1_27 || var_1_26)) || var_1_28);
  }
 }
 signed long int stepLocal_0 = var_1_9;
 if (stepLocal_0 > (var_1_3 ^ ((((var_1_2) > (4)) ? (var_1_2) : (4))))) {
  var_1_14 = ((((var_1_4) < (var_1_2)) ? (var_1_4) : (var_1_2)));
 } else {
  var_1_14 = (var_1_2 + (((((var_1_15) > (var_1_16)) ? (var_1_15) : (var_1_16))) - var_1_4));
 }
 var_1_29 = (var_1_30 - 32);
 var_1_31 = (4 - ((((var_1_25) < 0 ) ? -(var_1_25) : (var_1_25))));
 if (((var_1_33 - var_1_4) - var_1_25) == var_1_16) {
  var_1_32 = (8.5 - ((8.05 + var_1_34) + var_1_35));
 }
 signed long int stepLocal_3 = 16;
 if (stepLocal_3 <= (var_1_33 + var_1_63)) {
  if (! (var_1_24 >= ((((var_1_16) < (256u)) ? (var_1_16) : (256u))))) {
   if (15.6 >= (var_1_35 - 3.95)) {
    var_1_39 = (var_1_35 + ((((9.5f) > ((var_1_34 - var_1_40))) ? (9.5f) : ((var_1_34 - var_1_40)))));
   } else {
    var_1_39 = (((((var_1_40) < 0 ) ? -(var_1_40) : (var_1_40))) - (var_1_41 - var_1_34));
   }
  } else {
   var_1_39 = ((((var_1_41) < (var_1_35)) ? (var_1_41) : (var_1_35)));
  }
 } else {
  var_1_39 = ((((var_1_34) < (200.6f)) ? (var_1_34) : (200.6f)));
 }
 unsigned long int stepLocal_8 = var_1_24;
 if (200u >= stepLocal_8) {
  var_1_50 = (var_1_4 + ((((1u) < ((var_1_33 + var_1_24))) ? (1u) : ((var_1_33 + var_1_24)))));
 } else {
  var_1_50 = ((((var_1_45) < ((var_1_3 + var_1_2))) ? (var_1_45) : ((var_1_3 + var_1_2))));
 }
 if (var_1_40 <= (var_1_35 - var_1_34)) {
  var_1_51 = (47137 - var_1_16);
 }
 if (1 < (-64 * var_1_8)) {
  var_1_52 = (var_1_35 - ((var_1_34 + var_1_53) + var_1_40));
 } else {
  var_1_52 = (0.75f - var_1_41);
 }
 var_1_58 = ((((((var_1_53) < (var_1_34)) ? (var_1_53) : (var_1_34))) + var_1_59) + (var_1_60 + ((((var_1_61) > (var_1_62)) ? (var_1_61) : (var_1_62)))));
 if (var_1_34 < (var_1_62 / ((((var_1_41) < (var_1_22)) ? (var_1_41) : (var_1_22))))) {
  var_1_74 = ((((var_1_25) < ((((((var_1_24) < (var_1_45)) ? (var_1_24) : (var_1_45))) + var_1_4))) ? (var_1_25) : ((((((var_1_24) < (var_1_45)) ? (var_1_24) : (var_1_45))) + var_1_4))));
 } else {
  if (var_1_49 >= ((var_1_33 - var_1_45) - var_1_4)) {
   var_1_74 = (((((var_1_25) < (var_1_4)) ? (var_1_25) : (var_1_4))) + -50);
  } else {
   var_1_74 = ((((var_1_4) < 0 ) ? -(var_1_4) : (var_1_4)));
  }
 }
 var_1_85 = (((((var_1_13) < (var_1_18)) ? (var_1_13) : (var_1_18))) - var_1_68);
 if (var_1_81) {
  var_1_87 = ((((var_1_53) < 0 ) ? -(var_1_53) : (var_1_53)));
 }
 var_1_89 = var_1_24;
 var_1_90 = var_1_26;
 var_1_91 = var_1_62;
 var_1_93 = var_1_63;
 if (var_1_26) {
  var_1_94 = var_1_68;
 } else {
  var_1_94 = 8u;
 }
 if (var_1_27) {
  var_1_95 = var_1_61;
 } else {
  var_1_95 = var_1_60;
 }
 if (var_1_26) {
  var_1_99 = var_1_49;
 } else {
  var_1_99 = var_1_75;
 }
 var_1_100 = var_1_4;
 signed long int stepLocal_2 = (var_1_9 % var_1_16) * var_1_101;
 unsigned char stepLocal_1 = var_1_100;
 if ((var_1_29 >> (var_1_24 + var_1_25)) <= stepLocal_1) {
  if (var_1_50 == stepLocal_2) {
   var_1_23 = (! (! var_1_26));
  } else {
   var_1_23 = (! (var_1_27 || var_1_28));
  }
 }
 if (var_1_52 != var_1_61) {
  var_1_86 = var_1_40;
 } else {
  if ((- var_1_87) < var_1_53) {
   if (var_1_80) {
    var_1_86 = (((((var_1_35) > (var_1_60)) ? (var_1_35) : (var_1_60))) + (((((var_1_34) < (999.4f)) ? (var_1_34) : (999.4f))) + var_1_61));
   } else {
    var_1_86 = var_1_60;
   }
  }
 }
 if (var_1_27) {
  var_1_97 = var_1_51;
 } else {
  var_1_97 = var_1_64;
 }
 if (var_1_13 <= (- var_1_3)) {
  if (var_1_23 || var_1_80) {
   var_1_44 = ((((16) > ((var_1_25 + var_1_4))) ? (16) : ((var_1_25 + var_1_4))));
  } else {
   var_1_44 = ((((5) > (var_1_33)) ? (5) : (var_1_33)));
  }
 } else {
  var_1_44 = (var_1_45 + var_1_4);
 }
 if (var_1_47) {
  var_1_92 = var_1_50;
 } else {
  var_1_92 = var_1_4;
 }
 if ((31.75 + 15.5) < ((((var_1_58) > (var_1_87)) ? (var_1_58) : (var_1_87)))) {
  var_1_10 = ((((var_1_13 - var_1_4) < 0 ) ? -(var_1_13 - var_1_4) : (var_1_13 - var_1_4)));
 } else {
  var_1_10 = (256u + var_1_8);
 }
 if (var_1_23) {
  var_1_19 = (((((var_1_3 + ((((var_1_9) < (var_1_15)) ? (var_1_9) : (var_1_15))))) > (var_1_13)) ? ((var_1_3 + ((((var_1_9) < (var_1_15)) ? (var_1_9) : (var_1_15))))) : (var_1_13)));
 } else {
  var_1_19 = ((((var_1_16) > ((var_1_29 + var_1_3))) ? (var_1_16) : ((var_1_29 + var_1_3))));
 }
 if ((3.5 - var_1_34) > var_1_40) {
  if (var_1_90 || var_1_26) {
   var_1_76 = (((((var_1_41 - var_1_35)) > ((var_1_53 + var_1_62))) ? ((var_1_41 - var_1_35)) : ((var_1_53 + var_1_62))));
  }
 } else {
  if (var_1_26) {
   var_1_76 = (((((var_1_53 - (var_1_41 - 256.6f))) < (((((var_1_60) > (var_1_35)) ? (var_1_60) : (var_1_35))))) ? ((var_1_53 - (var_1_41 - 256.6f))) : (((((var_1_60) > (var_1_35)) ? (var_1_60) : (var_1_35))))));
  }
 }
 unsigned long int stepLocal_12 = (var_1_66 - var_1_45) + var_1_57;
 if (stepLocal_12 <= ((((128u) < (0u)) ? (128u) : (0u)))) {
  var_1_79 = var_1_99;
 } else {
  var_1_79 = var_1_33;
 }
 unsigned char stepLocal_13 = var_1_81;
 if (var_1_90) {
  if ((var_1_2 != var_1_68) && stepLocal_13) {
   var_1_82 = (((((var_1_59 + var_1_53)) < (((5.8 + var_1_40) - var_1_41))) ? ((var_1_59 + var_1_53)) : (((5.8 + var_1_40) - var_1_41))));
  }
 } else {
  if (var_1_28) {
   var_1_82 = ((((0.8) > (((var_1_34 + var_1_35) - var_1_53))) ? (0.8) : (((var_1_34 + var_1_35) - var_1_53))));
  }
 }
 unsigned long int stepLocal_17 = var_1_13 - var_1_57;
 if ((25 + var_1_36) < stepLocal_17) {
  var_1_84 = (8 + var_1_45);
 } else {
  if (var_1_81) {
   if (var_1_86 > (var_1_53 * 100.2f)) {
    var_1_84 = (((((var_1_45) < (var_1_4)) ? (var_1_45) : (var_1_4))) + var_1_75);
   } else {
    var_1_84 = ((var_1_25 + 8) + var_1_45);
   }
  } else {
   var_1_84 = ((((var_1_45) < (var_1_24)) ? (var_1_45) : (var_1_24)));
  }
 }
 if (var_1_60 != var_1_86) {
  if (var_1_28) {
   var_1_73 = var_1_61;
  } else {
   var_1_73 = var_1_60;
  }
 } else {
  var_1_73 = var_1_61;
 }
 if (var_1_23) {
  if (var_1_43 > var_1_4) {
   var_1_17 = (((((var_1_13) > (3076280705u)) ? (var_1_13) : (3076280705u))) - var_1_4);
  }
 } else {
  var_1_17 = (((((((((var_1_13) > (var_1_18)) ? (var_1_13) : (var_1_18))) - var_1_16)) > (var_1_2)) ? ((((((var_1_13) > (var_1_18)) ? (var_1_13) : (var_1_18))) - var_1_16)) : (var_1_2)));
 }
 if (var_1_32 > (var_1_73 + var_1_59)) {
  var_1_88 = (((((var_1_94 + 100)) > (var_1_36)) ? ((var_1_94 + 100)) : (var_1_36)));
 } else {
  var_1_88 = var_1_25;
 }
 if (var_1_48 != (var_1_4 / (var_1_9 + 5u))) {
  if (((var_1_100 + var_1_51) + var_1_48) >= var_1_67) {
   var_1_77 = ((var_1_45 + 5) + ((((((((var_1_3) < 0 ) ? -(var_1_3) : (var_1_3)))) > (var_1_14)) ? (((((var_1_3) < 0 ) ? -(var_1_3) : (var_1_3)))) : (var_1_14))));
  } else {
   var_1_77 = ((var_1_14 + var_1_33) + (var_1_10 + var_1_45));
  }
 } else {
  var_1_77 = var_1_24;
 }
 unsigned long int stepLocal_4 = (var_1_10 * var_1_30) / -128;
 if (var_1_26) {
  if (((((var_1_102) < (var_1_8)) ? (var_1_102) : (var_1_8))) < stepLocal_4) {
   var_1_42 = var_1_4;
  }
 } else {
  if (! ((var_1_36 * var_1_64) < var_1_3)) {
   var_1_42 = var_1_33;
  }
 }
 if (var_1_47) {
  if (var_1_76 >= (- (var_1_32 / var_1_22))) {
   var_1_20 = ((((var_1_2) < (((((var_1_3) > (var_1_4)) ? (var_1_3) : (var_1_4))))) ? (var_1_2) : (((((var_1_3) > (var_1_4)) ? (var_1_3) : (var_1_4))))));
  }
 }
 if (var_1_14 < var_1_42) {
  var_1_69 = ((((var_1_3) < ((((((var_1_54) > (var_1_33)) ? (var_1_54) : (var_1_33))) + var_1_101))) ? (var_1_3) : ((((((var_1_54) > (var_1_33)) ? (var_1_54) : (var_1_33))) + var_1_101))));
 }
 signed short int stepLocal_16 = var_1_20;
 unsigned long int stepLocal_15 = - 25u;
 unsigned long int stepLocal_14 = var_1_17;
 if (var_1_97 < stepLocal_15) {
  if (var_1_81) {
   if (stepLocal_14 > (var_1_45 - ((((var_1_3) < (var_1_24)) ? (var_1_3) : (var_1_24))))) {
    var_1_83 = ((var_1_10 == var_1_10) || var_1_26);
   }
  }
 } else {
  if (var_1_47) {
   if (stepLocal_16 > var_1_51) {
    var_1_83 = 1;
   } else {
    var_1_83 = ((! var_1_28) && (var_1_27 || var_1_26));
   }
  }
 }
 signed long int stepLocal_11 = var_1_100 + var_1_15;
 unsigned short int stepLocal_10 = var_1_68;
 signed short int stepLocal_9 = var_1_46;
 if (((((var_1_66) < ((- var_1_63))) ? (var_1_66) : ((- var_1_63)))) > stepLocal_11) {
  if (((((var_1_49) < (var_1_3)) ? (var_1_49) : (var_1_3))) > stepLocal_10) {
   if (((((var_1_22) < ((- 128.975))) ? (var_1_22) : ((- 128.975)))) >= var_1_95) {
    var_1_71 = ((var_1_97 + var_1_33) + var_1_20);
   }
  }
 } else {
  if (stepLocal_9 >= var_1_46) {
   var_1_71 = ((((var_1_67) > ((var_1_33 - var_1_36))) ? (var_1_67) : ((var_1_33 - var_1_36))));
  } else {
   var_1_71 = (((((var_1_49) < (var_1_33)) ? (var_1_49) : (var_1_33))) - var_1_20);
  }
 }
 if (var_1_83) {
  var_1_96 = 8u;
 } else {
  var_1_96 = var_1_3;
 }
 if ((var_1_2 - (var_1_3 - var_1_4)) == var_1_54) {
  if ((var_1_3 + var_1_54) >= (var_1_4 / var_1_2)) {
   if (var_1_54 > var_1_4) {
    var_1_1 = ((var_1_3 + var_1_2) + var_1_46);
   } else {
    if (var_1_83 || (var_1_2 < ((((var_1_46) < (var_1_54)) ? (var_1_46) : (var_1_54))))) {
     var_1_1 = ((((var_1_46) < (((var_1_3 - var_1_2) + ((((var_1_4) < (64)) ? (var_1_4) : (64)))))) ? (var_1_46) : (((var_1_3 - var_1_2) + ((((var_1_4) < (64)) ? (var_1_4) : (64)))))));
    } else {
     if (var_1_83) {
      var_1_1 = ((((((var_1_8) < (var_1_9)) ? (var_1_8) : (var_1_9))) - var_1_4) - ((((var_1_3) < (var_1_2)) ? (var_1_3) : (var_1_2))));
     } else {
      var_1_1 = ((((-128) < (((var_1_9 - var_1_4) - ((((100) < (var_1_3)) ? (100) : (var_1_3)))))) ? (-128) : (((var_1_9 - var_1_4) - ((((100) < (var_1_3)) ? (100) : (var_1_3)))))));
     }
    }
   }
  }
 } else {
  var_1_1 = var_1_3;
 }
}
void updateVariables() {
 var_1_2 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_2 >= 127);
 assume_abort_if_not(var_1_2 <= 255);
 var_1_3 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_3 >= 63);
 assume_abort_if_not(var_1_3 <= 127);
 var_1_4 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_4 >= 0);
 assume_abort_if_not(var_1_4 <= 63);
 var_1_8 = __VERIFIER_nondet_long();
 assume_abort_if_not(var_1_8 >= 1073741822);
 assume_abort_if_not(var_1_8 <= 2147483646);
 var_1_9 = __VERIFIER_nondet_long();
 assume_abort_if_not(var_1_9 >= 1073741822);
 assume_abort_if_not(var_1_9 <= 2147483646);
 var_1_13 = __VERIFIER_nondet_ulong();
 assume_abort_if_not(var_1_13 >= 2147483647);
 assume_abort_if_not(var_1_13 <= 4294967294);
 var_1_15 = __VERIFIER_nondet_ushort();
 assume_abort_if_not(var_1_15 >= 16383);
 assume_abort_if_not(var_1_15 <= 32767);
 var_1_16 = __VERIFIER_nondet_ushort();
 assume_abort_if_not(var_1_16 >= 16383);
 assume_abort_if_not(var_1_16 <= 32767);
 var_1_18 = __VERIFIER_nondet_ulong();
 assume_abort_if_not(var_1_18 >= 2147483647);
 assume_abort_if_not(var_1_18 <= 4294967294);
 var_1_22 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_22 >= -922337.2036854776000e+13F && var_1_22 <= -1.0e-20F) || (var_1_22 <= 9223372.036854776000e+12F && var_1_22 >= 1.0e-20F ));
 assume_abort_if_not(var_1_22 != 0.0F);
 var_1_24 = __VERIFIER_nondet_ulong();
 assume_abort_if_not(var_1_24 >= 0);
 assume_abort_if_not(var_1_24 <= 8);
 var_1_25 = __VERIFIER_nondet_ulong();
 assume_abort_if_not(var_1_25 >= 0);
 assume_abort_if_not(var_1_25 <= 8);
 var_1_26 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_26 >= 1);
 assume_abort_if_not(var_1_26 <= 1);
 var_1_27 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_27 >= 0);
 assume_abort_if_not(var_1_27 <= 0);
 var_1_28 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_28 >= 0);
 assume_abort_if_not(var_1_28 <= 0);
 var_1_30 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_30 >= 127);
 assume_abort_if_not(var_1_30 <= 254);
 var_1_33 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_33 >= 191);
 assume_abort_if_not(var_1_33 <= 255);
 var_1_34 = __VERIFIER_nondet_double();
 assume_abort_if_not((var_1_34 >= 0.0F && var_1_34 <= -1.0e-20F) || (var_1_34 <= 2305843.009213691390e+12F && var_1_34 >= 1.0e-20F ));
 var_1_35 = __VERIFIER_nondet_double();
 assume_abort_if_not((var_1_35 >= 0.0F && var_1_35 <= -1.0e-20F) || (var_1_35 <= 4611686.018427382800e+12F && var_1_35 >= 1.0e-20F ));
 var_1_37 = __VERIFIER_nondet_long();
 assume_abort_if_not(var_1_37 >= 1073741823);
 assume_abort_if_not(var_1_37 <= 2147483647);
 var_1_40 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_40 >= 0.0F && var_1_40 <= -1.0e-20F) || (var_1_40 <= 4611686.018427382800e+12F && var_1_40 >= 1.0e-20F ));
 var_1_41 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_41 >= 4611686.018427382800e+12F && var_1_41 <= -1.0e-20F) || (var_1_41 <= 9223372.036854765600e+12F && var_1_41 >= 1.0e-20F ));
 var_1_45 = __VERIFIER_nondet_char();
 assume_abort_if_not(var_1_45 >= 0);
 assume_abort_if_not(var_1_45 <= 63);
 var_1_49 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_49 >= 190);
 assume_abort_if_not(var_1_49 <= 254);
 var_1_53 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_53 >= 0.0F && var_1_53 <= -1.0e-20F) || (var_1_53 <= 2305843.009213691390e+12F && var_1_53 >= 1.0e-20F ));
 var_1_55 = __VERIFIER_nondet_ulong();
 assume_abort_if_not(var_1_55 >= 536870911);
 assume_abort_if_not(var_1_55 <= 1073741823);
 var_1_56 = __VERIFIER_nondet_ushort();
 assume_abort_if_not(var_1_56 >= 32767);
 assume_abort_if_not(var_1_56 <= 65535);
 var_1_57 = __VERIFIER_nondet_ulong();
 assume_abort_if_not(var_1_57 >= 1073741823);
 assume_abort_if_not(var_1_57 <= 2147483647);
 var_1_59 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_59 >= -230584.3009213691390e+13F && var_1_59 <= -1.0e-20F) || (var_1_59 <= 2305843.009213691390e+12F && var_1_59 >= 1.0e-20F ));
 var_1_60 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_60 >= -230584.3009213691390e+13F && var_1_60 <= -1.0e-20F) || (var_1_60 <= 2305843.009213691390e+12F && var_1_60 >= 1.0e-20F ));
 var_1_61 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_61 >= -230584.3009213691390e+13F && var_1_61 <= -1.0e-20F) || (var_1_61 <= 2305843.009213691390e+12F && var_1_61 >= 1.0e-20F ));
 var_1_62 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_62 >= -230584.3009213691390e+13F && var_1_62 <= -1.0e-20F) || (var_1_62 <= 2305843.009213691390e+12F && var_1_62 >= 1.0e-20F ));
 var_1_65 = __VERIFIER_nondet_ushort();
 assume_abort_if_not(var_1_65 >= 32767);
 assume_abort_if_not(var_1_65 <= 65534);
 var_1_66 = __VERIFIER_nondet_ushort();
 assume_abort_if_not(var_1_66 >= 32767);
 assume_abort_if_not(var_1_66 <= 65534);
 var_1_67 = __VERIFIER_nondet_ushort();
 assume_abort_if_not(var_1_67 >= 49150);
 assume_abort_if_not(var_1_67 <= 65534);
 var_1_68 = __VERIFIER_nondet_ushort();
 assume_abort_if_not(var_1_68 >= 8191);
 assume_abort_if_not(var_1_68 <= 16383);
 var_1_75 = __VERIFIER_nondet_char();
 assume_abort_if_not(var_1_75 >= -15);
 assume_abort_if_not(var_1_75 <= 15);
 var_1_81 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_81 >= 1);
 assume_abort_if_not(var_1_81 <= 1);
}
void updateLastVariables() {
 last_1_var_1_1 = var_1_1;
 last_1_var_1_17 = var_1_17;
 last_1_var_1_23 = var_1_23;
 last_1_var_1_29 = var_1_29;
 last_1_var_1_44 = var_1_44;
 last_1_var_1_46 = var_1_46;
 last_1_var_1_47 = var_1_47;
 last_1_var_1_48 = var_1_48;
 last_1_var_1_50 = var_1_50;
 last_1_var_1_69 = var_1_69;
 last_1_var_1_71 = var_1_71;
 last_1_var_1_73 = var_1_73;
 last_1_var_1_76 = var_1_76;
 last_1_var_1_77 = var_1_77;
 last_1_var_1_88 = var_1_88;
 last_1_var_1_90 = var_1_90;
 last_1_var_1_92 = var_1_92;
 last_1_var_1_100 = var_1_100;
}
int property() {
 return ((((((((((((((((((((((((((((((((((((((((((((((((((((((var_1_2 - (var_1_3 - var_1_4)) == var_1_54) ? (((var_1_3 + var_1_54) >= (var_1_4 / var_1_2)) ? ((var_1_54 > var_1_4) ? (var_1_1 == ((signed long int) ((var_1_3 + var_1_2) + var_1_46))) : ((var_1_83 || (var_1_2 < ((((var_1_46) < (var_1_54)) ? (var_1_46) : (var_1_54))))) ? (var_1_1 == ((signed long int) ((((var_1_46) < (((var_1_3 - var_1_2) + ((((var_1_4) < (64)) ? (var_1_4) : (64)))))) ? (var_1_46) : (((var_1_3 - var_1_2) + ((((var_1_4) < (64)) ? (var_1_4) : (64))))))))) : (var_1_83 ? (var_1_1 == ((signed long int) ((((((var_1_8) < (var_1_9)) ? (var_1_8) : (var_1_9))) - var_1_4) - ((((var_1_3) < (var_1_2)) ? (var_1_3) : (var_1_2)))))) : (var_1_1 == ((signed long int) ((((-128) < (((var_1_9 - var_1_4) - ((((100) < (var_1_3)) ? (100) : (var_1_3)))))) ? (-128) : (((var_1_9 - var_1_4) - ((((100) < (var_1_3)) ? (100) : (var_1_3)))))))))))) : 1) : (var_1_1 == ((signed long int) var_1_3))) && (((31.75 + 15.5) < ((((var_1_58) > (var_1_87)) ? (var_1_58) : (var_1_87)))) ? (var_1_10 == ((unsigned long int) ((((var_1_13 - var_1_4) < 0 ) ? -(var_1_13 - var_1_4) : (var_1_13 - var_1_4))))) : (var_1_10 == ((unsigned long int) (256u + var_1_8))))) && ((var_1_9 > (var_1_3 ^ ((((var_1_2) > (4)) ? (var_1_2) : (4))))) ? (var_1_14 == ((unsigned short int) ((((var_1_4) < (var_1_2)) ? (var_1_4) : (var_1_2))))) : (var_1_14 == ((unsigned short int) (var_1_2 + (((((var_1_15) > (var_1_16)) ? (var_1_15) : (var_1_16))) - var_1_4)))))) && (var_1_23 ? ((var_1_43 > var_1_4) ? (var_1_17 == ((unsigned long int) (((((var_1_13) > (3076280705u)) ? (var_1_13) : (3076280705u))) - var_1_4))) : 1) : (var_1_17 == ((unsigned long int) (((((((((var_1_13) > (var_1_18)) ? (var_1_13) : (var_1_18))) - var_1_16)) > (var_1_2)) ? ((((((var_1_13) > (var_1_18)) ? (var_1_13) : (var_1_18))) - var_1_16)) : (var_1_2))))))) && (var_1_23 ? (var_1_19 == ((unsigned long int) (((((var_1_3 + ((((var_1_9) < (var_1_15)) ? (var_1_9) : (var_1_15))))) > (var_1_13)) ? ((var_1_3 + ((((var_1_9) < (var_1_15)) ? (var_1_9) : (var_1_15))))) : (var_1_13))))) : (var_1_19 == ((unsigned long int) ((((var_1_16) > ((var_1_29 + var_1_3))) ? (var_1_16) : ((var_1_29 + var_1_3)))))))) && (var_1_47 ? ((var_1_76 >= (- (var_1_32 / var_1_22))) ? (var_1_20 == ((signed short int) ((((var_1_2) < (((((var_1_3) > (var_1_4)) ? (var_1_3) : (var_1_4))))) ? (var_1_2) : (((((var_1_3) > (var_1_4)) ? (var_1_3) : (var_1_4)))))))) : 1) : 1)) && (((var_1_29 >> (var_1_24 + var_1_25)) <= var_1_100) ? ((var_1_50 == ((var_1_9 % var_1_16) * var_1_101)) ? (var_1_23 == ((unsigned char) (! (! var_1_26)))) : (var_1_23 == ((unsigned char) (! (var_1_27 || var_1_28))))) : 1)) && (var_1_29 == ((unsigned char) (var_1_30 - 32)))) && (var_1_31 == ((signed char) (4 - ((((var_1_25) < 0 ) ? -(var_1_25) : (var_1_25))))))) && ((((var_1_33 - var_1_4) - var_1_25) == var_1_16) ? (var_1_32 == ((double) (8.5 - ((8.05 + var_1_34) + var_1_35)))) : 1)) && (((last_1_var_1_1 / var_1_30) > (((((last_1_var_1_88) > (var_1_9)) ? (last_1_var_1_88) : (var_1_9))) - (var_1_37 - 2))) ? ((((((last_1_var_1_50) > (last_1_var_1_1)) ? (last_1_var_1_50) : (last_1_var_1_1))) > var_1_15) ? (var_1_36 == ((signed long int) ((((200) < 0 ) ? -(200) : (200))))) : 1) : (last_1_var_1_90 ? ((256u >= var_1_18) ? (last_1_var_1_23 ? (var_1_36 == ((signed long int) (50 - (1976409169 - var_1_25)))) : 1) : (var_1_28 ? (var_1_26 ? (var_1_36 == ((signed long int) (-10 + last_1_var_1_71))) : (var_1_36 == ((signed long int) var_1_16))) : (var_1_36 == ((signed long int) last_1_var_1_50)))) : (var_1_36 == ((signed long int) var_1_3))))) && ((16 <= (var_1_33 + var_1_63)) ? ((! (var_1_24 >= ((((var_1_16) < (256u)) ? (var_1_16) : (256u))))) ? ((15.6 >= (var_1_35 - 3.95)) ? (var_1_39 == ((float) (var_1_35 + ((((9.5f) > ((var_1_34 - var_1_40))) ? (9.5f) : ((var_1_34 - var_1_40))))))) : (var_1_39 == ((float) (((((var_1_40) < 0 ) ? -(var_1_40) : (var_1_40))) - (var_1_41 - var_1_34))))) : (var_1_39 == ((float) ((((var_1_41) < (var_1_35)) ? (var_1_41) : (var_1_35)))))) : (var_1_39 == ((float) ((((var_1_34) < (200.6f)) ? (var_1_34) : (200.6f))))))) && (var_1_26 ? ((((((var_1_102) < (var_1_8)) ? (var_1_102) : (var_1_8))) < ((var_1_10 * var_1_30) / -128)) ? (var_1_42 == ((signed char) var_1_4)) : 1) : ((! ((var_1_36 * var_1_64) < var_1_3)) ? (var_1_42 == ((signed char) var_1_33)) : 1))) && ((var_1_102 <= (var_1_37 / ((((var_1_13) > (var_1_33)) ? (var_1_13) : (var_1_33))))) ? (var_1_43 == ((unsigned char) var_1_30)) : 1)) && ((var_1_13 <= (- var_1_3)) ? ((var_1_23 || var_1_80) ? (var_1_44 == ((signed char) ((((16) > ((var_1_25 + var_1_4))) ? (16) : ((var_1_25 + var_1_4)))))) : (var_1_44 == ((signed char) ((((5) > (var_1_33)) ? (5) : (var_1_33)))))) : (var_1_44 == ((signed char) (var_1_45 + var_1_4))))) && (last_1_var_1_47 ? (var_1_46 == ((signed short int) ((((last_1_var_1_46) > (last_1_var_1_88)) ? (last_1_var_1_46) : (last_1_var_1_88))))) : (var_1_46 == ((signed short int) (var_1_2 + last_1_var_1_46))))) && ((var_1_2 >= (last_1_var_1_92 + var_1_25)) ? ((! (var_1_15 >= last_1_var_1_44)) ? (var_1_47 == ((unsigned char) ((! (var_1_27 || var_1_26)) || var_1_28))) : 1) : 1)) && ((var_1_46 <= var_1_3) ? (var_1_48 == ((unsigned char) ((var_1_49 - var_1_45) - ((((((((var_1_3) > (var_1_4)) ? (var_1_3) : (var_1_4)))) < (var_1_24)) ? (((((var_1_3) > (var_1_4)) ? (var_1_3) : (var_1_4)))) : (var_1_24)))))) : 1)) && ((200u >= var_1_24) ? (var_1_50 == ((unsigned long int) (var_1_4 + ((((1u) < ((var_1_33 + var_1_24))) ? (1u) : ((var_1_33 + var_1_24))))))) : (var_1_50 == ((unsigned long int) ((((var_1_45) < ((var_1_3 + var_1_2))) ? (var_1_45) : ((var_1_3 + var_1_2)))))))) && ((var_1_40 <= (var_1_35 - var_1_34)) ? (var_1_51 == ((unsigned short int) (47137 - var_1_16))) : 1)) && ((1 < (-64 * var_1_8)) ? (var_1_52 == ((float) (var_1_35 - ((var_1_34 + var_1_53) + var_1_40)))) : (var_1_52 == ((float) (0.75f - var_1_41))))) && (last_1_var_1_90 ? (var_1_54 == ((unsigned long int) ((last_1_var_1_77 + (var_1_55 - var_1_16)) + ((((var_1_2) > (var_1_24)) ? (var_1_2) : (var_1_24)))))) : (((var_1_56 - last_1_var_1_100) > var_1_8) ? (last_1_var_1_90 ? (var_1_26 ? ((last_1_var_1_76 < last_1_var_1_73) ? (var_1_54 == ((unsigned long int) last_1_var_1_100)) : (var_1_54 == ((unsigned long int) ((((((var_1_57 - last_1_var_1_69)) > ((var_1_45 + 10u))) ? ((var_1_57 - last_1_var_1_69)) : ((var_1_45 + 10u)))) + var_1_8)))) : (var_1_54 == ((unsigned long int) ((((var_1_15) > (last_1_var_1_77)) ? (var_1_15) : (last_1_var_1_77)))))) : (var_1_54 == ((unsigned long int) (var_1_13 - var_1_55)))) : (var_1_54 == ((unsigned long int) (var_1_8 + var_1_57)))))) && (var_1_58 == ((float) ((((((var_1_53) < (var_1_34)) ? (var_1_53) : (var_1_34))) + var_1_59) + (var_1_60 + ((((var_1_61) > (var_1_62)) ? (var_1_61) : (var_1_62)))))))) && (var_1_27 ? ((var_1_43 == (var_1_45 / var_1_49)) ? ((var_1_62 < (var_1_41 - var_1_53)) ? ((var_1_62 <= (((((var_1_53) < 0 ) ? -(var_1_53) : (var_1_53))) - var_1_40)) ? (var_1_63 == ((signed char) (var_1_4 + var_1_24))) : 1) : (var_1_63 == ((signed char) (var_1_4 + var_1_45)))) : 1) : (var_1_63 == ((signed char) (var_1_24 + -2))))) && (((16u <= var_1_102) && var_1_28) ? (var_1_64 == ((unsigned short int) (((((((((var_1_65) > (var_1_66)) ? (var_1_65) : (var_1_66)))) < (40384)) ? (((((var_1_65) > (var_1_66)) ? (var_1_65) : (var_1_66)))) : (40384))) - ((((var_1_16) > (var_1_3)) ? (var_1_16) : (var_1_3)))))) : (var_1_64 == ((unsigned short int) ((var_1_67 - (var_1_68 - var_1_45)) - var_1_30))))) && ((var_1_14 < var_1_42) ? (var_1_69 == ((unsigned long int) ((((var_1_3) < ((((((var_1_54) > (var_1_33)) ? (var_1_54) : (var_1_33))) + var_1_101))) ? (var_1_3) : ((((((var_1_54) > (var_1_33)) ? (var_1_54) : (var_1_33))) + var_1_101)))))) : 1)) && ((((((var_1_66) < ((- var_1_63))) ? (var_1_66) : ((- var_1_63)))) > (var_1_100 + var_1_15)) ? ((((((var_1_49) < (var_1_3)) ? (var_1_49) : (var_1_3))) > var_1_68) ? ((((((var_1_22) < ((- 128.975))) ? (var_1_22) : ((- 128.975)))) >= var_1_95) ? (var_1_71 == ((signed short int) ((var_1_97 + var_1_33) + var_1_20))) : 1) : 1) : ((var_1_46 >= var_1_46) ? (var_1_71 == ((signed short int) ((((var_1_67) > ((var_1_33 - var_1_36))) ? (var_1_67) : ((var_1_33 - var_1_36)))))) : (var_1_71 == ((signed short int) (((((var_1_49) < (var_1_33)) ? (var_1_49) : (var_1_33))) - var_1_20)))))) && ((var_1_60 != var_1_86) ? (var_1_28 ? (var_1_73 == ((double) var_1_61)) : (var_1_73 == ((double) var_1_60))) : (var_1_73 == ((double) var_1_61)))) && ((var_1_34 < (var_1_62 / ((((var_1_41) < (var_1_22)) ? (var_1_41) : (var_1_22))))) ? (var_1_74 == ((signed char) ((((var_1_25) < ((((((var_1_24) < (var_1_45)) ? (var_1_24) : (var_1_45))) + var_1_4))) ? (var_1_25) : ((((((var_1_24) < (var_1_45)) ? (var_1_24) : (var_1_45))) + var_1_4)))))) : ((var_1_49 >= ((var_1_33 - var_1_45) - var_1_4)) ? (var_1_74 == ((signed char) (((((var_1_25) < (var_1_4)) ? (var_1_25) : (var_1_4))) + -50))) : (var_1_74 == ((signed char) ((((var_1_4) < 0 ) ? -(var_1_4) : (var_1_4)))))))) && (((3.5 - var_1_34) > var_1_40) ? ((var_1_90 || var_1_26) ? (var_1_76 == ((float) (((((var_1_41 - var_1_35)) > ((var_1_53 + var_1_62))) ? ((var_1_41 - var_1_35)) : ((var_1_53 + var_1_62)))))) : 1) : (var_1_26 ? (var_1_76 == ((float) (((((var_1_53 - (var_1_41 - 256.6f))) < (((((var_1_60) > (var_1_35)) ? (var_1_60) : (var_1_35))))) ? ((var_1_53 - (var_1_41 - 256.6f))) : (((((var_1_60) > (var_1_35)) ? (var_1_60) : (var_1_35)))))))) : 1))) && ((var_1_48 != (var_1_4 / (var_1_9 + 5u))) ? ((((var_1_100 + var_1_51) + var_1_48) >= var_1_67) ? (var_1_77 == ((signed short int) ((var_1_45 + 5) + ((((((((var_1_3) < 0 ) ? -(var_1_3) : (var_1_3)))) > (var_1_14)) ? (((((var_1_3) < 0 ) ? -(var_1_3) : (var_1_3)))) : (var_1_14)))))) : (var_1_77 == ((signed short int) ((var_1_14 + var_1_33) + (var_1_10 + var_1_45))))) : (var_1_77 == ((signed short int) var_1_24)))) && ((((var_1_66 - var_1_45) + var_1_57) <= ((((128u) < (0u)) ? (128u) : (0u)))) ? (var_1_79 == ((signed short int) var_1_99)) : (var_1_79 == ((signed short int) var_1_33)))) && ((! (last_1_var_1_48 < last_1_var_1_1)) ? (var_1_80 == ((unsigned char) var_1_26)) : (var_1_80 == ((unsigned char) (var_1_26 && ((var_1_28 || var_1_81) && (! var_1_27))))))) && (var_1_90 ? (((var_1_2 != var_1_68) && var_1_81) ? (var_1_82 == ((double) (((((var_1_59 + var_1_53)) < (((5.8 + var_1_40) - var_1_41))) ? ((var_1_59 + var_1_53)) : (((5.8 + var_1_40) - var_1_41)))))) : 1) : (var_1_28 ? (var_1_82 == ((double) ((((0.8) > (((var_1_34 + var_1_35) - var_1_53))) ? (0.8) : (((var_1_34 + var_1_35) - var_1_53)))))) : 1))) && ((var_1_97 < (- 25u)) ? (var_1_81 ? ((var_1_17 > (var_1_45 - ((((var_1_3) < (var_1_24)) ? (var_1_3) : (var_1_24))))) ? (var_1_83 == ((unsigned char) ((var_1_10 == var_1_10) || var_1_26))) : 1) : 1) : (var_1_47 ? ((var_1_20 > var_1_51) ? (var_1_83 == ((unsigned char) 1)) : (var_1_83 == ((unsigned char) ((! var_1_28) && (var_1_27 || var_1_26))))) : 1))) && (((25 + var_1_36) < (var_1_13 - var_1_57)) ? (var_1_84 == ((signed char) (8 + var_1_45))) : (var_1_81 ? ((var_1_86 > (var_1_53 * 100.2f)) ? (var_1_84 == ((signed char) (((((var_1_45) < (var_1_4)) ? (var_1_45) : (var_1_4))) + var_1_75))) : (var_1_84 == ((signed char) ((var_1_25 + 8) + var_1_45)))) : (var_1_84 == ((signed char) ((((var_1_45) < (var_1_24)) ? (var_1_45) : (var_1_24)))))))) && (var_1_85 == ((unsigned long int) (((((var_1_13) < (var_1_18)) ? (var_1_13) : (var_1_18))) - var_1_68)))) && ((var_1_52 != var_1_61) ? (var_1_86 == ((float) var_1_40)) : (((- var_1_87) < var_1_53) ? (var_1_80 ? (var_1_86 == ((float) (((((var_1_35) > (var_1_60)) ? (var_1_35) : (var_1_60))) + (((((var_1_34) < (999.4f)) ? (var_1_34) : (999.4f))) + var_1_61)))) : (var_1_86 == ((float) var_1_60))) : 1))) && (var_1_81 ? (var_1_87 == ((float) ((((var_1_53) < 0 ) ? -(var_1_53) : (var_1_53))))) : 1)) && ((var_1_32 > (var_1_73 + var_1_59)) ? (var_1_88 == ((signed long int) (((((var_1_94 + 100)) > (var_1_36)) ? ((var_1_94 + 100)) : (var_1_36))))) : (var_1_88 == ((signed long int) var_1_25)))) && (var_1_89 == ((signed char) var_1_24))) && (var_1_90 == ((unsigned char) var_1_26))) && (var_1_91 == ((float) var_1_62))) && (var_1_47 ? (var_1_92 == ((signed long int) var_1_50)) : (var_1_92 == ((signed long int) var_1_4)))) && (var_1_93 == ((unsigned short int) var_1_63))) && (var_1_26 ? (var_1_94 == ((unsigned long int) var_1_68)) : (var_1_94 == ((unsigned long int) 8u)))) && (var_1_27 ? (var_1_95 == ((double) var_1_61)) : (var_1_95 == ((double) var_1_60)))) && (var_1_83 ? (var_1_96 == ((unsigned long int) 8u)) : (var_1_96 == ((unsigned long int) var_1_3)))) && (var_1_27 ? (var_1_97 == ((unsigned long int) var_1_51)) : (var_1_97 == ((unsigned long int) var_1_64)))) && (var_1_26 ? (var_1_99 == ((signed char) var_1_49)) : (var_1_99 == ((signed char) var_1_75)))) && (var_1_100 == ((unsigned char) var_1_4))) && (var_1_80 ? (var_1_101 == ((unsigned char) var_1_45)) : (var_1_101 == ((unsigned char) var_1_4)))) && ((last_1_var_1_88 >= (last_1_var_1_17 * last_1_var_1_69)) ? (var_1_102 == ((unsigned short int) (var_1_66 - ((var_1_25 + var_1_30) + last_1_var_1_29)))) : (var_1_102 == ((unsigned short int) (last_1_var_1_29 + var_1_68))))
;
}
int main(void) {
 isInitial = 1;
 initially();
 while (1) {
  updateLastVariables();
  updateVariables();
  step();
  __VERIFIER_assert(property());
  isInitial = 0;
 }
 return 0;
}