object method add_lemma : LogicUsage.logic_lemma -> unit method add_strategy : WpStrategy.strategy -> unit method compute : Wpo.t Bag.t method lemma : bool method model : WpContext.model end