Example: Arithmetic overflow

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).

Proposed scenario

We use the pattern initialization, exploration and property for our scripts.

Initialization

• Create one user account
• Create the contract account

Exploration

• Call balances on the user account
• Call transfer with symbolic destination and value
• Call balances on the user account

Property

• Check if the user can have more token after the transfer than before.