let equal_width_of a b =
 match Istate.width_of a, Istate.width_of a with
   | Some(n), Some(m) when n = m -> n
   | Some(n), None -> n
   | NoneSome(n) -> n
   | Some _, Some _ ->
       raise (Invalid_argument "Argument mismatch")
   | NoneNone -> 
       raise (Invalid_argument (Term.to_string a ^ " not a bitvector."))