TestResult4

WARNING:root:You are using an untested version of z3. 4.5.1 is the officially tested version
WARNING:root:You are using evm version 1.8.16. The supported version is 1.7.3
WARNING:root:You are using solc version 0.4.24, The latest supported version is 0.4.19
INFO:root:contract ./contracts/4.sol:Reentrance:
INFO:symExec:	============ Results ===========
INFO:symExec:	  EVM Code Coverage: 			 97.0%
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): True
INFO:symExec:	  Timestamp Dependency: 		 False
INFO:symExec:	  Re-Entrancy Vulnerability: 		 True
INFO:symExec:./contracts/4.sol:16:9: Warning: Integer Overflow.
        userBalance[msg.sender] += msg.value
Integer Overflow occurs if:
    userBalance[msg.sender] = 101463263230742744495392917458341184112223491530675579251756683875854454543212
INFO:symExec:Flow1
./contracts/4.sol:33:16: Warning: Transaction-Ordering Dependency.
        if( ! (msg.sender.call.value(amount)()
Flow2
./contracts/4.sol:22:16: Warning: Transaction-Ordering Dependency.
        if( ! (msg.sender.call.value(userBalance[msg.sender])()
INFO:symExec:./contracts/4.sol:22:16: Warning: Re-Entrancy Vulnerability.
        if( ! (msg.sender.call.value(userBalance[msg.sender])()
INFO:symExec:	====== Analysis Completed ======