havoc: potentially missing havoc for unresolved call

[intrigus-lgtm]

Maybe this is intentional, but I could readily find information about it.

An unresolved regular call havocs the balance map and then incorrectly pins the callee's own balance to its pre-call value, excluding fallbacks that spend or forward funds.

So something like

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.28;

contract Repro {
    function ping(address dst) external {
        (bool ok,) = dst.call("");
        require(ok);
    }
}

rule unresolvedCalleeCannotSpend(address dst) {
    env e;
    require dst != currentContract;
    uint256 before = nativeBalances[dst];
    ping(e, dst);
    // False in reality: dst's fallback can transfer its existing balance away.
    assert nativeBalances[dst] == before;
}

can be verified (not violated) while dst's fallback could transfer its balance.

Reproduce

Unpack repro.tar.gz

certoraRun.py Repro.conf

Actual: Rule is verified.
Expected: Rule should probably be violated?

Version

Self-built 07.07.26 Release