session memcmp_Why3_ide = NTP4Verif +
theories
  "memcmp_Why3_ide_VCmemcmp_loop_inv_N_RANGE_preserved_part1_goal7"
  "memcmp_Why3_ide_VCmemcmp_loop_inv_C1_RANGE_established_goal3"
  "memcmp_Why3_ide_VCmemcmp_loop_inv_COMPARE_preserved_goal6"
  "memcmp_Why3_ide_VCmemcmp_not_eq_post_part2_goal10"
  "memcmp_Why3_ide_VCmemcmp_eq_post_part1_goal9"
  "memcmp_Why3_ide_VCmemcmp_loop_term_decrease_goal8"
  "memcmp_Why3_ide_VCmemcmp_loop_inv_C1_RANGE_preserved_goal2"
  "memcmp_Why3_ide_VCmemcmp_disjoint_not_eq_eq_goal1"
  "memcmp_Why3_ide_VCmemcmp_complete_not_eq_eq_goal0"
  "memcmp_Why3_ide_VCmemcmp_loop_inv_C2_RANGE_preserved_goal4"
  "memcmp_Why3_ide_VCmemcmp_loop_inv_C2_RANGE_established_goal5"
