Michael Emmi

And here is my rough understanding of the root cause: 1. line number adder iterates over the methods of class C 2. runs jb pack on body of bar, including...

It seems like there are at least two approaches to avoid CME here: * iterate over snapshot(s) of method list, or * do not change method list. For the first,...

@linghuiluo @StevenArzt @mbenz89 any thoughts about the above?

> Only phantom methods should be created during the (transitive) method resolving started by the LineNumberAdder But should phantom methods be added to the class for which bodies are already...

Hey @fdupress are you saying that some version of Ct-Verif supported dynamic-length annotations? I was under the impression that we had not implemented that, though I might be forgetting something.

Smack has never attempted this kind of thing, but it would indeed use quantifiers to express such specs (and loop invariants to verify the specs). The issue I intended to...

Does that mean that there’s no way to say that something changed depending on the return value? That situation actually something common to many APIs like collections. For instance, the...

That sounds reasonable to me.

I have not yet. I have seen a related issue ethereum/solidity#5130 which was fixed in ethereum/solidity#5558 in December, but I haven’t determined whether the code we’re using includes ethereum/solidity#5558.

It succeeds with `--artihmetic mod`, but why should it work actually (?) when the pre-value of `balance` could be so large so that the post-value overflew. Looking again, I would...