sig
  type rg
  val compute : Wp.Conditions.sequence -> Wp.Auto.Range.rg
  val ranges : Wp.Auto.Range.rg -> (int * int) Wp.Lang.F.Tmap.t
  val bounds : Wp.Auto.Range.rg -> (int option * int option) Wp.Lang.F.Tmap.t
end