let d_bvsym = function
  | Bv(op) -> Some(op)
  | _ -> None