External call encountered an issue at DELEGATECALL about halmos

[banicg]

Thanks, it is working perfectly now!

[daejunpark]

Thanks for the repro!

This is a known limitation. Please refer to this wiki page:
https://github.com/a16z/halmos/wiki/errors#symbolic-calldataload-offset

In your case, the arguments for UUPSUpgradeable.upgradeToAndCall(address,bytes) need to be explicitly constructed as described on the wiki page. For example,

    function prove4_NoBackdoor(bytes4 selector, address caller) public {
        bytes memory args;
        if (selector == UUPSUpgradeable.upgradeToAndCall.selector) {
            args = abi.encode(svm.createAddress("newImplementation"), svm.createBytes(1024, "data"));
        } else {
            args = svm.createBytes(1024, "args");
        }
        _checkNoBackdoor(selector, args, caller);
    }

Please let me know if you have any further questions!

[karmacoma-eth]

The error message has been documented here for future reference: https://github.com/a16z/halmos/wiki/errors#symbolic-calldataload-offset