Find a sophisticated motivating example for Solidity code analysis

[zchn]

The analysis should detect vulnerabilities not discoverable by the solc compiler.

The vulnerability should exist in real solidity contracts.

[Optional] the solidity contract should be used by more than X accounts.