sig
  type prover_answer =
      Valid
    | Invalid
    | Timeout
    | OutOfMemory
    | StepLimitExceeded
    | Unknown of string
    | Failure of string
    | HighFailure of string
  type prover_result = {
    pr_answer : Call_provers.prover_answer;
    pr_status : Unix.process_status;
    pr_output : string;
    pr_time : float;
    pr_steps : int;
    pr_models : (Call_provers.prover_answer * Model_parser.model) list;
  }
  val print_prover_answer :
    Stdlib.Format.formatter -> Call_provers.prover_answer -> unit
  val print_prover_result :
    ?json:bool ->
    Stdlib.Format.formatter -> Call_provers.prover_result -> unit
  val json_prover_result : Call_provers.prover_result -> Json_base.json
  val debug : Debug.flag
  type timeregexp
  type stepregexp
  val timeregexp : string -> Call_provers.timeregexp
  val stepregexp : string -> int -> Call_provers.stepregexp
  type prover_result_parser = {
    prp_regexps : (string * Call_provers.prover_answer) list;
    prp_timeregexps : Call_provers.timeregexp list;
    prp_stepregexps : Call_provers.stepregexp list;
    prp_exitcodes : (int * Call_provers.prover_answer) list;
    prp_model_parser : Model_parser.model_parser;
  }
  type prover_call
  type resource_limits = {
    limit_time : float;
    limit_mem : int;
    limit_steps : int;
  }
  val empty_limits : Call_provers.resource_limits
  val limit_max :
    Call_provers.resource_limits ->
    Call_provers.resource_limits -> Call_provers.resource_limits
  val call_editor :
    config:Whyconf.main ->
    command:string -> string -> Call_provers.prover_call
  val call_on_buffer :
    command:string ->
    config:Whyconf.main ->
    limits:Call_provers.resource_limits ->
    res_parser:Call_provers.prover_result_parser ->
    filename:string ->
    get_model:Printer.printing_info option ->
    gen_new_file:bool ->
    ?inplace:bool -> Stdlib.Buffer.t -> Call_provers.prover_call
  type prover_update =
      NoUpdates
    | ProverInterrupted
    | InternalFailure of exn
    | ProverStarted
    | ProverFinished of Call_provers.prover_result
  val get_new_results :
    blocking:bool ->
    (Call_provers.prover_call * Call_provers.prover_update) list
  val query_call : Call_provers.prover_call -> Call_provers.prover_update
  val interrupt_call :
    config:Whyconf.main -> Call_provers.prover_call -> unit
  val wait_on_call : Call_provers.prover_call -> Call_provers.prover_result
  val debug_attrs : Debug.flag
end