Question about some absurd reported cases

[renardbebe]

When I use Oyente to check the following contract, it has reported some integer overflow warnings in s[2] and s[3].
contract Benchmark {

uint128[] private s;

function init() public {
    s.length = 4;
    s[0] = 0xAA;
    s[1] = 0xBB;
    s[2] = 0xCC;
    s[3] = 0xDD;
}

}

Maybe someone could help me to understand, why and how Oyente reports these issues?
Any reasonable idea will help me a lot, thank you for all your help!

[yxliang01]

@renardbebe Could you paste the Oyente terminal output here as code block?

[renardbebe]

@renardbebe Could you paste the Oyente terminal output here as code block?

WARNING:root:You are using evm version 1.8.2. The supported version is 1.7.3
WARNING:root:You are using solc version 0.4.25, The latest supported version is 0.4.19
INFO:root:contract /arithmetic_all/testContracts/manticore_integer_overflow_dynarray.sol:Benchmark:
INFO:symExec:	============ Results ===========
INFO:symExec:	  EVM Code Coverage: 			 81.7%
INFO:symExec:	  Integer Underflow: 			 False
INFO:symExec:	  Integer Overflow: 			 True
INFO:symExec:	  Parity Multisig Bug 2: 		 False
INFO:symExec:	  Callstack Depth Attack Vulnerability:  False
INFO:symExec:	  Transaction-Ordering Dependence (TOD): False
INFO:symExec:	  Timestamp Dependency: 		 False
INFO:symExec:	  Re-Entrancy Vulnerability: 		 False
INFO:symExec:/arithmetic_all/testContracts/manticore_integer_overflow_dynarray.sol:13:9: Warning: Integer Overflow.
        s[2]
/arithmetic_all/testContracts/manticore_integer_overflow_dynarray.sol:14:9: Warning: Integer Overflow.
        s[3]
INFO:symExec:	====== Analysis Completed ======

@yxliang01 Here is the Oyente terminal output. I am wondering why it reports the warning in s[2] and s[3], and if the ADD operation involved in the calculation of array offset caused the false alarm, why s[0] and s[1] is assumed to be safe?
I would appreciate it if I could understand the cause of this problem with your help!

[yxliang01]

I think it might be a bug. I couldn't really see how integer overflow can happen here. Could you try using the officially supported versions of solc and evm and see whether it reports the same thing? From there, we can investigate more deeply.