Malte Schwerhoff

Being able to disable dragging is awesome! Would be great if this pull request were merged in soon :crossed_fingers:

I don't believe so. The simplifier is in general not exhaustive/complete. Pull requests are welcome :-)

Voila also doesn't use labels with invariants. Generally, I'm also in favour of keeping the semantics simple, and would thus reject non-loop-head labels with invariants. But as a consequence, we...

Debugging these kinds of performance issues is unfortunately very difficult. Given all the quantifiers, it *could* be that there is a matching loop (cycle in the instantiation graph), or that...

> However, the complete `elect.pvl` file is still unstable even with the `--numberOfParallelVerifiers` flag. Could you please post that file's Viper program as well? > When I use the flag,...

Thank you for the additional file. > When you say the root cause is that there are too many quantifier instantiations, do you mean there are too many foralls, that...

The problem affects the Viper IDE quite a bit, as illustrated by the screenshot below. 

Further highlighting surprises (all method calls fail due to their precondition): * difference between ending a line with a semicolon, and not * difference between a method that returns a...

That seems to be expected behaviour: in the first version, second quantifier, `l` is unconstrained, and could hence be outside the bounds of `last[z]`. In the second version, that is...

Sorry, my bad; I didn't spot that the LHS of the two implications were identical. Looks like a triggering problem that results in the first quantifier's body not being available...