/* Curious case of Egg invariant.
When a class is defined inside a method, the context is captured inside an invariant.
If this context is mutable and is changed before class declaration, the captured
check is wrong and an attempt to construct class instance fails.
The context should probably not be captured when there is no syntactic dependency.
If there is a syntactic dependency that is mutable, probably we should just throw
unless there is a clear way to handle such mutable context.
*/
import stainless.lang.*
import stainless.annotation.*
import StaticChecks.*
object EggInvariant {
case class Mut(var x: Int)
def test = {
val m = Mut(2)
m.x = 1
assert(m.x == 1)
final case class Egg(n: Int)
Egg(3)
}
}
The generated invariant is: