let theory_of (sym, _) =
  match sym with
    | Uninterp _ -> Th.u
    | Arith _ -> Th.la
    | Product _ -> Th.p
    | Bv _ -> Th.bv
    | Coproduct _ -> Th.cop
    | Arrays _ -> Th.arr
    | Pp _ -> Th.nl
    | Cl _ -> Th.app
    | Propset _ -> Th.set