let pp_i i fmt s =
    match i with
      | Th.Uninterpreted ->  U.S.pp fmt s.u
      | Th.Shostak(i) -> 
          (match i with
             | Th.LA -> 
                 La.pp La.R fmt s.la; 
                 Format.fprintf fmt "\n";
                 La.pp La.T fmt s.la
             | Th.BV -> S.pp fmt s.bv
             | Th.P -> S.pp fmt s.p
             | Th.COP -> S.pp fmt s.cop
             | Th.APP -> S.pp fmt s.cl
             | Th.SET -> S.pp fmt s.set)
      | Th.Can(i) ->
          (match i with
             | Th.NL -> S.pp fmt s.nl
             | Th.ARR -> S.pp fmt s.arr)