Solmate `wadMul()` bug ~ Halmos

SignedWadMath.t.sol

// Read more about this here: https://twitter.com/0xkarmacoma/status/1691251106561540097

// SPDX-License-Identifier: Unlicense
pragma solidity ^0.8.15;

import "forge-std/Test.sol";

contract SignedWadMathAsm {
    function wadMul(int256 x, int256 y) public pure returns (int256 r) {
        /// @solidity memory-safe-assembly
        assembly {
            // Store x * y in r for now.
            r := mul(x, y)

            // Equivalent to require(x == 0 || (x * y) / x == y)
            if iszero(or(iszero(x), eq(sdiv(r, x), y))) {
                revert(0, 0)
            }

            // Scale the result down by 1e18.
            r := sdiv(r, 1000000000000000000)
        }
    }
}

contract SignedWadMathSol {
    function wadMul(int256 x, int256 y) public pure returns (int256 r) {
        return (x * y) / 1e18;
    }
}

contract SignedWadMathTest is Test {
    /// sut: system-under-test
    SignedWadMathAsm sutAsm;
    SignedWadMathSol sutSol;

    function setUp() public {
        sutAsm = new SignedWadMathAsm();
        sutSol = new SignedWadMathSol();
    }

    function check_wadMul(int256 x, int256 y) public {
    
        (bool res1, bytes memory data1) = address(sutAsm).call(
            abi.encodeWithSelector(0xca0d24bf, x, y)
        );

        (bool res2, bytes memory data2) = address(sutSol).call(
            abi.encodeWithSelector(0xca0d24bf, x, y)
        );

        assertEq(res1, res2);

        if (res1 && res2) {
            int256 result1 = abi.decode(data1, (int256));
            int256 result2 = abi.decode(data2, (int256));

            assertEq(result1, result2);
        }
    }
}