Implement BVZX case in Simplifier (so that using BVZX will not fail with an exception).
Add BVZX to CVC parser and refactor SMT1/2 parsers to use BVZX.