Alexander Stekelenburg

I would say the underlying problem is #1301. That variable should never have been in the outer scope but because we get rid of “empty” scopes before we collect all...

I think the parsing is not the problem for the CI because what times out is some assert which it then concludes can't be proven (probably because the CI is...

Thanks for the report, the lack of a proper error here is definitely a bug. In VerCors we write Viper's inhale-exhale expression as `\polarity_dependent(inhale_expr, exhale_expr)` that should allow you to...

This crash occurs because we ignore Viper's checks that happen after parsing. In your output log you can see the line: ``` [WARN] Quantified arguments can only be used directly...

I'm not 100% sure what they mean by direct expression in Viper but I guess basically anything of the form `a.b` is a direct expression of `a`, but most other...

> I fixed some low hanging fruit. But for a total fix, we need the website to run at least some later version of VerCors. So I'll stop for now....

Here's a version of the script that outputs in the JUnit XML format (I saw there were multiple libraries for making such an XML file I picked a random one)...

I did add a note a couple of months ago that we don't support set comprehensions at the moment, but the change seems to have not appeared on the website,...

> What are the options here? > > 1. Might it be an idea to have a (dedicated) runner somewhere in the cloud, which runs our VerCors examples and sends...

That's interesting, when you exclude the call you get the the expected error about the contract. But when calling it the contract is evaluated again, and this leads to the...