<p>every time i have to interact with SMT solvers it leaves me incandescently angry in a way little other tooling does. would it fucking kill you to allow zero length bitvectors? did you take inspiration from verilog??</p>