bug: `symbolic` results in false positives about hevm HOT 2 CLOSED

// SPDX-License-Identifier: MIT
pragma solidity 0.8.15;

import {Test} from "forge-std/Test.sol";

interface IToken {
    function mint(address, uint256) external;
    function transfer(address, uint256) external;
    function balanceOf(address) external view returns (uint256);
}

/// @author philogy <https://github.com/philogy>
contract METH_WETHVerification is Test {
    function testMain(address _addr1, address _addr2, uint256 _amount1, uint256 _amount2) public {
        require(_amount1 >= _amount2);
        IToken token;
        bytes memory tokenCode =
            hex"606b8060093d393df3583560e01c8063a9059cbb1461002a57806370a0823114610047576340c10f19146100515760006000fd5b335460243581811161005e57600435805482909303335591019055005b600435545952593df35b6004358054602435019055005b63f4d678b83d526004601cfd";
        assembly {
            token := create(0, add(tokenCode, 0x20), mload(tokenCode))
        }
        emit log_named_address("this: ", address(this));

        // -- prepare storage prestate --
        vm.store(address(token), bytes32(uint(0x0)), 0xc41f9400030ace5d0babe3b93bd6041fbbd4060900ffe7ff1b78d6f4fdd74149);
        vm.store(address(token), bytes32(uint(0x4000000000)), 0xb20293c000018103400000000000000000000000000000000000000000000004);

        token.mint(_addr1, _amount1);
        vm.prank(_addr1);
        token.transfer(_addr2, _amount2);
        uint256 bal1 = token.balanceOf(_addr1);
        uint256 bal2 = token.balanceOf(_addr2);
        _assertNoOverflow(bal1, bal2);
        assert(bal1 + bal2 == _amount1);
    }

    function _assertNoOverflow(uint256 x, uint256 y) internal {
        assert(type(uint256).max - x >= y);
    }

    // -- verify that the hevm generated cex is valid
    function testCex() public {
        (bool res, bytes memory data) = address(this).call(hex"7e6f0d300000000000000000000000000000000000000000000000000000004000000000000000000000000000000000000000000000000000000000000000000000000098984142001000b000042886cd1cfbe04523f9ffff02000200072c1f4308caec1aa0dbbe90200000000000000000000000000000000000000000000000000000");
        assertFalse(res);
        assertEq0(abi.encodeWithSignature("Panic(uint256)", 0x1), data);
    }
}