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 is_trivial : Wp.Wpo.VC_Annot.t -> bool
val resolve : pid:Wp.WpPropId.prop_id -> 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