It would be more effective to test bug detection tools against a database of real smart contract code with precisely identified vulnerabilities and example patches. Any benchmark must contain more than simple tests: it must approximate real software with enough complexity to properly stress tools for automated bug discovery.
There is more discussion about what a good bug detection benchmark looks like in our own Challenge Sets from DARPA (https://blog.trailofbits.com/2016/08/01/your-tool-works-bett...) and something we were working on that is similar for smart contracts in "Not So Smart Contracts" (https://github.com/crytic/not-so-smart-contracts).
You'll note that ETH Zurich and ChainSecurity came up with their own benchmark that meets the description above when they evaluated VerX in the paper I linked above. I'm eagerly awaiting the release of those test cases since they'll help us improve the functionality of many of our tools.
If you want to compare the effectiveness of symbolic execution engines, then you should compare how many unique codepaths they can reach. ETH Zurich recently completed such an analysis in their paper on VerX (https://files.sri.inf.ethz.ch/website/papers/sp20-verx.pdf), an abstract interpretation-based verifier, and found that Manticore had the most complete model of the EVM compared to other symbolic execution engines by far, and we have continued to improve its accuracy in the releases since then. That said, ETH Zurich did underestimate a few of the capabilities of Manticore that we hope to better describe in an upcoming academic paper.
If you're looking to start using Manticore, then browse through the manticore-examples repository (https://github.com/trailofbits/manticore-examples) where we have complete working solutions to CTF challenges, crackmes, logic bombs, and other programs that Manticore excels at exploring.