SMT.Array
include SMT_sig.EQUALITY with type t := t
val mk_eq : t list -> t
val mk_distinct : t list -> t
val mk_var : string -> Sort.t -> t
val mk_fresh_var : string -> Sort.t -> t
val mk_sort : Sort.t -> Sort.t -> Sort.t
val mk_const : t -> Sort.t -> t
val mk_select : t -> t -> t
val mk_nary_select : int -> t -> t -> t
val mk_store : t -> t -> t -> t