session strcmp_Why3_ide = NTP4Verif +
theories
  "strcmp_Why3_ide_VCstrcmp_disjoint_not_eq_not_eq_i_j_eq_part2_goal2"
  "strcmp_Why3_ide_VCstrcmp_disjoint_not_eq_not_eq_i_j_eq_part1_goal1"
  "strcmp_Why3_ide_VCstrcmp_loop_term_positive_goal13"
  "strcmp_Why3_ide_VCstrcmp_loop_inv_4_established_part2_goal11"
  "strcmp_Why3_ide_VCstrcmp_eq_post_part1_goal14"
  "strcmp_Why3_ide_VCstrcmp_not_eq_i_j_post_part2_goal16"
  "strcmp_Why3_ide_VCstrcmp_disjoint_not_eq_not_eq_i_j_eq_part3_goal3"
  "strcmp_Why3_ide_VCstrcmp_loop_inv_4_established_part1_goal10"
  "strcmp_Why3_ide_VCstrcmp_loop_inv_3_established_part1_goal6"
  "strcmp_Why3_ide_VCstrcmp_loop_inv_3_preserved_part1_goal4"
  "strcmp_Why3_ide_VCstrcmp_loop_inv_4_preserved_part2_goal9"
  "strcmp_Why3_ide_VCstrcmp_loop_inv_4_preserved_part1_goal8"
  "strcmp_Why3_ide_VCstrcmp_loop_inv_3_established_part2_goal7"
  "strcmp_Why3_ide_VCstrcmp_not_eq_post_part2_goal15"
  "strcmp_Why3_ide_VCstrcmp_loop_inv_7_preserved_goal12"
  "strcmp_Why3_ide_VCstrcmp_loop_inv_3_preserved_part2_goal5"
  "strcmp_Why3_ide_VCstrcmp_complete_not_eq_not_eq_i_j_eq_goal0"
