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