module type VCgen = sig .. end
sig
end
include Mcfg.S
val register_lemma : LogicUsage.logic_lemma -> unit
LogicUsage.logic_lemma -> unit
val compile_lemma : LogicUsage.logic_lemma -> Wpo.t
LogicUsage.logic_lemma -> Wpo.t
val compile_wp : Wpo.index -> t_prop -> Wpo.t Bag.t
Wpo.index -> t_prop -> Wpo.t Bag.t