Summary

MulWadUp returns wrong value if input x and y becomes too large and the assertion in testMulWadUpFuzz will fail as the numbers become large.

Vulnerability Details

Try running the testMulWadUpFuzzwith more runs, it will eventually break.

With the line if iszero(sub(div(add(z, x), y), 1)) { x := add(x, 1) } adding 1 to x if the result of sub(div(add(z, x), y), 1) is not 0.

Adding 1 to x causes a big difference in results if the numbers are sufficiently large

Impact

Protocol dependent on the library will have their math wrong

Tools Used

Foundry

Recommendations

I'm not sure why 1 is added to x in this case, it should make more sense if it is added to z.
The portion add(z, x) in line if iszero(sub(div(add(z, x), y), 1)) { x := add(x, 1) } doesn't make much sense as z is still uninitialized.