Open
Description
Describe the bug
I was recently trying to replicate Solmate's SignedWadMath.sol contract's wadMul() bug (see @karmacoma-eth's tweet). When I ran halmos --smt-div the tests PASSED with the following output:
Expected behavior: The test should fail.
To Reproduce
- Use this code: https://gist.github.com/PraneshASP/352924cdbf6935cb73631eb73bd5f273
- Set solc version in your
foundry.tomlto0.8.15. - Run
halmos --smt-div
Environment:
- OS: Linux - Ubuntu 20.04
- Python version: Python 3.9.17
- Halmos and other dependency versions: Halmos 0.1.3.dev3+gd2c5d27
Additional context
Halmos produced expected counterexamples when solc version was >= 0.8.17