Module type CfgWP.VCgen

module type VCgen = sig .. end

include Mcfg.S
val register_lemma : LogicUsage.logic_lemma -> unit
val compile_lemma : LogicUsage.logic_lemma -> Wpo.t
val compile_wp : Wpo.index -> t_prop -> Wpo.t Bag.t