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