session strpbrk_Why3_ide = NTP4Verif +
theories
  "strpbrk_Why3_ide_VCstrpbrk_loop_inv_7_established_goal11"
  "strpbrk_Why3_ide_VCstrpbrk_found_post_goal19"
  "strpbrk_Why3_ide_VCstrpbrk_assert_4_goal16"
  "strpbrk_Why3_ide_VCstrpbrk_loop_inv_3_established_goal5"
  "strpbrk_Why3_ide_VCstrpbrk_loop_inv_established_goal2"
  "strpbrk_Why3_ide_VCstrpbrk_assert_goal13"
  "strpbrk_Why3_ide_VCstrpbrk_loop_inv_3_preserved_goal4"
  "strpbrk_Why3_ide_VCstrpbrk_loop_inv_6_preserved_goal9"
  "strpbrk_Why3_ide_VCstrpbrk_loop_inv_preserved_goal1"
  "strpbrk_Why3_ide_VCstrpbrk_loop_inv_4_preserved_goal6"
  "strpbrk_Why3_ide_VCstrpbrk_loop_inv_8_preserved_goal12"
  "strpbrk_Why3_ide_VCstrpbrk_post_goal0"
  "strpbrk_Why3_ide_VCstrpbrk_not_found_post_goal22"
  "strpbrk_Why3_ide_VCstrpbrk_assert_2_goal14"
  "strpbrk_Why3_ide_VCstrpbrk_loop_term_2_positive_goal18"
  "strpbrk_Why3_ide_VCstrpbrk_found_post_3_goal21"
  "strpbrk_Why3_ide_VCstrpbrk_loop_inv_5_preserved_goal7"
  "strpbrk_Why3_ide_VCstrpbrk_loop_term_positive_goal17"
  "strpbrk_Why3_ide_VCstrpbrk_loop_inv_7_preserved_goal10"
  "strpbrk_Why3_ide_VCstrpbrk_assert_3_goal15"
  "strpbrk_Why3_ide_VCstrpbrk_loop_inv_2_preserved_goal3"
  "strpbrk_Why3_ide_VCstrpbrk_loop_inv_5_established_goal8"
  "strpbrk_Why3_ide_VCstrpbrk_found_post_2_goal20"
