Parsing of bitvectors constant in counterexamplese
Counterexamples bitvectors from Z3 are ill-printed (example bv32.mlw):
let dummy_update (ref r : bv32)
(* r = #x00000022 *)
requires { r = (0x22:bv32) }
ensures { r = (0x42:bv32) } =
(* r = #x00000084 *)
r <- (0x42:bv32);
(* r = #x00000042 *)
r <- add r r
(* r = #x00000084 *)