SMT Checker : Unexpected " BMC: Insufficient funds happens here"

Question

I was using the SMT Solidity Model Checker, and I Don't understand why I have a :" BMC: Insufficient funds happens here". My code is quite simple, I just wanted to check if the Model Checker analyses well reentrancy. Does anyone know if the checker model actually has a problem, or is it the code that is vulnerable? Thanks in advance for your answers

pragma solidity >=0.8.0;

contract Reentrancy {

uint public balance;
    
function withdraw(uint amount) public payable {
    require (balance > amount);
    balance -= amount;
    payable(msg.sender).transfer(amount);
}

}

Answer 1

When the contract makes a transfer it does not use your state variable balance, but rather the balance of the contract as in address(this).balance. Since that balance is not being checked, transfer(amount) may revert because address(this).balance < amount is possible. The code below applies the proper check and the warning message is gone:

pragma solidity >=0.8.0;

contract Reentrancy {
    function withdraw(uint amount) public payable {
        require (address(this).balance > amount);
        payable(msg.sender).transfer(amount);
    }

}

Please note that because transfer does not forward a lot of gas, the model checker assumes that reentrancy is not possible in this case. One possible way for you to play with reentrancy in the model checker is, for example:

pragma solidity >=0.8.0;

interface D { function e() external; }

contract C {
    bool locked = true;

    function call(address target) public {
        locked = false;
        D(target).e();
        locked = true;
    }

    function broken() public view {
        assert(locked);
    }
}