Undetermined value in Z3?

[Muxucao0812]

For hardware language, such as Verilog, there exist undetermined values x and high resistance z, for the x, it can represent 0 or 1, for example, 3'bx1x can be 3'b110, 3'b111, 3'b011, 3'b010. I want to know if there are some expressions like this in Z3Prover. Thanks

[NikolajBjorner]

there is not.
You can encode these using two bit-vectors or one bit-vector of double size.
The typical approach is to use two bit-vectors. Then define:
1 = 11
0 = 01
x = 00
z = 10

or similar.