Adding Constraints

Table of contents:


We will see how to constrain the exploration. We will make the assumption that the documentation of f() states that the function is never called with a == 65, so any bug with a == 65 is not a real bug. 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) {


The Operators module facilitates the manipulation of constraints, among other it provides:

  • Operators.AND,
  • Operators.OR,
  • Operators.UGT (unsigned greater than),
  • Operators.UGE (unsigned greater than or equal to),
  • Operators.ULT (unsigned lower than),
  • Operators.ULE (unsigned lower than or equal to).

To import the module use the following:

from manticore.core.smtlib import Operators

Operators.CONCAT is used to concatenate an array to a value. For example, the return_data of a transaction needs to be changed to a value to be checked against another value:

last_return = Operators.CONCAT(256, *last_return)


You can use constraints globally or for a specific state.

Global constraint

Use m.constrain(constraint) to add a global cosntraint. For example, you can call a contract from a symbolic address, and restraint this address to be specific values:

symbolic_address = m.make_symbolic_value()
m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))

State constraint

Use state.constrain(constraint) to add a constraint to a specific state It can be used to constrain the state after its exploration to check some property on it.

Checking Constraint

Use solver.check(state.constraints) to know if a constraint is still feasible. For example, the following will constraint symbolic_value to be different from 65 and check if the state is still feasible:

state.constrain(symbolic_var != 65)
if solver.check(state.constraints):
    # state is feasible

Summary: Adding Constraints

Adding constraint to the previous code, we obtain:

from manticore.ethereum import ManticoreEVM
from manticore.core.smtlib.solver import Z3Solver

solver = Z3Solver.instance()

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

no_bug_found = True

## 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']:
        # we do not consider the path were a == 65
        condition = symbolic_var != 65
        if m.generate_testcase(state, name="BugFound", only_if=condition):
            print(f'Bug found, results are in {m.workspace}')
            no_bug_found = False

if no_bug_found:
    print(f'No bug found')

All the code above you can find into the

The next step is to follow the exercises.