Marco Eilers

Hm. I tried this again, and I still think it doesn't work the way it should. IMO if ignore_fully_annotated_function is set to true, the following program should be accepted: ```...

This wasn't really motivated by a specific program that's slow, it was more of an idea that we could potentially explore if we get performance problems and there's a chance...

Nagini and 2Vyper also don't use label invariants and wouldn't be affected.

I don't. If I remember correctly, we basically implemented the code for storing parse positions ourselves when we moved to fastparse (the library didn't offer that feature), and then our...

I'll have a look at this in the next couple of days. As you said, this will almost certainly have performance implications (one way or the other, it might actually...

I tried it out quickly (https://github.com/viperproject/silicon/tree/meilers_adt_sortwrappers) and it seems to mostly work fine. At least two examples get a lot slower and four tests fail, but apart from that, everything...

I'll need more time to look into fixing the sort wrappers. But the predicate trigger issue is fixed now, so your program verifies if you explicitly add the predicate as...

I'll look at it tomorrow.

@JonasAlaif That seems to be a separate issue, I've filed an issue for it here: #698

I guess to avoid this we'd either have to re-check well-definedness on unfold, or verify well-definedness using an unknown positive multiplicator?