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

SMTChecker can't last for more than 200+ contracts #14345

Open
molecula451 opened this issue Jun 21, 2023 · 0 comments
Open

SMTChecker can't last for more than 200+ contracts #14345

molecula451 opened this issue Jun 21, 2023 · 0 comments
Labels

Comments

@molecula451
Copy link
Contributor

molecula451 commented Jun 21, 2023

Description

put on a test to make the SMTChecker formal proof verification the contracts recursively and it can't last for more than 200+ without Solc error, or the compiler hanging, on FAST hardware,

Environment

  • Compiler version: 0.8.19 - last
  • Target EVM version (as per compiler settings): any
  • Framework/IDE (e.g. Truffle or Remix): plain solc
  • EVM execution environment / backend / blockchain client: any
  • Operating system: any

Steps to Reproduce

Check more than 200+ contracts with SMTChecker (using Z3) recursively without hanging fast hardware, or outputting error. Actually outputting the checker logs

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant