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 while(i<=3) and i is initialized to 0).
Try using the flags --loop_iter and --optimistic_loop as described in the docs:
https://docs.certora.com/en/latest/docs/ref-manual/approx/loops.html
Be aware that using strings also leads to this assert message due to the way strings are implemented in solidity.
1 Like