session float_quat_of_rmat_Why3_ide = NTP4Verif +
theories
  "float_quat_of_rmat_Why3_ide_VCfloat_quat_of_rmat_trace_pos_post_goal12"
  "float_quat_of_rmat_Why3_ide_VCfloat_quat_of_rmat_call_sqrtf_pre_finite_arg_goal1"
  "float_quat_of_rmat_Why3_ide_VCfloat_quat_of_rmat_call_sqrtf_pre_arg_positive_goal2"
  "float_quat_of_rmat_Why3_ide_VCfloat_quat_of_rmat_call_sqrtf_pre_finite_arg_2_goal3"
  "float_quat_of_rmat_Why3_ide_VCfloat_quat_of_rmat_call_sqrtf_pre_arg_positive_2_goal4"
  "float_quat_of_rmat_Why3_ide_VCfloat_quat_of_rmat_call_sqrtf_pre_finite_arg_3_goal5"
  "float_quat_of_rmat_Why3_ide_VCfloat_quat_of_rmat_call_sqrtf_pre_finite_arg_4_goal7"
  "float_quat_of_rmat_Why3_ide_VCfloat_quat_of_rmat_call_sqrtf_pre_arg_positive_4_goal8"
  "float_quat_of_rmat_Why3_ide_VCfloat_quat_of_rmat_a00_max_post_goal9"
  "float_quat_of_rmat_Why3_ide_VCfloat_quat_of_rmat_complete_a22_max_a11_max_a00_max_trace____goal0"
  "float_quat_of_rmat_Why3_ide_VCfloat_quat_of_rmat_call_sqrtf_pre_arg_positive_3_goal6"
  "float_quat_of_rmat_Why3_ide_VCfloat_quat_of_rmat_a22_max_post_goal11"
  "float_quat_of_rmat_Why3_ide_VCfloat_quat_of_rmat_a11_max_post_goal10"
