Bit Blasting Algorithm
I assume the formula is

$$(x \ne 0) \land (y|2 = z) \land (1&lt;3).$$

We can handle each clause of the conjunction separately.  If $x=(b_3,b_4)$, then $x \ne 0$ translates to

$$b_3 \lor b_4.$$

If $y=(b_5,b_6)$ and $z=(b_7,b_8)$, then $y|2$ translates to $(b_5|1,b_6)$, which simplifies to $(1,b_6)$ (if you are doing simplification).  Now $(1,b_6) = (b_7,b_8)$ translates to

$$(b_7=1) \land (b_6 = b_8),$$

which in CNF form is

$$b_7 \land (b_6 \lor \neg b_8) \land (\neg b_6 \lor b_8).$$

Finally, $1&lt;3$ translates to True, if you are doing simplification.  So, the final result is the conjunction of those:

$$(b_3 \lor b_4) \land (b_7) \land (b_6 \lor \neg b_8) \land (\neg b_6 \lor b_8).$$