session bsearch_Why3_ide = NTP4Verif +
theories
  "bsearch_Why3_ide_VCbsearch_assign_normal_part1_goal2"
  "bsearch_Why3_ide_VCbsearch_assign_normal_part2_goal3"
  "bsearch_Why3_ide_VCbsearch_assign_exit_part1_goal0"
  "bsearch_Why3_ide_VCbsearch_assign_exit_part2_goal1"
