session strcpy_Why3_ide = NTP4Verif +
theories
  "strcpy_Why3_ide_VCstrcpy_loop_inv_4_preserved_part2_goal3"
  "strcpy_Why3_ide_VCstrcpy_loop_inv_9_preserved_part2_goal10"
  "strcpy_Why3_ide_VCstrcpy_loop_inv_13_preserved_goal14"
  "strcpy_Why3_ide_VCstrcpy_loop_inv_4_established_part2_goal4"
  "strcpy_Why3_ide_VCstrcpy_loop_term_positive_goal18"
  "strcpy_Why3_ide_VCstrcpy_loop_inv_8_established_part1_goal7"
  "strcpy_Why3_ide_VCstrcpy_assign_part11_goal17"
  "strcpy_Why3_ide_VCstrcpy_loop_inv_9_established_part1_goal11"
  "strcpy_Why3_ide_VCstrcpy_loop_inv_12_preserved_goal13"
  "strcpy_Why3_ide_VCstrcpy_loop_inv_4_preserved_part1_goal2"
  "strcpy_Why3_ide_VCstrcpy_assign_part05_goal16"
  "strcpy_Why3_ide_VCstrcpy_post_goal0"
  "strcpy_Why3_ide_VCstrcpy_post_2_goal1"
  "strcpy_Why3_ide_VCstrcpy_loop_inv_8_preserved_part1_goal5"
  "strcpy_Why3_ide_VCstrcpy_loop_inv_9_established_part2_goal12"
  "strcpy_Why3_ide_VCstrcpy_loop_inv_9_preserved_part1_goal9"
  "strcpy_Why3_ide_VCstrcpy_loop_assign_part5_goal15"
  "strcpy_Why3_ide_VCstrcpy_loop_inv_8_established_part2_goal8"
  "strcpy_Why3_ide_VCstrcpy_loop_inv_8_preserved_part2_goal6"
