# if $x = 0$ then $y \ne b$

I'm trying to model the following:

if $$x=0$$ then $$y \ne b$$

$$y$$ is a positive integer number( $$y\le U$$) and $$x$$ is binary and $$b$$ is a constant.

Introduce binary variables $$z_1$$, $$z_2$$, and $$z_3$$, and impose linear constraints \begin{align} z_1+z_2 +z_3&= 1 \tag1\\ 1z_1+bz_2+(b+1)z_3 \le y &\le (b-1)z_1+bz_2+Uz_3 \tag2\\ z_2&\le x\tag3 \end{align} Constraints $$(1)$$ and $$(2)$$ enforce the three disjoint cases $$y, $$y=b$$, and $$y>b$$. Constraint $$(3)$$ enforces $$x=0\implies z_2=0$$, and $$z_2=0$$ excludes the $$y=b$$ case.