Open Source Adventures: Episode 11: Bit Vectors support for Crystal Z3

Time to add the last common sort - bit vectors. Z3 has some other sorts, like floating point numbers, so you can prove why Quake inverse square root works, as well as arrays, functions, and so on, but they're really complicated, and very rarely used....