session strtok_r_Why3_ide = NTP4Verif +
theories
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_3_preserved_part1_goal8"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_5_part05_goal36"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_3_part1_goal28"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_5_part11_goal42"
  "strtok_r_Why3_ide_VCstrtok_r_assign_normal_part2_goal20"
  "strtok_r_Why3_ide_VCstrtok_r_assign_exit_part3_goal17"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_3_part2_goal29"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_4_preserved_part4_goal13"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_2_established_part2_goal7"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_5_part08_goal39"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_4_part2_goal31"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_4_preserved_part1_goal10"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_preserved_part2_goal1"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_5_part06_goal37"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_4_part1_goal30"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_2_preserved_part1_goal2"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_4_established_part1_goal14"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_2_part2_goal27"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_5_part02_goal33"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_4_preserved_part2_goal11"
  "strtok_r_Why3_ide_VCstrtok_r_assign_exit_part2_goal16"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_5_part03_goal34"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_5_part10_goal41"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_5_part09_goal40"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_part2_goal25"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_part1_goal24"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_4_preserved_part3_goal12"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_5_part04_goal35"
  "strtok_r_Why3_ide_VCstrtok_r_assign_normal_part5_goal23"
  "strtok_r_Why3_ide_VCstrtok_r_assign_normal_part3_goal21"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_2_part1_goal26"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_2_preserved_part4_goal5"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_2_preserved_part3_goal4"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_3_preserved_part2_goal9"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_4_established_part2_goal15"
  "strtok_r_Why3_ide_VCstrtok_r_assign_normal_part4_goal22"
  "strtok_r_Why3_ide_VCstrtok_r_assign_exit_part5_goal19"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_5_part07_goal38"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_2_established_part1_goal6"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_2_preserved_part2_goal3"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_5_part12_goal43"
  "strtok_r_Why3_ide_VCstrtok_r_loop_inv_preserved_part1_goal0"
  "strtok_r_Why3_ide_VCstrtok_r_assign_exit_part4_goal18"
  "strtok_r_Why3_ide_VCstrtok_r_call_strsep_pre_5_part01_goal32"
