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.


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