let of_sym = function
  | Sym.Uninterp _ -> u
  | Sym.Arith _ -> la
  | Sym.Pair _ -> p
  | Sym.Bv _ -> bv
  | Sym.Coproduct _ -> cop
  | Sym.Arrays _ -> arr
  | Sym.Pp _ -> pprod
  | Sym.Fun _ -> app
  | Sym.Bvarith _ -> bvarith