let pp p fmt (op, al) =
    match op, al with
      | Const(b), [] -> 
          Format.fprintf fmt "0b%s" (Bitv.to_string b)
      | Conc(n, m), [a; b] -> 
          (match !Pretty.flag with
             | Pretty.Mode.Mixfix ->  
                 Pretty.infix p "++" p fmt (a, b)
             | _ ->
                 let op = Format.sprintf "conc[%d,%d]" n m in
                   Pretty.apply p fmt (op, [a; b]))
      | Sub(n, i, j), [a] -> 
          (match !Pretty.flag with
             | Pretty.Mode.Mixfix ->  
                 let op = Format.sprintf "[%d:%d]" i j in
                   p fmt a; Pretty.string fmt op
             | _ ->
                   let op = Format.sprintf "sub[%d,%d,%d]" n i j in
                   Pretty.apply p fmt (op, [a]))
      | _ ->
          invalid_arg "Ill-formed application in bitvector theory"