Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Halmos is not able to generate paths for contracts deployed with CREATE3 #217

Open
aviggiano opened this issue Nov 8, 2023 · 0 comments
Labels
bug Something isn't working

Comments

@aviggiano
Copy link
Contributor

aviggiano commented Nov 8, 2023

Describe the bug

While testing Halmos on a DeFi protocol, Halmos was not able to generate valid paths due to the contracts being deployed with CREATE3.

To Reproduce

I created a MWE with this issue

$ git clone https://github.com/aviggiano/property-based-testing-benchmark
$ cd projects/create3

# will succeed
$ forge test --match-test test

Running 1 test for test/Create3.t.sol:Create3Test
[PASS] test_create3() (gas: 183018)
Test result: ok. 1 passed; 0 failed; 0 skipped; finished in 4.91ms

Ran 1 test suites: 1 tests passed, 0 failed, 0 skipped (1 total tests)


# will fail
$ halmos --function test

Running 1 tests for test/Create3.t.sol:Create3Test
[FAIL] test_create3() (paths: 0/0, time: 0.22s, bounds: [])
Symbolic test result: 0 passed; 1 failed; time: 0.24s

Environment:

  • OS: macOS
  • Python version: Python 3.11.4
  • Halmos and other dependency versions: Halmos 0.1.10.dev2+g44dca2e

Additional context
Add any other context about the problem here.

@aviggiano aviggiano added the bug Something isn't working label Nov 8, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant