Getting Throwing Path

Table of contents:


We will now improve the previous example and generate specific inputs for the paths raising an exception in f(). The target is still the following smart contract (example.sol):

pragma solidity >=0.4.24 <0.6.0;

contract Simple {
    function f(uint256 a) public payable {
        if (a == 65) {

Using state information

Each path executed has its state of the blockchain. A state is either ready or it is killed, meaning that it reaches a THROW or REVERT instruction:

  • m.ready_states: the list of states that are ready (they did not execute a REVERT/INVALID)
  • m.killed_states: the list of states that are ready (they did not execute a REVERT/INVALID)
  • m.all_states: all the states
for state in m.all_states:
    # do something with state

You can access state information. For example:

  • state.platform.get_balance(account.address): the balance of the account
  • state.platform.transactions: the list of transactions
  • state.platform.transactions[-1].return_data: the data returned by the last transaction

The data returned by the last transaction is an array, which can be converted to a value with ABI.deserialize, for example:

data = state.platform.transactions[0].return_data
data = ABI.deserialize("uint256", data)

How to generate testcase

Use m.generate_testcase(state, name) to generate testcase:

m.generate_testcase(state, 'BugFound')


  • You can iterate over the state with m.all_states
  • state.platform.get_balance(account.address) returns the account’s balance
  • state.platform.transactions returns the list of transactions
  • transaction.return_data is the data returned
  • m.generate_testcase(state, name) generate inputs for the state

Summary: Getting Throwing Path

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

with open('example.sol') as f:
    source_code =

user_account = m.create_account(balance=1*10**18)
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()

## Check if an execution ends with a REVERT or INVALID
for state in m.terminated_states:
    last_tx = state.platform.transactions[-1]
    if last_tx.result in ['REVERT', 'INVALID']:
        print('Throw found {}'.format(m.workspace))
        m.generate_testcase(state, 'ThrowFound')

All the code above you can find into the

The next step is to add constraints to the state.

Note we could have generated a much simpler script, as all the states returned by terminated_state have REVERT or INVALID in their result: this example was only meant to demonstrate how to manipulate the API.