let rec type_of_smtlib_sexpr = function | HStringSExpr.Atom s when s == s_int -> Type.t_int | HStringSExpr.Atom s when s == s_real -> Type.t_real | HStringSExpr.Atom s when s == s_bool -> Type.t_bool | HStringSExpr.List [HStringSExpr.Atom s; si; se] when s == s_array () -> let ti, te = type_of_smtlib_sexpr si, type_of_smtlib_sexpr se in Type.mk_array te ti | HStringSExpr.Atom _ | HStringSExpr.List _ as s -> raise (Invalid_argument (Format.asprintf "Sort %a not supported" HStringSExpr.pp_print_sexpr s))