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);
}
}