let rec type_of = function | Const cs -> if is_int_const (fst (MConst.choose cs)) then Smt.Type.type_int else Smt.Type.type_real | Elem (x, Var) -> Smt.Type.type_proc | Elem (x, _) | Access (x, _) -> snd (Smt.Symbol.type_of x) | Arith(t, _) -> type_of t