This scenario is given as an example. You can follow its structure to solve the exercises.
my_token.py
uses Manticore to find for an attacker to generate tokens during a transfer on Token (my_token.sol).
We use the pattern initialization, exploration and property for our scripts.
- Create one user account
- Create the contract account
- Call balances on the user account
- Call transfer with symbolic destination and value
- Call balances on the user account
- Check if the user can have more token after the transfer than before.