session strstr_Why3_ide = NTP4Verif +
theories
  "strstr_Why3_ide_VCstrstr_loop_inv_3_preserved_goal3"
  "strstr_Why3_ide_VCstrstr_call_memcmp_pre_5_goal15"
  "strstr_Why3_ide_VCstrstr_loop_term_positive_goal10"
  "strstr_Why3_ide_VCstrstr_assert_goal0"
  "strstr_Why3_ide_VCstrstr_loop_inv_3_established_goal4"
  "strstr_Why3_ide_VCstrstr_loop_inv_4_preserved_goal5"
  "strstr_Why3_ide_VCstrstr_loop_inv_2_preserved_goal2"
  "strstr_Why3_ide_VCstrstr_call_memcmp_pre_goal11"
  "strstr_Why3_ide_VCstrstr_assert_2_goal8"
  "strstr_Why3_ide_VCstrstr_loop_term_decrease_goal9"
  "strstr_Why3_ide_VCstrstr_call_memcmp_pre_4_goal14"
  "strstr_Why3_ide_VCstrstr_loop_inv_5_established_goal7"
  "strstr_Why3_ide_VCstrstr_not_exists_post_goal17"
  "strstr_Why3_ide_VCstrstr_exists_post_goal16"
  "strstr_Why3_ide_VCstrstr_loop_inv_preserved_goal1"
  "strstr_Why3_ide_VCstrstr_loop_inv_5_preserved_goal6"
  "strstr_Why3_ide_VCstrstr_call_memcmp_pre_2_goal12"
  "strstr_Why3_ide_VCstrstr_call_memcmp_pre_3_goal13"
