-
Notifications
You must be signed in to change notification settings - Fork 68
warnings
Welcome to the halmos wiki!
It seems you've encountered a halmos bug or limitation! Some options:
- search for existing issues
- ask about your issue on Telegram
- file a new issue (please provide as many details as possible)
To avoid the path explosion problem, halmos performs bounded analysis. This message means that you have hit such a bound, and so the exploration of all possible paths has been cut short.
Workarounds:
- you can try reducing the complexity of the code under test, in particular around looping and branching
- you can try increasing the loop bound with the
--loopoption (but results may take longer)
You can learn more about loop unrolling and bounded execution in Formally Verifying Loops: Part 1
During execution, the EVM in Halmos encountered an opcode that it does not support yet. Some of these are already known, see the existing issue.
Please consider implementing the missing opcode and opening a pull request, adding a new opcode is typically a good first issue to tackle!
halmos employs SMT solvers to search for counterexamples. But if the bytecode includes nonlinear arithmetic (division, multiplication, modulo, exponentiation...), the SMT solvers might become very slow, even if they are not relevant to assertions. To mitigate this, the nonlinear arithmetic reasoning is disabled by default, but this can sometimes result in generating invalid counterexamples.
There is a known case where this can happen if the contract code contains exponentiation (e.g. x ** 4, EXP EVM instruction). In this case, the following option may be helpful:
--smt-exp-by-const N interpret constant power up to N (default: 2)
This is typically caused by a timeout in the assertion solver. Here are some potential things you can try to fix this:
- try to reduce the complexity of the test function (for instance by removing irrelevant code)
- increase the assertion solver timeout, or disable the timeout entirely with
--solver-timeout-assertion 0
Halmos tried to load bytecode that contains library placeholders. This typically happens when you use public library functions in a Solidity source file, resulting in unlinked bytecode that will perform a DELEGATECALL at an address that is as yet undetermined because the placeholder has not been replaced by a concrete address.
See:
As a workaround, it is suggested to avoid using public library functions (change the visibility to internal or copy the function in your own contract if possible)