Currently, Oyente is available as a Docker image for easy testing and installation. It is available at https://github.com/melonproject/oyente and can be downloaded and tested.
In the following example, a simple contract taken from Solidity documentation that contains a reentrancy bug has been tested and it is shown that Oyente successfully analyzes the code and finds the bug:
Contract with reentrancy bug, source: solidity documentation
This sample code contains a reentrancy bug which basically means that if a contract is interacting with another contract or transferring Ether, it is effectively handing over the control to that ...
