sig
  val sp_attr : Why3.Ident.attribute
  val wp_attr : Why3.Ident.attribute
  val kp_attr : Why3.Ident.attribute
  val wb_attr : Why3.Ident.attribute
  val nt_attr : Why3.Ident.attribute
  val set_infer_invs :
    (Why3.Ident.Sattr.t ->
     Why3.Env.env ->
     Why3.Decl.known_map ->
     Why3.Pdecl.known_map ->
     Why3.Expr.expr -> Why3.Ity.cty -> (Why3.Expr.expr * Why3.Term.term) list) ->
    unit
  val warn_missing_diverges : Why3.Loc.warning_id
  val vc :
    Why3.Env.env ->
    Why3.Pdecl.known_map ->
    Why3.Theory.theory_uc -> Why3.Pdecl.pdecl -> Why3.Pdecl.pdecl list
  val expl_pre : Why3.Ident.attribute
  val expl_post : Why3.Ident.attribute
  val expl_xpost : Why3.Ident.attribute
  val expl_assume : Why3.Ident.attribute
  val expl_assert : Why3.Ident.attribute
  val expl_check : Why3.Ident.attribute
  val expl_lemma : Why3.Ident.attribute
  val expl_absurd : Why3.Ident.attribute
  val expl_for_bound : Why3.Ident.attribute
  val expl_off_bound : Why3.Ident.attribute
  val expl_loop_init : Why3.Ident.attribute
  val expl_loop_keep : Why3.Ident.attribute
  val expl_loop_vari : Why3.Ident.attribute
  val expl_variant : Why3.Ident.attribute
  val expl_type_inv : Why3.Ident.attribute
  val expl_divergent : Why3.Ident.attribute
  val print_expl : Why3.Ident.attribute Why3.Pp.pp
end