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