Martin Blicha
Martin Blicha
I should squash everything to a single commit?
I tried to keep the commits logically compact. I think I can improve some of the commit messages and squash some of the commits together, but I would prefer to...
Looks like [Eldarica](https://github.com/uuverifiers/eldarica) 2.1 can solve this example (~12 seconds wall clock time on my machine).
It seems to me you need a quantified invariant here in order to be inductive. Something like $\forall i : i \geq element \implies \neg set[i]$. You may try `FreqHorn`...
Would it help if I try to minimize the example further?
I have tried rerunning the benchmarks with `master` and they now work fine. I am closing this issue and I am looking forward to a new release!
After #15252, I think we can close this issue?
This has the same underlying cause as the incorrect behaviour reported in #14275. However, the problem reported here is much more serious.
Here is the simplified example: ``` contract Test { function loop() public { for (uint k = 0; (k == 0 ? true : false); k++) { } } }...
How important is this right now? I guess we need to implement handling of `call` with value the same way we now handle `transfer`?