Federico Poli

Can you try adding the following configuration to the "rules" section of `.eslintrc`? ``` // Report unused variables only if they don't start with "_". // Source: https://stackoverflow.com/a/64067915/2491528 "no-unused-vars": "off",...

> To use these new features, prusti needs to be at least at version 0.3.0. @Aurel300 this means that we should publish a >=0.3.0 Prusti release *before* merging this PR.

Why is `self.f` checked to have enough permission?

I see, so when unfolding `acc(F(x), rd())` Silicon checks that the scaled `acc(self.f, rd() * rd())` is enough to access the `self.f` in `G(self.f)`. But then, why does the well-definedness...

For a similar case, I found that it's enough to assume `none < rd() * rd()` before the `unfold`, like in the following program. For some reason, adding that property...

When fixing this behaviour, please consider also [Simplifier.scala](https://github.com/viperproject/silver/blob/master/src/main/scala/viper/silver/ast/utility/Simplifier.scala) and [SimplifierTests.scala](https://github.com/viperproject/silver/blob/master/src/test/scala/SimplifierTests.scala). I'm not sure whether Silicon or Carbon actually use this simplifier, but for sure in Prusti we do.

Currently in Prusti we encode Rust's `left % right` to Z3's `(left >= 0 || left % right == 0) ? (left % right) : (left % right - abs(right))`....

> I'm test-driving to move one of my organisation's repositories to Github, but in the end all existing pull requests (already merged) are converted into issues. Is it meant to...

Related to issue #9. It would be nice to solve both at once.

Indeed, Carbon doesn't seem to support quantified magic wands. I get the same kind of Java exception with the following program. ``` predicate P(x: Int) method lemma() requires forall x:...