My rule seems to be correct but I keep getting the following assert message: Unwinding condition in a loop. What is this type of assert and why do I get it?
“Unwind condition in a loop” asserts happen due to the way Certora Prover is dealing with loops. It does “loop unrolling”, means that the code inside the scope of the loop is copied several times. By default, the code inside the scope is copied one time and then an assert of the form
assert !exp when
exp is the loop condition. This may lead to the unwinding assert if one copy of the code is not enough to make
exp false (for example
i is initialized to 0).
Try using the flags
--optimistic_loop as described in the docs:
Be aware that using strings also leads to this assert message due to the way strings are implemented in solidity.