let dom s a =
  let rec of_term = function
    | App(Arith(op), xl) -> of_arith op xl
    | App(Pp(op), xl) -> of_pprod op xl
    | App(Bvarith(op), xl) -> of_bvarith op xl
    | a -> 
        if is_intvar a then Dom.Int 
        else if is_realvar a then Dom.Real 
        else of_term (apply Th.la s a)
  and of_arith op xl =
    try
      match op, xl with
        | Num(q), [] ->
            if Q.is_integer q then Dom.Int else Dom.Real
        | Multq(q), [x] -> 
            if Q.is_integer q && of_term x = Dom.Int 
            then Dom.Int 
            else Dom.Real
        | Add, xl -> 
            if List.for_all (fun x -> Dom.eq (of_term x) Dom.Int) xl 
            then Dom.Int 
            else Dom.Real
        | _ -> 
            Dom.Real
      with
          Not_found -> Dom.Real
  and of_pprod op xl = 
    try
      match op, xl with
        | Mult, _ -> 
            if List.for_all (fun x -> Dom.eq (of_term x) Dom.Int) xl 
            then Dom.Int 
            else Dom.Real
        | Expt(n), [x] ->
            if n >= 0 && of_term x = Dom.Int 
            then Dom.Int 
            else Dom.Real
        | _ ->
            Dom.Real
      with
          Not_found -> Dom.Real
  and of_bvarith op xl =
    match op, xl with
      | Unsigned, [_] -> Dom.Int
      | _ -> Dom.Real
  in
    of_term a