sig
  type t = {
    axioms : Wp.Definitions.axioms option;
    goal : Wp.Wpo.GOAL.t;
    tags : Wp.Splitter.tag list;
    warn : Wp.Warning.t list;
    deps : Property.Set.t;
    path : Cil_datatype.Stmt.Set.t;
    effect : (Cil_types.stmt * Wp.WpPropId.effect_source) option;
  }
  val resolve : Wp.Wpo.VC_Annot.t -> bool
  val is_trivial : Wp.Wpo.VC_Annot.t -> bool
  val cache_descr :
    pid:Wp.WpPropId.prop_id ->
    Wp.Wpo.VC_Annot.t -> (Wp.VCS.prover * Wp.VCS.result) list -> string
end