For reasons unknown, `hash_map::to_array` seems to send Boogie into an infinite loop.
For reasons unknown,
hash_map::to_arrayseems to send Boogie into an infinite loop.