This comes from a fundamental misunderstanding of what UB is.

Think of this piece of code - `y * x / y`.

Would you like to simplify it to just `x` ?

You need to either lean on UB to do so or have some magical way to prove that y can not be 0.

Otherwise this transformation changes behavior, and is illegal.