sig
  val init_real : int * int * int -> unit
  type ctx
  val mk_empty_env :
    Why3.Env.env -> Why3.Pmodule.pmodule0 -> Why3.Pinterp_core.env
  val mk_rac :
    ?ignore_incomplete:bool ->
    Why3.Pinterp_core.check_term -> Why3.Pinterp_core.rac
  val mk_ctx :
    Why3.Pinterp_core.env ->
    limits:Why3.Call_provers.resource_limits ->
    ?giant_steps:bool ->
    ?do_rac:bool ->
    ?rac:Why3.Pinterp_core.rac ->
    ?oracle:Why3.Pinterp_core.oracle ->
    ?compute_term:(Why3.Pinterp_core.env -> Why3.Term.term -> Why3.Term.term) ->
    unit -> Pinterp.ctx
  val get_env : Pinterp.ctx -> Why3.Pinterp_core.env
  val get_do_rac : Pinterp.ctx -> bool
  val get_rac : Pinterp.ctx -> Why3.Pinterp_core.rac
  val get_giant_steps : Pinterp.ctx -> bool
  type result =
      Normal of Why3.Pinterp_core.Value.value
    | Excep of Why3.Ity.xsymbol * Why3.Pinterp_core.Value.value
    | Irred of Why3.Expr.expr
  val print_logic_result : Pinterp.result Why3.Pp.pp
  val exec_rs :
    Pinterp.ctx -> Why3.Expr.rsymbol -> Pinterp.result * Pinterp.ctx
  val exec_global_fundef :
    Pinterp.ctx ->
    (Why3.Expr.rsymbol * Why3.Expr.cexp) list ->
    Why3.Expr.rec_defn list option ->
    Why3.Expr.expr ->
    Pinterp.result * Why3.Pinterp_core.Value.value Why3.Term.Mvs.t *
    Why3.Pinterp_core.Value.value Stdlib.Lazy.t Why3.Expr.Mrs.t
  val report_eval_result :
    Why3.Expr.expr ->
    Stdlib.Format.formatter ->
    Pinterp.result * Why3.Pinterp_core.Value.value Why3.Term.Mvs.t *
    Why3.Pinterp_core.Value.value Stdlib.Lazy.t Why3.Expr.Mrs.t -> unit
  val report_cntr : (Why3.Pinterp_core.cntr_ctx * Why3.Term.term) Why3.Pp.pp
  val debug_disable_builtin_mach : Why3.Debug.flag
  val debug_rac_values : Why3.Debug.flag
end