-
Notifications
You must be signed in to change notification settings - Fork 5.7k
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
ICE in Z3Interface::fromZ3Expr()
when running tests on Arch Linux
#15196
Comments
Try Disabling the SMT Checker: As mentioned in my previous response, you can try compiling Solidity with the SMT checker disabled by using the --no-auto-solve or --no-smt compiler options. This may allow the compilation to succeed, but you'll lose the benefits of the formal verification provided by the SMT checker. |
This is compilation straight from the arch user repositories https://aur.archlinux.org/packages/solidity |
I will take a look at it. |
This is definitely a bug that we should fix. These assertions do not fail in our CI so I suspect this has something to do with the difference in Z3 versions. We're still running our tests on 4.12 and it's possible that 4.13 has introduced something new that the current code assumes won't happen. @blishko @pgebal maybe you could take a look? We should also finally update to 4.13 (#15198). @Spixmaster Yeah, if this is failing then disabling the SMT checker is probably the best course of action until we release 0.8.27 with a fix. Another workaround might be to use older Z3 (if that's indeed the issue), but that does not seem to be possible on Arch Linux since it ships the latest one. |
Z3Interface::fromZ3Expr()
when running tests on Arch Linux
I am done with my testing. I did not experience the issues before because I did not have I am not sure whether this is an issue or expected behaviour and the process would have finished. |
It's likely they'd finish if you gave them more time. IIRC the last time I checked (which was quite a while ago) they were taking ~30% of the time needed to run the whole suite. And the suite is quite extensive so it takes a lot of time to run it all. In CI we heavily rely on parallelization to make that manageable. |
I will start investigating on Monday. |
That would conform to my observation. |
Trying to compile solidity from source I run into this:
I think I'm building
solidity_0.8.26
Steps to repro:
The text was updated successfully, but these errors were encountered: