I don't see anything wrong in Z3 behavior. Why do you think the formula should be satisfiable?
A = (w*x*y+31) & ~31 -- imply that the 5 rightmost bits will be always zero
B = UDiv( A & ~31, 8 ) (equal to a logical shift right by 3) -- imply that the 2 rightmost bits will be always zero.
C = B * z -- this will always have the 2 rightmost bits zero
c == 0xffffffff -- that's impossible
If you change the constant to 0xfffffffc, then you'll get a solution.