session kstrtobool_Why3_ide = NTP4Verif +
theories
  "kstrtobool_Why3_ide_VCkstrtobool_CORRECT_post_2_part3_goal7"
  "kstrtobool_Why3_ide_VCkstrtobool_CORRECT_post_2_part6_goal9"
  "kstrtobool_Why3_ide_VCkstrtobool_CORRECT_post_part7_goal5"
  "kstrtobool_Why3_ide_VCkstrtobool_INVAL_assign_part08_goal19"
  "kstrtobool_Why3_ide_VCkstrtobool_CORRECT_post_2_part2_goal6"
  "kstrtobool_Why3_ide_VCkstrtobool_CORRECT_post_part3_goal3"
  "kstrtobool_Why3_ide_VCkstrtobool_INVAL_post_part5_goal13"
  "kstrtobool_Why3_ide_VCkstrtobool_CORRECT_post_2_part4_goal8"
  "kstrtobool_Why3_ide_VCkstrtobool_INVAL_assign_part06_goal18"
  "kstrtobool_Why3_ide_VCkstrtobool_INVAL_assign_part02_goal16"
  "kstrtobool_Why3_ide_VCkstrtobool_complete_CORRECT_INVAL_goal0"
  "kstrtobool_Why3_ide_VCkstrtobool_CORRECT_post_3_part3_goal11"
  "kstrtobool_Why3_ide_VCkstrtobool_INVAL_post_part6_goal14"
  "kstrtobool_Why3_ide_VCkstrtobool_CORRECT_post_part5_goal4"
  "kstrtobool_Why3_ide_VCkstrtobool_CORRECT_post_part2_goal2"
  "kstrtobool_Why3_ide_VCkstrtobool_disjoint_CORRECT_INVAL_goal1"
  "kstrtobool_Why3_ide_VCkstrtobool_INVAL_post_part4_goal12"
  "kstrtobool_Why3_ide_VCkstrtobool_CORRECT_post_3_part2_goal10"
  "kstrtobool_Why3_ide_VCkstrtobool_INVAL_assign_part04_goal17"
  "kstrtobool_Why3_ide_VCkstrtobool_INVAL_post_part7_goal15"
