SMT.Arithmetic
include SMT_sig.EQUALITY with type t := t
val mk_eq : t list -> t
val mk_distinct : t list -> t
val mk_var : string -> t
val mk_fresh_var : string -> t
val mk_const : int -> t
val mk_plus : t list -> t
val mk_minus : t -> t -> t
val mk_mult : t list -> t
val mk_lesser : t -> t -> t
val mk_lesser_eq : t -> t -> t