#ifdef COMPILE_FOR_TEST
#include <assert.h>
#define assume(cond) assert(cond)
#endif

void main(int argc, char* argv[]) {
int x_0_0;//sh_buf.outcnt 
int x_0_1;//sh_buf.outcnt 
int x_0_2;//sh_buf.outcnt 
int x_0_3;//sh_buf.outcnt 
int x_0_4;//sh_buf.outcnt 
int x_0_5;//sh_buf.outcnt 
int x_0_6;//sh_buf.outcnt 
int x_0_7;//sh_buf.outcnt 
int x_1_0;//sh_buf.outbuf[0] 
int x_1_1;//sh_buf.outbuf[0] 
int x_2_0;//sh_buf.outbuf[1] 
int x_2_1;//sh_buf.outbuf[1] 
int x_3_0;//sh_buf.outbuf[2] 
int x_3_1;//sh_buf.outbuf[2] 
int x_4_0;//sh_buf.outbuf[3] 
int x_4_1;//sh_buf.outbuf[3] 
int x_5_0;//sh_buf.outbuf[4] 
int x_5_1;//sh_buf.outbuf[4] 
int x_6_0;//sh_buf.outbuf[5] 
int x_7_0;//sh_buf.outbuf[6] 
int x_8_0;//sh_buf.outbuf[7] 
int x_9_0;//sh_buf.outbuf[8] 
int x_10_0;//sh_buf.outbuf[9] 
int x_11_0;//LOG_BUFSIZE 
int x_11_1;//LOG_BUFSIZE 
int x_12_0;//CREST_scheduler::lock_0 
int x_13_0;//t3 T0
int x_14_0;//t2 T0
int x_15_0;//arg T0
int x_16_0;//functioncall::param T0
int x_16_1;//functioncall::param T0
int x_17_0;//buffered T0
int x_18_0;//functioncall::param T0
int x_18_1;//functioncall::param T0
int x_19_0;//functioncall::param T0
int x_19_1;//functioncall::param T0
int x_20_0;//functioncall::param T0
int x_20_1;//functioncall::param T0
int x_21_0;//functioncall::param T0
int x_21_1;//functioncall::param T0
int x_22_0;//direction T0
int x_23_0;//functioncall::param T0
int x_23_1;//functioncall::param T0
int x_24_0;//functioncall::param T0
int x_24_1;//functioncall::param T0
int x_25_0;//functioncall::param T0
int x_25_1;//functioncall::param T0
int x_26_0;//functioncall::param T0
int x_26_1;//functioncall::param T0
int x_27_0;//functioncall::param T0
int x_27_1;//functioncall::param T0
int x_28_0;//functioncall::param T0
int x_28_1;//functioncall::param T0
int x_29_0;//functioncall::param T0
int x_29_1;//functioncall::param T0
int x_30_0;//functioncall::param T0
int x_30_1;//functioncall::param T0
int x_31_0;//functioncall::param T0
int x_31_1;//functioncall::param T0
int x_32_0;//functioncall::param T0
int x_32_1;//functioncall::param T0
int x_33_0;//functioncall::param T0
int x_33_1;//functioncall::param T0
int x_34_0;//functioncall::param T0
int x_34_1;//functioncall::param T0
int x_35_0;//functioncall::param T1
int x_35_1;//functioncall::param T1
int x_36_0;//functioncall::param T1
int x_36_1;//functioncall::param T1
int x_37_0;//i T1
int x_37_1;//i T1
int x_37_2;//i T1
int x_38_0;//rv T1
int x_39_0;//rv T1
int x_39_1;//rv T1
int x_40_0;//functioncall::param T1
int x_40_1;//functioncall::param T1
int x_41_0;//functioncall::param T1
int x_41_1;//functioncall::param T1
int x_42_0;//functioncall::param T1
int x_42_1;//functioncall::param T1
int x_43_0;//functioncall::param T1
int x_43_1;//functioncall::param T1
int x_44_0;//functioncall::param T1
int x_44_1;//functioncall::param T1
int x_45_0;//functioncall::param T1
int x_45_1;//functioncall::param T1
int x_46_0;//functioncall::param T1
int x_46_1;//functioncall::param T1
int x_47_0;//functioncall::param T1
int x_47_1;//functioncall::param T1
int x_48_0;//functioncall::param T1
int x_48_1;//functioncall::param T1
int x_49_0;//functioncall::param T2
int x_49_1;//functioncall::param T2
int x_50_0;//functioncall::param T2
int x_50_1;//functioncall::param T2
int x_51_0;//i T2
int x_51_1;//i T2
int x_51_2;//i T2
int x_51_3;//i T2
int x_52_0;//rv T2
int x_53_0;//rv T2
int x_53_1;//rv T2
int x_54_0;//functioncall::param T2
int x_54_1;//functioncall::param T2
int x_55_0;//functioncall::param T2
int x_55_1;//functioncall::param T2
int x_56_0;//functioncall::param T2
int x_56_1;//functioncall::param T2
int x_57_0;//functioncall::param T2
int x_57_1;//functioncall::param T2
int x_58_0;//functioncall::param T2
int x_58_1;//functioncall::param T2
int x_59_0;//functioncall::param T2
int x_59_1;//functioncall::param T2
int x_59_2;//functioncall::param T2
int x_60_0;//functioncall::param T2
int x_60_1;//functioncall::param T2

T_0_0_0: x_0_0 = 0;
T_0_1_0: x_1_0 = 0;
T_0_2_0: x_2_0 = 0;
T_0_3_0: x_3_0 = 0;
T_0_4_0: x_4_0 = 0;
T_0_5_0: x_5_0 = 0;
T_0_6_0: x_6_0 = 0;
T_0_7_0: x_7_0 = 0;
T_0_8_0: x_8_0 = 0;
T_0_9_0: x_9_0 = 0;
T_0_10_0: x_10_0 = 0;
T_0_11_0: x_11_0 = 0;
T_0_12_0: x_13_0 = 1697663424;
T_0_13_0: x_14_0 = 901907040;
T_0_14_0: x_15_0 = 0;
T_0_15_0: x_16_0 = 212179953;
T_0_16_0: x_16_1 = -1;
T_0_17_0: x_17_0 = 0;
T_0_18_0: x_18_0 = 1380393363;
T_0_19_0: x_18_1 = x_17_0;
T_0_20_0: x_19_0 = 2069386296;
T_0_21_0: x_19_1 = 97;
T_0_22_0: x_20_0 = 1338815156;
T_0_23_0: x_20_1 = 0;
T_0_24_0: x_21_0 = 1474106319;
T_0_25_0: x_21_1 = 0;
T_0_26_0: x_22_0 = 901902400;
T_0_27_0: x_23_0 = 1320036158;
T_0_28_0: x_23_1 = x_22_0;
T_0_29_0: x_24_0 = 737524459;
T_0_30_0: x_24_1 = 0;
T_0_31_0: x_12_0 = -1;
T_0_32_0: x_0_1 = 5;
T_0_33_0: x_1_1 = 72;
T_0_34_0: x_2_1 = 69;
T_0_35_0: x_3_1 = 76;
T_0_36_0: x_4_1 = 76;
T_0_37_0: x_5_1 = 79;
T_0_38_0: x_25_0 = 109999608;
T_0_39_0: x_25_1 = 83;
T_0_40_0: x_26_0 = 130415466;
T_0_41_0: x_26_1 = 1;
T_0_42_0: x_27_0 = 377193742;
T_0_43_0: x_27_1 = 1;
T_0_44_0: x_28_0 = 9768864;
T_0_45_0: x_28_1 = 1;
T_0_46_0: x_29_0 = 261775239;
T_0_47_0: x_29_1 = 82;
T_0_48_0: x_30_0 = 1142416626;
T_0_49_0: x_30_1 = 90;
T_0_50_0: x_31_0 = 1825571830;
T_0_51_0: x_31_1 = 1;
T_0_52_0: x_32_0 = 699990639;
T_0_53_0: x_32_1 = 1;
T_0_54_0: x_33_0 = 523640966;
T_0_55_0: x_33_1 = 2;
T_0_56_0: x_34_0 = 711277958;
T_0_57_0: x_34_1 = 2;
T_0_58_0: x_11_1 = 5;
T_1_59_1: x_35_0 = 1375239949;
T_1_60_1: x_35_1 = x_27_1;
T_1_61_1: x_36_0 = 1945409727;
T_1_62_1: x_36_1 = x_28_1;
T_1_63_1: x_37_0 = 0;
T_1_64_1: x_38_0 = -950463999;
T_2_65_2: x_49_0 = 332699735;
T_2_66_2: x_49_1 = x_33_1;
T_2_67_2: x_50_0 = 252167031;
T_2_68_2: x_50_1 = x_34_1;
T_2_69_2: x_51_0 = 0;
T_2_70_2: x_52_0 = -952565247;
T_2_71_2: if (x_0_1 + x_50_1 > x_11_1 && x_0_1 != 0)  x_53_0 = 908969904;
T_1_72_1: if (x_0_1 + x_36_1 > x_11_1 && x_0_1 != 0)  x_39_0 = 908969904;
T_1_73_1: if (x_0_1 + x_36_1 > x_11_1 && x_0_1 != 0 && x_18_1 == 0 && x_18_1 == 0)  x_40_0 = 403544067;
T_1_74_1: if (x_0_1 + x_36_1 > x_11_1 && x_0_1 != 0 && x_18_1 == 0 && x_18_1 == 0)  x_40_1 = -1;
T_1_75_1: if (x_0_1 + x_36_1 > x_11_1 && x_0_1 != 0 && x_18_1 == 0 && x_18_1 == 0)  x_39_1 = x_40_1;
T_1_76_1: if (x_0_1 + x_36_1 > x_11_1 && x_0_1 != 0 && x_18_1 == 0 && x_39_1 + 1 == 0)  x_0_2 = 0;
T_1_77_1: if (x_0_1 + x_36_1 > x_11_1 && x_0_1 != 0)  x_41_0 = 23321305;
T_1_78_1: if (x_0_1 + x_36_1 > x_11_1 && x_0_1 != 0)  x_41_1 = 9;
T_1_79_1: if (x_0_1 + x_36_1 > x_11_1 && x_0_1 != 0)  x_42_0 = 1603863562;
T_1_80_1: if (x_0_1 + x_36_1 > x_11_1 && x_0_1 != 0)  x_42_1 = x_41_1;
T_1_81_1: if (x_0_1 + x_36_1 > x_11_1 && x_0_1 != 0)  x_0_3 = 0;
T_1_82_1: if (x_36_1 < x_11_1)  x_43_0 = 1537988727;
T_1_83_1: if (x_36_1 < x_11_1)  x_43_1 = 47456044119808;
T_1_84_1: if (x_0_1 + x_50_1 > x_11_1 && x_0_1 != 0 && x_18_1 == 0 && x_18_1 == 0)  x_54_0 = 460393066;
T_1_85_1: if (x_0_1 + x_50_1 > x_11_1 && x_0_1 != 0 && x_18_1 == 0 && x_18_1 == 0)  x_54_1 = -1;
T_1_86_1: if (x_0_1 + x_50_1 > x_11_1 && x_0_1 != 0 && x_18_1 == 0 && x_18_1 == 0)  x_53_1 = x_54_1;
T_2_87_2: if (x_0_1 + x_50_1 > x_11_1 && x_0_1 != 0 && x_18_1 == 0 && x_53_1 + 1 == 0)  x_0_4 = 0;
T_2_88_2: if (x_36_1 < x_11_1)  x_44_0 = 408900919;
T_2_89_2: if (x_36_1 < x_11_1)  x_44_1 = x_0_3 + x_36_1;
T_2_90_2: if (x_36_1 < x_11_1)  x_37_1 = 0;
T_1_91_1: if (x_36_1 < x_11_1 && x_37_1 < x_35_1)  x_45_0 = 1735312804;
T_1_92_1: if (x_36_1 < x_11_1 && x_37_1 < x_35_1)  x_45_1 = 47456044119808;
T_1_93_1: if (x_36_1 < x_11_1)  x_37_2 = 1 + x_37_1;
T_1_94_1: if (x_36_1 < x_11_1)  x_46_0 = 383833922;
T_1_95_1: if (x_36_1 < x_11_1)  x_46_1 = 47456044119808;
T_1_96_1: if (x_0_1 + x_50_1 > x_11_1 && x_0_1 != 0)  x_55_0 = 581727840;
T_1_97_1: if (x_0_1 + x_50_1 > x_11_1 && x_0_1 != 0)  x_55_1 = 9;
T_1_98_1: if (x_0_1 + x_50_1 > x_11_1 && x_0_1 != 0)  x_56_0 = 415965933;
T_1_99_1: if (x_0_1 + x_50_1 > x_11_1 && x_0_1 != 0)  x_56_1 = x_55_1;
T_2_100_2: if (x_0_1 + x_50_1 > x_11_1 && x_0_1 != 0)  x_0_5 = 0;
T_2_101_2: if (x_50_1 < x_11_1)  x_57_0 = 596013875;
T_2_102_2: if (x_50_1 < x_11_1)  x_57_1 = 47456046221056;
T_2_103_2: if (x_36_1 < x_11_1)  x_0_6 = x_0_4 + x_36_1;
T_2_104_2: if (x_50_1 < x_11_1)  x_58_0 = 1962121203;
T_2_105_2: if (x_50_1 < x_11_1)  x_58_1 = x_0_5 + x_50_1;
T_2_106_2: if (x_50_1 < x_11_1)  x_51_1 = 0;
T_2_107_2: if (x_50_1 < x_11_1 && x_51_1 < x_49_1)  x_59_0 = 337868581;
T_2_108_2: if (x_50_1 < x_11_1 && x_51_1 < x_49_1)  x_59_1 = 47456046221056;
T_2_109_2: if (x_50_1 < x_11_1)  x_51_2 = 1 + x_51_1;
T_2_110_2: if (x_50_1 < x_11_1 && x_51_2 < x_49_1)  x_59_2 = 47456046221056;
T_2_111_2: if (x_50_1 < x_11_1)  x_51_3 = 1 + x_51_2;
T_2_112_2: if (x_50_1 < x_11_1)  x_60_0 = 1934829032;
T_2_113_2: if (x_50_1 < x_11_1)  x_60_1 = 47456046221056;
T_2_114_2: if (x_36_1 < x_11_1)  x_47_0 = 1288743874;
T_2_115_2: if (x_36_1 < x_11_1)  x_47_1 = 47456044119808;
T_2_116_2: if (x_50_1 < x_11_1)  x_0_7 = x_0_6 + x_50_1;
T_2_117_2: if (x_36_1 < x_11_1)  x_48_0 = 1657904739;
T_1_118_1: if (x_36_1 < x_11_1)  x_48_1 = 47456044119808;
T_1_119_1: if (x_36_1 < x_11_1)  assert(x_0_7 == x_44_1);
}
