sig
  exception Not_in_LIA
  val to_presburger : Var.t list -> Term.t -> Poly.cformula
  val term_of_poly : Poly.poly -> Term.t
  val term_of_cformula : Poly.cformula -> Term.t list
end