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 print_dbg_rac_result_model :
    print_normal:bool ->
    print_giant:bool ->
    int option ->
    (int * 'a * 'b * Check_ce.rac_result * 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 :
    Pdecl.known_map -> Model_parser.model -> Pinterp_core.oracle
  val model_of_exec_log :
    env:Env.env ->
    known_map:Decl.known_map ->
    prover_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 : 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 ->
    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
  val models_from_rac :
    limits:Call_provers.resource_limits ->
    ?verb_lvl:int ->
    ?compute_term:Pinterp_core.compute_term ->
    Pinterp_core.rac ->
    Env.env ->
    Pmodule.pmodule ->
    (Call_provers.prover_answer * Model_parser.model) list ->
    (Model_parser.model * Check_ce.rac_result * Check_ce.rac_result *
     Check_ce.classification)
    list
  val models_from_giant_step :
    limits:Call_provers.resource_limits ->
    ?verb_lvl:int ->
    ?compute_term:Pinterp_core.compute_term ->
    Pinterp_core.rac ->
    Env.env ->
    Pmodule.pmodule ->
    (Call_provers.prover_answer * Model_parser.model) list ->
    (Model_parser.model * Check_ce.rac_result) list
  val best_rac_result :
    (Model_parser.model * Check_ce.rac_result * Check_ce.rac_result *
     Check_ce.classification)
    list -> (Model_parser.model * Check_ce.classification) option
  val best_giant_step_result :
    (Model_parser.model * Check_ce.rac_result) list ->
    (Model_parser.model * Check_ce.rac_result) option
  val last_nonempty_model :
    env:Env.env ->
    known_map:Decl.known_map ->
    (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
  val warn_concrete_term : Loc.warning_id
end