session _fwrite_Why3_ide = NTP4Verif +
theories
  "X_fwrite_Why3_ide_VC_fwrite_call_fwrite_noflush_pre_3_part8_goal20"
  "X_fwrite_Why3_ide_VC_fwrite_call_fwrite_noflush_pre_3_part3_2_goal19"
  "X_fwrite_Why3_ide_VC_fwrite_loop_inv_preserved_goal7"
  "X_fwrite_Why3_ide_VC_fwrite_call_fwrite_noflush_pre_3_part1_goal13"
  "X_fwrite_Why3_ide_VC_fwrite_loop_inv_2_preserved_part1_goal8"
  "X_fwrite_Why3_ide_VC_fwrite_disjoint_def_ionbf_iolbf_iofbf_part1_goal1"
  "X_fwrite_Why3_ide_VC_fwrite_call_fwrite_noflush_pre_2_part4_goal12"
  "X_fwrite_Why3_ide_VC_fwrite_call_fwrite_noflush_pre_3_part4_goal14"
  "X_fwrite_Why3_ide_VC_fwrite_call_fwrite_noflush_pre_2_part8_goal17"
  "X_fwrite_Why3_ide_VC_fwrite_loop_inv_3_preserved_part1_goal9"
  "X_fwrite_Why3_ide_VC_fwrite_loop_term_decrease_goal11"
  "X_fwrite_Why3_ide_VC_fwrite_complete_def_ionbf_iolbf_iofbf_goal0"
  "X_fwrite_Why3_ide_VC_fwrite_disjoint_def_ionbf_iolbf_iofbf_part2_goal2"
  "X_fwrite_Why3_ide_VC_fwrite_call___fflush_pre_part1_goal15"
  "X_fwrite_Why3_ide_VC_fwrite_disjoint_def_ionbf_iolbf_iofbf_part3_goal3"
  "X_fwrite_Why3_ide_VC_fwrite_disjoint_def_ionbf_iolbf_iofbf_part5_goal5"
  "X_fwrite_Why3_ide_VC_fwrite_call___fflush_pre_part4_goal16"
  "X_fwrite_Why3_ide_VC_fwrite_loop_inv_4_preserved_goal10"
  "X_fwrite_Why3_ide_VC_fwrite_disjoint_def_ionbf_iolbf_iofbf_part6_goal6"
  "X_fwrite_Why3_ide_VC_fwrite_call_fwrite_noflush_pre_3_part2_2_goal18"
  "X_fwrite_Why3_ide_VC_fwrite_disjoint_def_ionbf_iolbf_iofbf_part4_goal4"
