sig
  type rac_result_state =
      Res_normal
    | Res_fail of Why3.Pinterp_core.cntr_ctx * Why3.Term.term
    | Res_stuck of string
    | Res_incomplete of string
  val print_rac_result_state : Check_ce.rac_result_state Why3.Pp.pp
  type rac_result =
      RAC_not_done of string
    | RAC_done of Check_ce.rac_result_state * Why3.Pinterp_core.Log.exec_log
  val string_of_rac_result_state : Check_ce.rac_result_state -> string
  val print_rac_result : ?verb_lvl:int -> Check_ce.rac_result Why3.Pp.pp
  val print_dbg_rac_result_model :
    print_normal:bool ->
    print_giant:bool ->
    int option ->
    (int * 'a * 'b * Check_ce.rac_result * Check_ce.rac_result) Why3.Pp.pp
  val rac_execute :
    Why3.Pinterp.ctx ->
    Why3.Expr.rsymbol ->
    Check_ce.rac_result_state * Why3.Pinterp_core.Log.exec_log
  val oracle_of_model :
    Why3.Pdecl.known_map ->
    Why3.Model_parser.model -> Why3.Pinterp_core.oracle
  val model_of_exec_log :
    env:Why3.Env.env ->
    known_map:Why3.Decl.known_map ->
    prover_model:Why3.Model_parser.model ->
    Why3.Pinterp_core.Log.exec_log -> Why3.Model_parser.model
  type verdict = NC | SW | NC_SW | BAD_CE of string | INCOMPLETE of string
  val string_of_verdict : Check_ce.verdict -> string
  type classification = Check_ce.verdict * Why3.Pinterp_core.Log.exec_log
  val report_verdict : Why3.Env.env -> Check_ce.classification Why3.Pp.pp
  val print_classification_log_or_model :
    ?verb_lvl:int ->
    json:bool ->
    print_attrs:bool ->
    (Why3.Model_parser.model * Check_ce.classification) Why3.Pp.pp
  val print_model_classification :
    ?verb_lvl:int ->
    json:bool ->
    Why3.Env.env ->
    (Why3.Model_parser.model * Check_ce.classification) Why3.Pp.pp
  val classify :
    vc_term_loc:Why3.Loc.position option ->
    vc_term_attrs:Why3.Ident.Sattr.t ->
    normal_result:Check_ce.rac_result_state * Why3.Pinterp_core.Log.exec_log ->
    giant_step_result:Check_ce.rac_result_state *
                      Why3.Pinterp_core.Log.exec_log ->
    Check_ce.classification
  val models_from_rac :
    limits:Why3.Call_provers.resource_limits ->
    ?verb_lvl:int ->
    ?compute_term:Why3.Pinterp_core.compute_term ->
    Why3.Pinterp_core.rac ->
    Why3.Env.env ->
    Why3.Pmodule.pmodule0 ->
    (Why3.Call_provers.prover_answer * Why3.Model_parser.model) list ->
    (Why3.Model_parser.model * Check_ce.rac_result * Check_ce.rac_result *
     Check_ce.classification)
    list
  val models_from_giant_step :
    limits:Why3.Call_provers.resource_limits ->
    ?verb_lvl:int ->
    ?compute_term:Why3.Pinterp_core.compute_term ->
    Why3.Pinterp_core.rac ->
    Why3.Env.env ->
    Why3.Pmodule.pmodule0 ->
    (Why3.Call_provers.prover_answer * Why3.Model_parser.model) list ->
    (Why3.Model_parser.model * Check_ce.rac_result) list
  val best_rac_result :
    (Why3.Model_parser.model * Check_ce.rac_result * Check_ce.rac_result *
     Check_ce.classification)
    list -> (Why3.Model_parser.model * Check_ce.classification) option
  val best_giant_step_result :
    (Why3.Model_parser.model * Check_ce.rac_result) list ->
    (Why3.Model_parser.model * Check_ce.rac_result) option
  val last_nonempty_model :
    env:Why3.Env.env ->
    known_map:Why3.Decl.known_map ->
    (Why3.Call_provers.prover_answer * Why3.Model_parser.model) list ->
    Why3.Model_parser.model option
  val debug_check_ce_rac_results : Why3.Debug.flag
  val debug_check_ce_categorization : Why3.Debug.flag
  val warn_concrete_term : Why3.Loc.warning_id
end