CryptoMental

I have no idea why Travis errored, the build is fine locally: ``` $ git clone https://github.com/cryptomental/augur-core.git $ cd augur-core/ $ git co feature/ignore-selected-oyente-issues $ npm run docker:run:test:security:oyente ```

Hi @nuevoalex , I have to split the answer in two parts. First, the reason of the behavior that you observe is that Oyente does not treat Integer underflow/overflow hits...

@nuevoalex yes. We can leave this PR in a limbo until there is a response from Z3 side. Perhaps I can also have a look at their dev branch, try...

@nuevoalex I found out that Z3 segfaults at https://github.com/Z3Prover/z3/blob/master/src/smt/theory_bv.cpp#L1394 , I added this information to https://github.com/Z3Prover/z3/issues/1766 but unfortunately I cannot do much more about it, hopefully Z3 team will pick...

I am attaching a full Oyente log with debug log enabled. [oyente.debug.txt](https://github.com/melonproject/oyente/files/2176161/oyente.debug.txt)

Hi @yxliang01 there has not been any reply since two weeks but I noticed that you commented on another ticket yesterday. Is the Oyente project still maintained? And would it...

Hi @yxliang01 thank you a lot for looking into this. This is exactly the case - there are no assert statements and assertions should be marked as false positives. I...

Hi @yxliang01 again, I upgraded Z3 solver and those false assertions are gone, but the analysis was just half done as it segfaulted https://github.com/AugurProject/augur-core/issues/689 , I will try to find...

Hi @yxliang01 it did not get to that point, I pasted the whole log for you here https://gist.github.com/cryptomental/c5ff857becfeda48c8c0fbb432eeba90

Hi @yxliang01 the assertions there are 'true' assertions. The only one found was for Cash.sol, where indeed the assertion could have been triggered. ``` EVM Code Coverage: 97.2% Integer Underflow:...