Samuel Chassot

Let's try to first impose a restriction on `swap` to only take a variable as argument. This would solve this unsoundness issue.

And if we disallow ´Cell´ to appear in arguments altogether?

Implemented in #1461

So in summary, it would be interesting to have a notion of "private" vs "public" implementations: so - always`opaque` - `opaque` from the outside of the class - not `opaque`

can use the `unfold` operator where the opaque function body should be visible. Maybe we could add it automatically?

> We can hopefully also accept Exception as a super class (e.g. define it in stainless.lang) and permit its subclasses. Here users would have to redefine their own exception classes...

https://github.com/epfl-lara/stainless/blob/54399d0a62cabd8c2480b8a14cc1fbf0d684e426/frontends/library/stainless/lang/package.scala#L41 there was a tentative apparently.

This compiles, once I removed the check in `FragmentChecker`: ``` import stainless.lang.Exception class IllegalArgumentException(msg: String) extends Exception object ThrowTest { def f(): Unit = throw new IllegalArgumentException("This is an exception")...

I added a note to point to the latest Scala 2.13 supporting release

@vkuncak Perfect! As a commit message, I'll keep the github generated one. Does it work for you?