pepecoin.py

from manticore import ManticoreEVM
from manticore.core.smtlib import Operators
m = ManticoreEVM()	# initiate the blockchain
ETHER = 1**18
# Create accounts and the target contract
user = m.create_account(balance=1*ETHER, name='owner')
attacker = m.create_account(balance=1*ETHER, name='attacker')
contract = m.solidity_create_contract('pepecoin.sol', owner=user)

# Prepare symbolic input
wei = m.make_symbolic_value(name='wei')
token = m.make_symbolic_value(name='token')

# The attacker try to buy some tokens
contract.buy(token, value=wei, caller=attacker)

# Property - check if the attacker got free money
prop = Operators.UGT(token, wei*10)
for state in m.ready_states:
    if state.can_be_true(prop):
        state.constrain(prop)
        wei_sol, token_sol = state.solve_one_n(wei, token)
        print(f'Bug found, free money!')
        print(f'Call buy({token_sol}) and send {wei_sol} ethers')

https://gist.github.com/feliam/712a3089af6fb784b299553b6dd60bef