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 : Model.t end