You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This is again the problem with BMC not tracking the state of the contract.
Since it is doing only a local check, it does not know that the state variable amount is always 0 and cannot change.
So this is not a bug, but false positive due to BMC's over-approximating modeling.
The problem is that CHC currently does not attempts to verify the verification target Insufficient funds for transfer.
But maybe it should.
Description
When the transfer amount is 0, SMTChecker incorrectly determines insufficient balance
Environment
Steps to Reproduce
The text was updated successfully, but these errors were encountered: