By Farkas lemma, infeasibility of $Ax\leq b$ is equivalent to feasibility of $A^Ty = 0, y^Tb < 0, y\geq 0$, or more practically useful $A^Ty=0, y^Tb \leq -1, y\geq 0$.
Unfortunately, this will lead to a bilinear model when you parameterize $b(z)$. It is fairly similar to an application I worked on a decade ago Oops! I cannot do it again:
Testing for recursive feasibility in MPC where we started with bilinear stuff coming from Farkas lemma, and it was possible to trade that bilinearity with a complementarity condition (Sec 4.2) which (at the time) was more efficiently solved.
EDIT: Missed the fact that $z$ is binary. In that case, you can linearize $y^Tb(z)$ using standard big-M methods, and you end up with a MILP.
Here is a small proof-of-concept implementation in the MATLAB Toolbox YALMIP (disclaimer, developed by me). I was too lazy to manually linearize so I used a built-in command to derive the big-M model
% Feasible model
m = 50;n = 5;
A = randn(m,n);
b0 = A*randn(n,1) + 0.99
z = binvar(m,1);
b = b0 - z;
y = sdpvar(m,1);
[linear_b_y,cut]=binmodel(b'*y,[-100 <= y <= 100]);
Model = [A'*y == 0, y >= 0, linear_b_y == -1, cut];
% Check that it is infeasible
x = sdpvar(n,1);