text: #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_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_12_1;//CREST_scheduler::lock_0 
  int x_12_2;//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_20_2;//functioncall::param T0
  int x_20_3;//functioncall::param T0
  int x_21_0;//functioncall::param T0
  int x_21_1;//functioncall::param T0
  int x_21_2;//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_23_2;//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;//functioncall::param T1
  int x_39_1;//functioncall::param 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 T2
  int x_43_1;//functioncall::param T2
  int x_44_0;//functioncall::param T2
  int x_44_1;//functioncall::param T2
  int x_45_0;//i T2
  int x_45_1;//i T2
  int x_45_2;//i T2
  int x_45_3;//i T2
  int x_46_0;//rv T2
  int x_47_0;//rv T2
  int x_47_1;//rv T2
  int x_48_0;//blocksize T2
  int x_48_1;//blocksize T2
  int x_49_0;//functioncall::param T2
  int x_49_1;//functioncall::param T2
  int x_49_2;//functioncall::param T2
  int x_50_0;//apr_thread_mutex_lock::rv T2
  int x_50_1;//apr_thread_mutex_lock::rv T2
  int x_51_0;//functioncall::param T2
  int x_51_1;//functioncall::param T2
  int x_52_0;//status T2
  int x_52_1;//status T2
  int x_53_0;//functioncall::param T2
  int x_53_1;//functioncall::param 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_57_2;//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_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 = 2692284784;
  T_0_13_0: x_14_0 = 1974800992;
  T_0_14_0: x_15_0 = 0;
  T_0_15_0: x_16_0 = 306567652;
  T_0_16_0: x_16_1 = -1;
  T_0_17_0: x_17_0 = 0;
  T_0_18_0: x_18_0 = 602723486;
  T_0_19_0: x_18_1 = x_17_0;
  T_0_20_0: x_19_0 = 575316446;
  T_0_21_0: x_19_1 = 97;
  T_0_22_0: x_20_0 = 1263009208;
  T_0_23_0: x_20_1 = 0;
  T_0_24_0: x_21_0 = 330708567;
  T_0_25_0: x_21_1 = 0;
  T_0_26_0: x_22_0 = 1974796352;
  T_0_27_0: x_23_0 = 253890326;
  T_0_28_0: x_23_1 = x_22_0;
  T_0_29_0: x_24_0 = 1085347168;
  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 = 246740856;
  T_0_39_0: x_25_1 = 83;
  T_0_40_0: x_26_0 = 1637511837;
  T_0_41_0: x_26_1 = 1;
  T_0_42_0: x_27_0 = 497613114;
  T_0_43_0: x_27_1 = 1;
  T_0_44_0: x_28_0 = 2026836850;
  T_0_45_0: x_28_1 = 1;
  T_0_46_0: x_29_0 = 1121916300;
  T_0_47_0: x_29_1 = 82;
  T_0_48_0: x_30_0 = 572008975;
  T_0_49_0: x_30_1 = 90;
  T_0_50_0: x_31_0 = 1327222551;
  T_0_51_0: x_31_1 = 1;
  T_0_52_0: x_32_0 = 35503153;
  T_0_53_0: x_32_1 = 1;
  T_0_54_0: x_33_0 = 1226678124;
  T_0_55_0: x_33_1 = 2;
  T_0_56_0: x_34_0 = 1862110505;
  T_0_57_0: x_34_1 = 2;
  T_0_58_0: x_11_1 = 5;
  T_2_59_2: x_43_0 = 325429835;
  T_2_60_2: x_43_1 = x_33_1;
  T_2_61_2: x_44_0 = 1892044385;
  T_2_62_2: x_44_1 = x_34_1;
  T_2_63_2: x_45_0 = 0;
  T_2_64_2: x_46_0 = -2025459199;
  T_2_65_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0)  x_47_0 = 1981863856;
  T_2_66_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0)  x_48_0 = 11096;
  T_2_67_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0)  x_49_0 = 1585432646;
  T_2_68_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0)  x_49_1 = x_0_1;
  T_2_69_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && x_0_1 == x_49_1)  x_50_0 = 0;
  T_2_70_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && x_0_1 == x_49_1 && 0 == x_12_0 + 1)  x_12_1 = 2;
  T_2_71_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && x_0_1 == x_49_1 && 2 == x_12_1)  x_50_1 = 0;
  T_2_72_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && x_23_1 == 0 && 2 == x_12_1)  x_51_0 = 1964668816;
  T_2_73_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && x_23_1 == 0 && 2 == x_12_1)  x_51_1 = x_20_1 + -1*x_21_1 + x_24_1;
  T_2_74_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && x_23_1 == 0 && 2 == x_12_1)  x_20_2 = 0;
  T_2_75_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && x_23_1 == 0 && 2 == x_12_1)  x_21_2 = 0;
  T_2_76_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && x_23_1 == 0 && 2 == x_12_1)  x_23_2 = 1;
  T_2_77_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && 2 == x_12_1)  x_47_1 = 0;
  T_2_78_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && 0 == x_47_1 && 2 == x_12_1)  x_48_1 = x_49_1;
  T_2_79_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && 0 == x_47_1 && 2 == x_12_1)  x_20_3 = x_20_2 + x_48_1;
  T_2_80_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && 0 == x_47_1 && 2 == x_12_1)  x_49_2 = -1*x_48_1 + x_49_1;
  T_2_81_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && x_49_2 <= 0 && 2 == x_12_1)  x_52_0 = 0;
  T_2_82_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && x_49_2 <= 0 && 2 == x_12_1)  x_12_2 = -1;
  T_2_83_2: x_35_0 = 280445463;
  T_2_84_2: x_35_1 = x_27_1;
  T_2_85_2: x_36_0 = 922206922;
  T_1_86_1: x_36_1 = x_28_1;
  T_1_87_1: x_37_0 = 0;
  T_1_88_1: x_38_0 = -2023357951;
  T_1_89_1: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0 && x_18_1 != 0 && x_49_2 <= 0)  x_52_1 = 0;
  T_1_90_1: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0)  x_53_0 = 1256183799;
  T_1_91_1: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0)  x_53_1 = x_47_1;
  T_2_92_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0)  x_54_0 = 1635576202;
  T_2_93_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0)  x_54_1 = x_53_1;
  T_2_94_2: if (x_0_1 + x_44_1 > x_11_1 && x_0_1 != 0)  x_0_2 = 0;
  T_2_95_2: if (x_44_1 < x_11_1)  x_55_0 = 251108696;
  T_2_96_2: if (x_44_1 < x_11_1)  x_55_1 = 47658982577920;
  T_2_97_2: if (x_44_1 < x_11_1)  x_56_0 = 20531448;
  T_2_98_2: if (x_44_1 < x_11_1)  x_56_1 = x_0_2 + x_44_1;
  T_1_99_1: if (x_44_1 < x_11_1)  x_45_1 = 0;
  T_2_100_2: if (x_44_1 < x_11_1 && x_45_1 < x_43_1)  x_57_0 = 1221558678;
  T_2_101_2: if (x_44_1 < x_11_1 && x_45_1 < x_43_1)  x_57_1 = 47658982577920;
  T_2_102_2: if (x_44_1 < x_11_1)  x_45_2 = 1 + x_45_1;
  T_2_103_2: if (x_44_1 < x_11_1 && x_45_2 < x_43_1)  x_57_2 = 47658982577920;
  T_2_104_2: if (x_44_1 < x_11_1)  x_45_3 = 1 + x_45_2;
  T_2_105_2: if (x_44_1 < x_11_1)  x_58_0 = 1458127972;
  T_2_106_2: if (x_44_1 < x_11_1)  x_58_1 = 47658982577920;
  T_2_107_2: if (x_36_1 < x_11_1)  x_39_0 = 1088352508;
  T_1_108_1: if (x_36_1 < x_11_1)  x_39_1 = 47658980476672;
  T_1_109_1: if (x_36_1 < x_11_1)  x_40_0 = 1160602325;
  T_1_110_1: if (x_36_1 < x_11_1)  x_40_1 = x_0_2 + x_36_1;
  T_1_111_1: if (x_36_1 < x_11_1)  x_37_1 = 0;
  T_1_112_1: if (x_36_1 < x_11_1 && x_37_1 < x_35_1)  x_41_0 = 1764695624;
  T_1_113_1: if (x_36_1 < x_11_1 && x_37_1 < x_35_1)  x_41_1 = 47658980476672;
  T_1_114_1: if (x_36_1 < x_11_1)  x_37_2 = 1 + x_37_1;
  T_1_115_1: if (x_36_1 < x_11_1)  x_42_0 = 1691075994;
  T_1_116_1: if (x_36_1 < x_11_1)  x_42_1 = 47658980476672;
  T_1_117_1: if (x_44_1 < x_11_1)  x_0_3 = x_0_2 + x_44_1;
  T_1_118_1: if (x_36_1 < x_11_1)  x_0_4 = x_0_2 + x_36_1;
  T_1_119_1: if (x_44_1 < x_11_1)  x_59_0 = 1735918771;
  T_2_120_2: if (x_44_1 < x_11_1)  x_59_1 = 47658982577920;
  T_1_121_1: if (x_44_1 < x_11_1)  x_60_0 = 880221184;
  T_2_122_2: if (x_44_1 < x_11_1)  x_60_1 = 47658982577920;
  T_2_123_2: if (x_44_1 < x_11_1)  assert(x_0_4 == x_56_1);
  }
  