let solve th e =
  match th with
    | Th.Shostak(i) ->
        (match i with
           | Th.LA -> Arith.solve e
           | Th.BV -> Bitvector.solve e
           | Th.P -> Product.solve e
           | Th.COP -> Coproduct.solve e
           | Th.APP -> Apply.solve e
           | Th.SET -> Propset.solve e)
    | _ ->
        raise Exc.Incomplete