session strcasecmp_Why3_ide = NTP4Verif +
theories
  "strcasecmp_Why3_ide_VCstrcasecmp_loop_inv_5_preserved_goal12"
  "strcasecmp_Why3_ide_VCstrcasecmp_call_toupper_pre_part1_2_goal16"
  "strcasecmp_Why3_ide_VCstrcasecmp_disjoint_not_eq_not_eq_i_j_eq_part3_goal3"
  "strcasecmp_Why3_ide_VCstrcasecmp_loop_inv_preserved_part1_goal4"
  "strcasecmp_Why3_ide_VCstrcasecmp_call_toupper_pre_part2_goal15"
  "strcasecmp_Why3_ide_VCstrcasecmp_loop_inv_2_preserved_part1_goal8"
  "strcasecmp_Why3_ide_VCstrcasecmp_disjoint_not_eq_not_eq_i_j_eq_part1_goal1"
  "strcasecmp_Why3_ide_VCstrcasecmp_loop_inv_established_part1_goal6"
  "strcasecmp_Why3_ide_VCstrcasecmp_disjoint_not_eq_not_eq_i_j_eq_part2_goal2"
  "strcasecmp_Why3_ide_VCstrcasecmp_loop_inv_2_established_part1_goal10"
  "strcasecmp_Why3_ide_VCstrcasecmp_loop_term_positive_goal13"
  "strcasecmp_Why3_ide_VCstrcasecmp_complete_not_eq_not_eq_i_j_eq_goal0"
  "strcasecmp_Why3_ide_VCstrcasecmp_loop_inv_2_established_part2_goal11"
  "strcasecmp_Why3_ide_VCstrcasecmp_loop_inv_2_preserved_part2_goal9"
  "strcasecmp_Why3_ide_VCstrcasecmp_call_toupper_pre_part1_goal14"
  "strcasecmp_Why3_ide_VCstrcasecmp_loop_inv_preserved_part2_goal5"
  "strcasecmp_Why3_ide_VCstrcasecmp_not_eq_post_part2_goal19"
  "strcasecmp_Why3_ide_VCstrcasecmp_call_toupper_pre_part2_2_goal17"
  "strcasecmp_Why3_ide_VCstrcasecmp_not_eq_i_j_post_part2_goal20"
  "strcasecmp_Why3_ide_VCstrcasecmp_loop_inv_established_part2_goal7"
  "strcasecmp_Why3_ide_VCstrcasecmp_eq_post_part1_goal18"
