let rec occurs a b =
  let rec loop x =
    (Term.eq x a)
    || (match d_interp x with
          | Some(op,l) ->
              (match op, l with
                 | Sym.Const(_), [] -> false
                 | Sym.Sub _, [x] -> loop x
                 | Sym.Conc(n,m), [x;y] -> (loop x) || (loop y)
                 | Sym.Bitwise(n), [x;y;z] -> (loop x) || (loop y) || (loop z)
                 | _ ->  failwith "Bv.map: ill-formed expression")
          | None -> false)
  in
  loop b