sig
  module rec Value :
    sig
      type float_mode = Why3deps.Mlmpfr_wrapper.mpfr_rnd_t
      type big_float = Why3deps.Mlmpfr_wrapper.mpfr_float
      type value = private {
        v_desc : Pinterp_core.Value.value_desc;
        v_ty : Why3.Ty.ty;
      }
      and field
      and value_desc =
          Vconstr of Why3.Expr.rsymbol option * Why3.Expr.rsymbol list *
            Pinterp_core.Value.field list
        | Vnum of Why3.BigInt.t
        | Vreal of Why3.Big_real.real
        | Vfloat_mode of Pinterp_core.Value.float_mode
        | Vfloat of Pinterp_core.Value.big_float
        | Vstring of string
        | Vbool of bool
        | Vproj of Why3.Term.lsymbol * Pinterp_core.Value.value
        | Varray of Pinterp_core.Value.value array
        | Vpurefun of Why3.Ty.ty *
            Pinterp_core.Value.value Pinterp_core.Mv.t *
            Pinterp_core.Value.value
        | Vfun of Pinterp_core.Value.value Why3.Term.Mvs.t *
            Why3.Term.vsymbol * Why3.Expr.expr
        | Vterm of Why3.Term.term
        | Vundefined
    end
  and Mv :
    sig
      type key = Value.value
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val singleton : key -> 'a -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val for_all : (key -> 'a -> bool) -> 'a t -> bool
      val exists : (key -> 'a -> bool) -> 'a t -> bool
      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val set_union : 'a t -> 'a t -> 'a t
      val set_inter : 'a t -> 'b t -> 'a t
      val set_diff : 'a t -> 'b t -> 'a t
      val set_submap : 'a t -> 'b t -> bool
      val set_disjoint : 'a t -> 'b t -> bool
      val set_compare : 'a t -> 'b t -> int
      val set_equal : 'a t -> 'b t -> bool
      val find_def : 'a -> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('a -> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> 'a -> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
      val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val fold2_inter :
        (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> 'c -> 'c) ->
        'a t -> 'b t -> 'c -> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> 'a -> 'a t -> 'a t
      val replace : exn -> key -> 'a -> 'a t -> 'a t
      val keys : 'a t -> key list
      val values : 'a t -> 'a list
      val of_list : (key * 'a) list -> 'a t
      val contains : 'a t -> key -> bool
      val domain : 'a t -> unit t
      val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
      val is_num_elt : int -> 'a t -> bool
      type 'a enumeration
      val val_enum : 'a enumeration -> (key * 'a) option
      val start_enum : 'a t -> 'a enumeration
      val next_enum : 'a enumeration -> 'a enumeration
      val start_ge_enum : key -> 'a t -> 'a enumeration
      val next_ge_enum : key -> 'a enumeration -> 'a enumeration
    end
  val print_value :
    Stdlib.Format.formatter -> Pinterp_core.Value.value -> unit
  val compare_values :
    Pinterp_core.Value.value -> Pinterp_core.Value.value -> int
  val v_ty : Pinterp_core.Value.value -> Why3.Ty.ty
  val v_desc : Pinterp_core.Value.value -> Pinterp_core.Value.value_desc
  val field : Pinterp_core.Value.value -> Pinterp_core.Value.field
  val field_get : Pinterp_core.Value.field -> Pinterp_core.Value.value
  val field_set :
    Pinterp_core.Value.field -> Pinterp_core.Value.value -> unit
  val v_inst :
    Pinterp_core.Value.value ->
    Why3.Ty.ty Why3.Ty.Mtv.t -> Pinterp_core.Value.value
  val bool_value : bool -> Pinterp_core.Value.value
  val int_value : Why3.BigInt.t -> Pinterp_core.Value.value
  val string_value : string -> Pinterp_core.Value.value
  val num_value : Why3.Ity.ity -> Why3.BigInt.t -> Pinterp_core.Value.value
  val float_value :
    Why3.Ity.ity -> Pinterp_core.Value.big_float -> Pinterp_core.Value.value
  val real_value : Why3.Big_real.real -> Pinterp_core.Value.value
  val constr_value :
    Why3.Ity.ity ->
    Why3.Expr.rsymbol option ->
    Why3.Expr.rsymbol list ->
    Pinterp_core.Value.value list -> Pinterp_core.Value.value
  val purefun_value :
    result_ity:Why3.Ity.ity ->
    arg_ity:Why3.Ity.ity ->
    Pinterp_core.Value.value Pinterp_core.Mv.t ->
    Pinterp_core.Value.value -> Pinterp_core.Value.value
  val unit_value : Pinterp_core.Value.value
  val range_value : Why3.Ity.ity -> Why3.BigInt.t -> Pinterp_core.Value.value
  val term_value : Why3.Ity.ity -> Why3.Term.term -> Pinterp_core.Value.value
  val snapshot : Pinterp_core.Value.value -> Pinterp_core.Value.value
  val snapshot_vsenv :
    Pinterp_core.Value.value Why3.Term.Mvs.t ->
    Pinterp_core.Value.value Why3.Term.Mvs.t
  val snapshot_oldies :
    Why3.Ity.pvsymbol Why3.Ity.Mpv.t ->
    Pinterp_core.Value.value Why3.Term.Mvs.t ->
    Pinterp_core.Value.value Why3.Term.Mvs.t
  module Log :
    sig
      type exec_mode = Exec_giant_steps | Exec_normal
      val pp_mode :
        Stdlib.Format.formatter -> Pinterp_core.Log.exec_mode -> unit
      type value_or_invalid = Value of Pinterp_core.Value.value | Invalid
      type log_entry_desc = private
          Val_assumed of (Why3.Ident.ident * Pinterp_core.Value.value)
        | Res_assumed of
            (Why3.Expr.rsymbol option * Pinterp_core.Value.value)
        | Const_init of Why3.Ident.ident
        | Exec_call of
            (Why3.Expr.rsymbol option *
             Pinterp_core.Value.value Why3.Term.Mvs.t *
             Pinterp_core.Log.exec_mode)
        | Exec_pure of (Why3.Term.lsymbol * Pinterp_core.Log.exec_mode)
        | Exec_any of
            (Why3.Expr.rsymbol option *
             Pinterp_core.Value.value Why3.Term.Mvs.t)
        | Iter_loop of Pinterp_core.Log.exec_mode
        | Exec_main of
            (Why3.Expr.rsymbol *
             Pinterp_core.Log.value_or_invalid Why3.Term.Mls.t *
             Pinterp_core.Value.value Why3.Term.Mvs.t *
             Pinterp_core.Log.value_or_invalid Why3.Expr.Mrs.t)
        | Exec_stucked of
            (string * Pinterp_core.Value.value Why3.Ident.Mid.t)
        | Exec_failed of
            (string * Pinterp_core.Log.value_or_invalid Why3.Expr.Mrs.t *
             Pinterp_core.Log.value_or_invalid Why3.Term.Mls.t *
             Pinterp_core.Value.value Why3.Term.Mvs.t *
             Pinterp_core.Value.value Why3.Ident.Mid.t)
        | Exec_ended
      type log_entry = private {
        log_desc : Pinterp_core.Log.log_entry_desc;
        log_loc : Why3.Loc.position option;
      }
      type exec_log = Pinterp_core.Log.log_entry list
      type log_uc
      val log_val :
        Pinterp_core.Log.log_uc ->
        Why3.Ident.ident ->
        Pinterp_core.Value.value -> Why3.Loc.position option -> unit
      val log_const :
        Pinterp_core.Log.log_uc ->
        Why3.Ident.ident -> Why3.Loc.position option -> unit
      val log_call :
        Pinterp_core.Log.log_uc ->
        Why3.Expr.rsymbol option ->
        Pinterp_core.Value.value Why3.Term.Mvs.t ->
        Pinterp_core.Log.exec_mode -> Why3.Loc.position option -> unit
      val log_pure_call :
        Pinterp_core.Log.log_uc ->
        Why3.Term.lsymbol ->
        Pinterp_core.Log.exec_mode -> Why3.Loc.position option -> unit
      val log_any_call :
        Pinterp_core.Log.log_uc ->
        Why3.Expr.rsymbol option ->
        Pinterp_core.Value.value Why3.Term.Mvs.t ->
        Why3.Loc.position option -> unit
      val log_iter_loop :
        Pinterp_core.Log.log_uc ->
        Pinterp_core.Log.exec_mode -> Why3.Loc.position option -> unit
      val log_exec_main :
        Pinterp_core.Log.log_uc ->
        Why3.Expr.rsymbol ->
        Pinterp_core.Value.value Stdlib.Lazy.t Why3.Term.Mls.t ->
        Pinterp_core.Value.value Why3.Term.Mvs.t ->
        Pinterp_core.Value.value Stdlib.Lazy.t Why3.Expr.Mrs.t ->
        Why3.Loc.position option -> unit
      val log_failed :
        Pinterp_core.Log.log_uc ->
        string ->
        Pinterp_core.Value.value Stdlib.Lazy.t Why3.Expr.Mrs.t ->
        Pinterp_core.Value.value Stdlib.Lazy.t Why3.Term.Mls.t ->
        Pinterp_core.Value.value Why3.Term.Mvs.t ->
        Pinterp_core.Value.value Why3.Ident.Mid.t ->
        Why3.Loc.position option -> unit
      val log_stucked :
        Pinterp_core.Log.log_uc ->
        string ->
        Pinterp_core.Value.value Why3.Ident.Mid.t ->
        Why3.Loc.position option -> unit
      val log_exec_ended :
        Pinterp_core.Log.log_uc -> Why3.Loc.position option -> unit
      val empty_log_uc : unit -> Pinterp_core.Log.log_uc
      val empty_log : Pinterp_core.Log.exec_log
      val get_log : Pinterp_core.Log.log_uc -> Pinterp_core.Log.exec_log
      val flush_log : Pinterp_core.Log.log_uc -> Pinterp_core.Log.exec_log
      val sort_log_by_loc :
        Pinterp_core.Log.exec_log ->
        Pinterp_core.Log.log_entry list Why3.Wstdlib.Mint.t
        Why3.Wstdlib.Mstr.t
      val json_log : Pinterp_core.Log.exec_log -> Why3.Json_base.json
      val print_log : ?verb_lvl:int -> Pinterp_core.Log.exec_log Why3.Pp.pp
      val get_exec_calls_and_loops :
        Why3.Env.env ->
        Pinterp_core.Log.exec_log -> Pinterp_core.Log.log_entry list
    end
  type premises
  val with_push_premises : Pinterp_core.premises -> (unit -> 'a) -> 'a
  val add_premises : Why3.Term.term list -> Pinterp_core.premises -> unit
  val fold_premises :
    ('a -> Why3.Term.term -> 'a) -> Pinterp_core.premises -> 'a -> 'a
  type env = {
    why_env : Why3.Env.env;
    pmodule : Why3.Pmodule.pmodule0;
    funenv :
      (Why3.Expr.cexp * Why3.Expr.rec_defn list option) Why3.Expr.Mrs.t;
    tvenv : Why3.Ty.ty Why3.Ty.Mtv.t;
    vsenv : Pinterp_core.Value.value Why3.Term.Mvs.t;
    lsenv : Pinterp_core.Value.value Stdlib.Lazy.t Why3.Term.Mls.t;
    rsenv : Pinterp_core.Value.value Stdlib.Lazy.t Why3.Expr.Mrs.t;
    premises : Pinterp_core.premises;
    log_uc : Pinterp_core.Log.log_uc;
  }
  val mk_empty_env :
    Why3.Env.env -> Why3.Pmodule.pmodule0 -> Pinterp_core.env
  val get_vs :
    Pinterp_core.env -> Why3.Term.Mvs.key -> Pinterp_core.Value.value
  val get_pvs :
    Pinterp_core.env -> Why3.Ity.pvsymbol -> Pinterp_core.Value.value
  val bind_vs :
    Why3.Term.Mvs.key ->
    Pinterp_core.Value.value -> Pinterp_core.env -> Pinterp_core.env
  val bind_ls :
    Why3.Term.Mls.key ->
    Pinterp_core.Value.value Stdlib.Lazy.t ->
    Pinterp_core.env -> Pinterp_core.env
  val bind_rs :
    Why3.Expr.Mrs.key ->
    Pinterp_core.Value.value Stdlib.Lazy.t ->
    Pinterp_core.env -> Pinterp_core.env
  val bind_pvs :
    ?register:(Why3.Ident.ident -> Pinterp_core.Value.value -> unit) ->
    Why3.Ity.pvsymbol ->
    Pinterp_core.Value.value -> Pinterp_core.env -> Pinterp_core.env
  val multibind_pvs :
    ?register:(Why3.Ident.ident -> Pinterp_core.Value.value -> unit) ->
    Why3.Ity.pvsymbol list ->
    Pinterp_core.Value.value list -> Pinterp_core.env -> Pinterp_core.env
  exception Cannot_evaluate of string
  val cannot_evaluate :
    ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a
  val term_of_value :
    ?ty_mt:Why3.Ty.ty Why3.Ty.Mtv.t ->
    Pinterp_core.env ->
    (Why3.Term.vsymbol * Why3.Term.term) list ->
    Pinterp_core.Value.value ->
    (Why3.Term.vsymbol * Why3.Term.term) list * Why3.Term.term
  type compute_term = Pinterp_core.env -> Why3.Term.term -> Why3.Term.term
  val compute_term_dummy : Pinterp_core.compute_term
  val default_value_of_type :
    Pinterp_core.env -> Why3.Ity.ity -> Pinterp_core.Value.value
  type check_value = Why3.Ity.ity -> Pinterp_core.Value.value -> unit
  type oracle = {
    for_variable :
      Pinterp_core.env ->
      ?check:Pinterp_core.check_value ->
      loc:Why3.Loc.position option ->
      Why3.Ident.ident -> Why3.Ity.ity -> Pinterp_core.Value.value option;
    for_result :
      Pinterp_core.env ->
      ?check:Pinterp_core.check_value ->
      loc:Why3.Loc.position ->
      call_id:Why3.Expr.expr_id option ->
      Why3.Ity.ity -> Pinterp_core.Value.value option;
  }
  val oracle_dummy : Pinterp_core.oracle
  val register_used_value :
    Pinterp_core.env ->
    Why3.Loc.position option ->
    Why3.Ident.ident -> Pinterp_core.Value.value -> unit
  val register_res_value :
    Pinterp_core.env ->
    Why3.Loc.position ->
    Why3.Expr.rsymbol option -> Pinterp_core.Value.value -> unit
  val register_const_init :
    Pinterp_core.env -> Why3.Loc.position option -> Why3.Ident.ident -> unit
  val register_call :
    Pinterp_core.env ->
    Why3.Loc.position option ->
    Why3.Expr.rsymbol option ->
    Pinterp_core.Value.value Why3.Term.Mvs.t ->
    Pinterp_core.Log.exec_mode -> unit
  val register_pure_call :
    Pinterp_core.env ->
    Why3.Loc.position option ->
    Why3.Term.lsymbol -> Pinterp_core.Log.exec_mode -> unit
  val register_any_call :
    Pinterp_core.env ->
    Why3.Loc.position option ->
    Why3.Expr.rsymbol option ->
    Pinterp_core.Value.value Why3.Term.Mvs.t -> unit
  val register_iter_loop :
    Pinterp_core.env ->
    Why3.Loc.position option -> Pinterp_core.Log.exec_mode -> unit
  val register_exec_main : Pinterp_core.env -> Why3.Expr.rsymbol -> unit
  val register_failure :
    Pinterp_core.env ->
    Why3.Loc.position option ->
    string -> Pinterp_core.Value.value Why3.Ident.Mid.t -> unit
  val register_stucked :
    Pinterp_core.env ->
    Why3.Loc.position option ->
    string -> Pinterp_core.Value.value Why3.Ident.Mid.t -> unit
  val register_ended : Pinterp_core.env -> Why3.Loc.position option -> unit
  type cntr_ctx = {
    attr : Why3.Ident.attribute;
    desc : string option;
    loc : Why3.Loc.position option;
    attrs : Why3.Ident.Sattr.t;
    cntr_env : Pinterp_core.env;
    giant_steps : bool option;
  }
  val mk_cntr_ctx :
    Pinterp_core.env ->
    giant_steps:bool option ->
    ?loc:Why3.Loc.position ->
    ?attrs:Why3.Ident.Sattr.t ->
    ?desc:string -> Why3.Ident.attribute -> Pinterp_core.cntr_ctx
  val describe_cntr_ctx : Pinterp_core.cntr_ctx -> string
  val report_cntr_title : (Pinterp_core.cntr_ctx * string) Why3.Pp.pp
  val report_cntr_head :
    (Pinterp_core.cntr_ctx * string * Why3.Term.term) Why3.Pp.pp
  val report_cntr_body : (Pinterp_core.cntr_ctx * Why3.Term.term) Why3.Pp.pp
  val report_cntr :
    (Pinterp_core.cntr_ctx * string * Why3.Term.term) Why3.Pp.pp
  exception Fail of Pinterp_core.cntr_ctx * Why3.Term.term
  exception Stuck of Pinterp_core.cntr_ctx * Why3.Loc.position option *
              string
  exception Cannot_decide of Pinterp_core.cntr_ctx * Why3.Term.term list *
              string
  exception FatalRACError of Pinterp_core.Log.log_uc * string
  val fatal_rac_error :
    Pinterp_core.Log.log_uc ->
    ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a
  val stuck :
    ?loc:Why3.Loc.position ->
    Pinterp_core.cntr_ctx ->
    ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a
  val stuck_for_fail :
    ?loc:Why3.Loc.position -> Pinterp_core.cntr_ctx -> Why3.Term.term -> 'a
  type check_term =
      ?vsenv:(Why3.Term.vsymbol * Why3.Term.term) list ->
      Pinterp_core.cntr_ctx -> Why3.Term.term -> unit
  val check_term_dummy : Pinterp_core.check_term
  type rac = {
    check_term : Pinterp_core.check_term;
    ignore_incomplete : bool;
  }
  val mk_rac :
    ?ignore_incomplete:bool -> Pinterp_core.check_term -> Pinterp_core.rac
  val rac_dummy : Pinterp_core.rac
  val check_term :
    Pinterp_core.rac ->
    ?vsenv:(Why3.Term.vsymbol * Why3.Term.term) list ->
    Pinterp_core.cntr_ctx -> Why3.Term.term -> unit
  val check_assume_term :
    Pinterp_core.rac -> Pinterp_core.cntr_ctx -> Why3.Term.term -> unit
  val check_terms :
    Pinterp_core.rac -> Pinterp_core.cntr_ctx -> Why3.Term.term list -> unit
  val check_assume_terms :
    Pinterp_core.rac -> Pinterp_core.cntr_ctx -> Why3.Term.term list -> unit
  val check_post :
    Pinterp_core.rac ->
    Pinterp_core.cntr_ctx ->
    Pinterp_core.Value.value -> Why3.Ity.post -> unit
  val check_posts :
    Pinterp_core.rac ->
    Pinterp_core.cntr_ctx ->
    Pinterp_core.Value.value -> Why3.Ity.post list -> unit
  val check_assume_posts :
    Pinterp_core.rac ->
    Pinterp_core.cntr_ctx ->
    Pinterp_core.Value.value -> Why3.Ity.post list -> unit
  val check_type_invs :
    Pinterp_core.rac ->
    ?loc:Why3.Loc.position ->
    giant_steps:bool ->
    Pinterp_core.env -> Why3.Ity.ity -> Pinterp_core.Value.value -> unit
  val check_assume_type_invs :
    Pinterp_core.rac ->
    ?loc:Why3.Loc.position ->
    giant_steps:bool ->
    Pinterp_core.env -> Why3.Ity.ity -> Pinterp_core.Value.value -> unit
  val oldify_varl :
    Pinterp_core.env ->
    (Why3.Term.term * Why3.Term.lsymbol option) list ->
    (Why3.Term.term * Why3.Term.lsymbol option) list *
    Pinterp_core.Value.value Why3.Term.Mvs.t
  val check_variant :
    Pinterp_core.rac ->
    Why3.Ident.Sattr.elt ->
    Why3.Loc.position option ->
    giant_steps:bool ->
    Pinterp_core.env ->
    (Why3.Term.term * Why3.Term.lsymbol option) list *
    Pinterp_core.Value.value Why3.Term.Mvs.t ->
    (Why3.Term.term * Why3.Term.lsymbol option) list -> unit
  val t_undefined : string -> Why3.Ty.ty -> Why3.Term.term
  val ty_app_arg : Why3.Ty.tysymbol -> int -> Why3.Ty.ty -> Why3.Ty.ty
  val ity_components :
    Why3.Ity.ity ->
    Why3.Ity.itysymbol * Why3.Ity.ity list * Why3.Ity.ity list
  val is_range_ty : Why3.Ty.ty -> bool
  val debug_array_as_update_chains_not_epsilon : Why3.Debug.flag
  val undefined_value :
    Pinterp_core.env -> Why3.Ity.ity -> Pinterp_core.Value.value
  val debug_trace_exec : Why3.Debug.flag
  val pp_bindings :
    ?sep:unit Why3.Pp.pp ->
    ?pair_sep:unit Why3.Pp.pp ->
    ?delims:unit Why3.Pp.pp * unit Why3.Pp.pp ->
    'a Why3.Pp.pp -> 'b Why3.Pp.pp -> ('a * 'b) list Why3.Pp.pp
  val pp_env :
    'a Why3.Pp.pp ->
    'b Why3.Pp.pp -> Stdlib.Format.formatter -> ('a * 'b) list -> unit
  val value :
    Why3.Ty.ty -> Pinterp_core.Value.value_desc -> Pinterp_core.Value.value
end