Assertion failure: assert value.size == self.size when gas is ignored

OS / Environment

Ubuntu 18.04

Manticore version

cc7811b10d9ce4f5c3444ebceff16b3ed2753f21

Python version

Python 3.6

Summary of the problem

Manticode crashes with an assertion failure when gas computation is ignored.

Step to reproduce the behavior

Use this solidity contract:

contract C {
  function hash(string x) public returns (bytes32) {
    return(keccak256(x));
  }
}

with manticore:

$ manticore bug.sol  --txlimit 1 --evm.oog ignore

Expected behavior

It should should not crash. It's unclear how to proceed with the symbolic exploration since manticore will waste resourced exploring the keccak256 code. Maybe a warning saying that such path will not be explored?

Actual behavior

2019-07-22 10:24:54,158: [15617] m.main:INFO: Registered plugins: DetectReentrancyAdvanced, DetectSuicidal, DetectUnusedRetVal, DetectInvalid, DetectUninitializedMemory, DetectIntegerOverflow, DetectEnvInstruction, DetectExternalCallAndLeak, DetectDelegatecall, DetectReentrancySimple, DetectUninitializedStorage
2019-07-22 10:24:54,158: [15617] m.main:INFO: Beginning analysis
2019-07-22 10:24:54,163: [15617] m.e.manticore:INFO: Starting symbolic create contract
2019-07-22 10:24:54,710: [15617] m.e.manticore:INFO: Starting symbolic transaction: 0
2019-07-22 10:25:10,260: [15916] m.c.worker:ERROR: Exception in state 0: AssertionError()
Traceback (most recent call last):
  File "/home/gustavo/.local/lib/python3.6/site-packages/manticore-0.3.0-py3.6.egg/manticore/core/worker.py", line 121, in run
    current_state.execute()
  File "/home/gustavo/.local/lib/python3.6/site-packages/manticore-0.3.0-py3.6.egg/manticore/ethereum/state.py", line 6, in execute
    return self._platform.execute()
  File "/home/gustavo/.local/lib/python3.6/site-packages/manticore-0.3.0-py3.6.egg/manticore/platforms/evm.py", line 2684, in execute
    self.current_vm.execute()
  File "/home/gustavo/.local/lib/python3.6/site-packages/manticore-0.3.0-py3.6.egg/manticore/platforms/evm.py", line 1210, in execute
    last_pc, last_gas, instruction, arguments, fee, allocated = self._checkpoint()
  File "/home/gustavo/.local/lib/python3.6/site-packages/manticore-0.3.0-py3.6.egg/manticore/platforms/evm.py", line 1106, in _checkpoint
    fee = self._calculate_gas(*arguments)
  File "/home/gustavo/.local/lib/python3.6/site-packages/manticore-0.3.0-py3.6.egg/manticore/platforms/evm.py", line 1079, in _calculate_gas
    return current.fee + implementation(*arguments)
  File "/home/gustavo/.local/lib/python3.6/site-packages/manticore-0.3.0-py3.6.egg/manticore/platforms/evm.py", line 1533, in SHA3_gas
    return GSHA3WORD * (ceil32(size) // 32) + memfee
  File "/home/gustavo/.local/lib/python3.6/site-packages/manticore-0.3.0-py3.6.egg/manticore/core/smtlib/expression.py", line 295, in __add__
    return BitVecAdd(self, self.cast(other))
  File "/home/gustavo/.local/lib/python3.6/site-packages/manticore-0.3.0-py3.6.egg/manticore/core/smtlib/expression.py", line 284, in cast
    assert value.size == self.size
AssertionError
 
2019-07-22 10:25:10,346: [15617] m.e.manticore:INFO: 0 alive states, 3 terminated states
2019-07-22 10:25:10,378: [16754] m.c.manticore:INFO: Generated testcase No. 0 - RETURN(1 txs)
2019-07-22 10:25:10,383: [16755] m.c.manticore:INFO: Generated testcase No. 1 - REVERT(2 txs)
2019-07-22 10:25:10,387: [16757] m.c.manticore:INFO: Generated testcase No. 2 - REVERT(2 txs)
2019-07-22 10:25:10,417: [16760] m.c.manticore:INFO: Generated testcase No. 3 - RETURN(1 txs)