sig
  type rac_result_state =
      Res_normal
    | Res_fail of Pinterp_core.cntr_ctx * Term.term
    | Res_stuck of string
    | Res_incomplete of string
  val print_rac_result_state : Check_ce.rac_result_state Pp.pp
  type rac_result =
      RAC_not_done of string
    | RAC_done of Check_ce.rac_result_state * 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 Pp.pp
  val rac_execute :
    Pinterp.ctx ->
    Expr.rsymbol -> Check_ce.rac_result_state * Pinterp_core.Log.exec_log
  val oracle_of_model :
    Pmodule.pmodule -> Model_parser.model -> Pinterp_core.oracle
  val model_of_exec_log :
    original_model:Model_parser.model ->
    Pinterp_core.Log.exec_log -> 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 * Pinterp_core.Log.exec_log
  val report_verdict :
    ?check_ce:bool -> Env.env -> Check_ce.classification Pp.pp
  val print_classification_log_or_model :
    ?verb_lvl:int ->
    json:bool ->
    print_attrs:bool -> (Model_parser.model * Check_ce.classification) Pp.pp
  val print_model_classification :
    ?verb_lvl:int ->
    json:bool ->
    ?check_ce:bool ->
    Env.env -> (Model_parser.model * Check_ce.classification) Pp.pp
  val classify :
    vc_term_loc:Loc.position option ->
    vc_term_attrs:Ident.Sattr.t ->
    normal_result:Check_ce.rac_result_state * Pinterp_core.Log.exec_log ->
    giant_step_result:Check_ce.rac_result_state * Pinterp_core.Log.exec_log ->
    Check_ce.classification
  type strategy_from_rac =
      (int * Call_provers.prover_answer * Model_parser.model *
       Check_ce.rac_result * Check_ce.rac_result)
      list ->
      (int * Call_provers.prover_answer * Model_parser.model *
       Check_ce.rac_result * Check_ce.rac_result)
      list
  val best_non_empty_giant_step_rac_result : Check_ce.strategy_from_rac
  val last_non_empty_model : Check_ce.strategy_from_rac
  val get_rac_results :
    limits:Call_provers.resource_limits ->
    ?verb_lvl:int ->
    ?compute_term:Pinterp_core.compute_term ->
    ?only_giant_step:bool ->
    Pinterp_core.rac ->
    Env.env ->
    Pmodule.pmodule ->
    (Call_provers.prover_answer * Model_parser.model) list ->
    (int * Call_provers.prover_answer * Model_parser.model *
     Check_ce.rac_result * Check_ce.rac_result)
    list
  val select_model_from_verdict :
    (int * Call_provers.prover_answer * Model_parser.model *
     Check_ce.rac_result * Check_ce.rac_result)
    list -> (Model_parser.model * Check_ce.classification) option
  val select_model_from_giant_step_rac_results :
    ?strategy:Check_ce.strategy_from_rac ->
    (int * Call_provers.prover_answer * Model_parser.model *
     Check_ce.rac_result * Check_ce.rac_result)
    list -> (Model_parser.model * Check_ce.rac_result) option
  val select_model :
    limits:Call_provers.resource_limits ->
    ?verb_lvl:int ->
    ?compute_term:Pinterp_core.compute_term ->
    check_ce:bool ->
    Pinterp_core.rac ->
    Env.env ->
    Pmodule.pmodule ->
    (Call_provers.prover_answer * Model_parser.model) list ->
    (Model_parser.model * Check_ce.classification) option
  val select_model_last_non_empty :
    (Call_provers.prover_answer * Model_parser.model) list ->
    Model_parser.model option
  val debug_check_ce_rac_results : Debug.flag
  val debug_check_ce_categorization : Debug.flag
end