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