Z3 translation support for zero-bit values

The Z3 APIs do not permit zero bits in a bitvector, but we want to support use cases where zero-bit values show up (e.g. a concat with empty operands).

We probably want a unified abstract for the Z3 values that know how to work with "faked" zero bit values that are actually placed into Z3 as single bit values. For now, just disabling the (one) affected test -- this primarily showed up with single-arm match statements, where:

* there are no selectors so they...
* `one_hot` turns them into a simple one bit and...
* the `one_hot_sel` just has a default value

It's more regular for the frontend to always emit this pattern than special case the "one arm" case, so ideally we could leave it, and empty concat operands could be supported, vs outlawing them.