Docker image of Manticore from Docker Hub fails to run `examples/evm/umd_example.sol` example

[lahiri-phdworks]

Summary of the problem

Docker image of Manticore from Docker Hub fails to run examples/evm/umd_example.sol example. The example fails with the following error.

m.c.worker:ERROR: Exception in state 1: ManticoreError('Forking on unfeasible constraint set')

Full Error

2022-01-07 08:52:26,570: [17] m.c.worker:ERROR: Exception in state 1: ManticoreError('Forking on unfeasible constraint set')
Traceback (most recent call last):
  File "/usr/local/lib/python3.7/dist-packages/manticore/core/worker.py", line 137, in run
    current_state.execute()
  File "/usr/local/lib/python3.7/dist-packages/manticore/ethereum/state.py", line 8, in execute
    return self._platform.execute()
  File "/usr/local/lib/python3.7/dist-packages/manticore/platforms/evm.py", line 3106, in execute
    self.current_vm.execute()
  File "/usr/local/lib/python3.7/dist-packages/manticore/platforms/evm.py", line 1322, in execute
    raise Concretize("Symbolic PC", expression=expression, setstate=setstate, policy="ALL")
manticore.core.state.Concretize

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/usr/local/lib/python3.7/dist-packages/manticore/core/worker.py", line 158, in run
    m._fork(current_state, exc.expression, exc.policy, exc.setstate, exc.values)
  File "/usr/local/lib/python3.7/dist-packages/manticore/core/manticore.py", line 518, in _fork
    raise ManticoreError("Forking on unfeasible constraint set")
manticore.exceptions.ManticoreError: Forking on unfeasible constraint set

Manticore version

Python version

OS / Environment

Dependencies

Step to reproduce the behavior

Pulled the docker image and ran it with the following commands,

docker run --name test --ulimit stack=10000000:10000000 -it trailofbits/manticore
manticore manticore/examples/evm/umd_example.sol

Expected behavior

Actual behavior

manticore → λ git master* → docker run --name evm --ulimit stack=10000000:10000000 -it trailofbits/manticore  
root@79678e02a3f8:/# 
root@79678e02a3f8:/# cd manticore/
root@79678e02a3f8:/manticore# manticore examples/evm/umd_example.sol 
2022-01-07 08:52:25,626: [17] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
2022-01-07 08:52:25,626: [17] m.main:INFO: Beginning analysis
2022-01-07 08:52:25,628: [17] m.e.manticore:INFO: Starting symbolic create contract
2022-01-07 08:52:25,994: [17] m.e.manticore:INFO: Starting symbolic transaction: 0
2022-01-07 08:52:26,570: [17] m.c.worker:ERROR: Exception in state 1: ManticoreError('Forking on unfeasible constraint set')
Traceback (most recent call last):
  File "/usr/local/lib/python3.7/dist-packages/manticore/core/worker.py", line 137, in run
    current_state.execute()
  File "/usr/local/lib/python3.7/dist-packages/manticore/ethereum/state.py", line 8, in execute
    return self._platform.execute()
  File "/usr/local/lib/python3.7/dist-packages/manticore/platforms/evm.py", line 3106, in execute
    self.current_vm.execute()
  File "/usr/local/lib/python3.7/dist-packages/manticore/platforms/evm.py", line 1322, in execute
    raise Concretize("Symbolic PC", expression=expression, setstate=setstate, policy="ALL")
manticore.core.state.Concretize

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/usr/local/lib/python3.7/dist-packages/manticore/core/worker.py", line 158, in run
    m._fork(current_state, exc.expression, exc.policy, exc.setstate, exc.values)
  File "/usr/local/lib/python3.7/dist-packages/manticore/core/manticore.py", line 518, in _fork
    raise ManticoreError("Forking on unfeasible constraint set")
manticore.exceptions.ManticoreError: Forking on unfeasible constraint set
 
2022-01-07 08:52:26,576: [17] m.e.manticore:INFO: 0 alive states, 1 terminated states
2022-01-07 08:52:26,675: [17] m.c.manticore:INFO: Results in /manticore/mcore_ijmw898c
2022-01-07 08:52:26,675: [17] m.c.manticore:INFO: Total time: 0.6769917011260986

Any relevant logs

[lahiri-phdworks]

I noticed that the example examples/evm/umd_example.sol runs fine, if the view modifier from function in the smart contract is removed.