stainless: Inconsistent change propagation in `AntiAliasing`

The following test case shows of some strange behaviour with change/mutation propagation in the AntiAliasing/ImperativeCodeElimination phases.

import stainless.lang._
import stainless.annotation._

object Mutable {
  final case class Mut[@mutable T](var t: T)
  final case class Thing[@mutable T](var field: T)

  def change_thing[@mutable T](thing: Mut[Thing[T]], t: T) = {
    thing.t = Thing(freshCopy(t))
  }
  def main() = {
    val thing = Thing(123)
    change_thing(Mut(thing), 456)
    assert(thing.field == 456)

    val thing2 = Mut(thing)
    change_thing(thing2, 789)
    assert(thing.field == 789)

    val thing3 = Mut(thing)
    thing3.t = Thing(0)
    assert(thing.field == 0)
  }
}

For the first block, the changes made to the wrapped thing are correctly propagated back, whereas for the next two blocks, the changes to the Mut(thing) are only propagated back to the bound thing2/thing3.

EDIT: with the latest master version (a5292b4a3a55a3ba85c18aaa55db2f915b95724f), the third assertion also passes, even though it is not clear to me from the trees, why…

stainless trees in some phases

Performed with the latest master version (a5292b4a3a55a3ba85c18aaa55db2f915b95724f)

[info] [ Debug  ] Symbols before Preprocessing
[info] [ Debug  ] 
[info] [ Debug  ] -------------Functions-------------
[info] [ Debug  ] def change_thing[T @mutable](thing: Mut[Thing[T @mutable]], t: T @mutable): Unit = thing.t_=(Thing[T @mutable](freshCopy(t)))
[info] [ Debug  ] 
[info] [ Debug  ] @accessor(t)
[info] [ Debug  ] @method(Mut)
[info] [ Debug  ] def t: T @mutable = this.t
[info] [ Debug  ] 
[info] [ Debug  ] def main: Unit = {
[info] [ Debug  ]   val thing: Thing[Int] = Thing[Int](123)
[info] [ Debug  ]   change_thing[Int](Mut[Thing[Int]](thing), 456)
[info] [ Debug  ]   assert(thing.field == 456)
[info] [ Debug  ]   val thing2: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   change_thing[Int](thing2, 789)
[info] [ Debug  ]   assert(thing.field == 789)
[info] [ Debug  ]   val thing3: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   thing3.t_=(Thing[Int](0))
[info] [ Debug  ]   assert(thing.field == 0)
[info] [ Debug  ]   ()
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] @accessor(t)
[info] [ Debug  ] @method(Mut)
[info] [ Debug  ] def t_=(x$1: T @mutable): Unit = this.t = x$1
[info] [ Debug  ] 
[info] [ Debug  ] @accessor(field)
[info] [ Debug  ] @method(Thing)
[info] [ Debug  ] def field: T @mutable = this.field
[info] [ Debug  ] 
[info] [ Debug  ] @accessor(field)
[info] [ Debug  ] @method(Thing)
[info] [ Debug  ] def field_=(x$1: T @mutable): Unit = this.field = x$1
[info] [ Debug  ] 
[info] [ Debug  ] -------------Classes-------------
[info] [ Debug  ] case class Thing[T @mutable]((field: T @mutable) @var) {
[info] [ Debug  ]   
[info] [ Debug  ] 
[info] [ Debug  ]   @accessor(field)
[info] [ Debug  ]   @method(Thing)
[info] [ Debug  ]   def field: T @mutable = this.field
[info] [ Debug  ]   
[info] [ Debug  ]   @accessor(field)
[info] [ Debug  ]   @method(Thing)
[info] [ Debug  ]   def field_=(x$1: T @mutable): Unit = this.field = x$1
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] case class Mut[T @mutable]((t: T @mutable) @var) {
[info] [ Debug  ]   
[info] [ Debug  ] 
[info] [ Debug  ]   @accessor(t)
[info] [ Debug  ]   @method(Mut)
[info] [ Debug  ]   def t: T @mutable = this.t
[info] [ Debug  ]   
[info] [ Debug  ]   @accessor(t)
[info] [ Debug  ]   @method(Mut)
[info] [ Debug  ]   def t_=(x$1: T @mutable): Unit = this.t = x$1
[info] [ Debug  ] }
...
[info] [ Debug  ] Symbols before AntiAliasing
[info] [ Debug  ] 
[info] [ Debug  ] -------------Functions-------------
[info] [ Debug  ] def change_thing[T @mutable](thing: Mut[Thing[T @mutable]], t: T @mutable): Unit = thing.t = Thing[T @mutable](freshCopy(t))
[info] [ Debug  ] 
[info] [ Debug  ] def main: Unit = {
[info] [ Debug  ]   val thing: Thing[Int] = Thing[Int](123)
[info] [ Debug  ]   change_thing[Int](Mut[Thing[Int]](thing), 456)
[info] [ Debug  ]   assert(thing.field == 456)
[info] [ Debug  ]   val thing2: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   change_thing[Int](thing2, 789)
[info] [ Debug  ]   assert(thing.field == 789)
[info] [ Debug  ]   val thing3: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   thing3.t = Thing[Int](0)
[info] [ Debug  ]   assert(thing.field == 0)
[info] [ Debug  ]   ()
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] -------------Classes-------------
[info] [ Debug  ] case class Thing[T @mutable]((field: T @mutable) @var)
[info] [ Debug  ] 
[info] [ Debug  ] case class Mut[T @mutable]((t: T @mutable) @var)
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] Symbols after AntiAliasing
[info] [ Debug  ] 
[info] [ Debug  ] -------------Functions-------------
[info] [ Debug  ] def change_thing[T @mutable](thing: Mut[Thing[T @mutable]], t: T @mutable): (Unit, Mut[Thing[T @mutable]]) = {
[info] [ Debug  ]   var thing: Mut[Thing[T @mutable]] = thing
[info] [ Debug  ]   ({
[info] [ Debug  ]     thing = Mut[Thing[T @mutable]](Thing[T @mutable](freshCopy(t)))
[info] [ Debug  ]     ()
[info] [ Debug  ]   }, thing)
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] def main: Unit = {
[info] [ Debug  ]   var thing: Thing[Int] = Thing[Int](123)
[info] [ Debug  ]   var res: (Unit, Mut[Thing[Int]]) = change_thing[Int](Mut[Thing[Int]](thing), 456)
[info] [ Debug  ]   (if (res._2.isInstanceOf[Mut[Thing[Int]]]) {
[info] [ Debug  ]     thing = @unchecked @unchecked res._2.asInstanceOf[Mut[Thing[Int]]].t.asInstanceOf[Thing[Int]]
[info] [ Debug  ]   } else {
[info] [ Debug  ]     ()
[info] [ Debug  ]   })
[info] [ Debug  ]   res._1
[info] [ Debug  ]   assert(thing.field == 456)
[info] [ Debug  ]   var thing2: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   var res: (Unit, Mut[Thing[Int]]) = change_thing[Int](thing2, 789)
[info] [ Debug  ]   (if (res._2.isInstanceOf[Mut[Thing[Int]]]) {
[info] [ Debug  ]     thing2 = @unchecked Mut[Thing[Int]](@unchecked res._2.asInstanceOf[Mut[Thing[Int]]].t).asInstanceOf[Mut[Thing[Int]]]
[info] [ Debug  ]   } else {
[info] [ Debug  ]     ()
[info] [ Debug  ]   })
[info] [ Debug  ]   res._1
[info] [ Debug  ]   assert(thing.field == 789)
[info] [ Debug  ]   var thing3: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   thing3 = Mut[Thing[Int]](Thing[Int](0))
[info] [ Debug  ]   ()
[info] [ Debug  ]   assert(thing.field == 0)
[info] [ Debug  ]   ()
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] -------------Classes-------------
[info] [ Debug  ] case class Thing[T @mutable]((field: T @mutable) @var)
[info] [ Debug  ] 
[info] [ Debug  ] case class Mut[T @mutable]((t: T @mutable) @var)
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] Ensuring well-formedness after phase AntiAliasing...
[info] [ Debug  ] => SUCCESS
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] Symbols before ReturnElimination
[info] [ Debug  ] 
[info] [ Debug  ] -------------Functions-------------
[info] [ Debug  ] def change_thing[T @mutable](thing: Mut[Thing[T @mutable]], t: T @mutable): (Unit, Mut[Thing[T @mutable]]) = {
[info] [ Debug  ]   var thing: Mut[Thing[T @mutable]] = thing
[info] [ Debug  ]   ({
[info] [ Debug  ]     thing = Mut[Thing[T @mutable]](Thing[T @mutable](freshCopy(t)))
[info] [ Debug  ]     ()
[info] [ Debug  ]   }, thing)
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] def main: Unit = {
[info] [ Debug  ]   var thing: Thing[Int] = Thing[Int](123)
[info] [ Debug  ]   var res: (Unit, Mut[Thing[Int]]) = change_thing[Int](Mut[Thing[Int]](thing), 456)
[info] [ Debug  ]   (if (res._2.isInstanceOf[Mut[Thing[Int]]]) {
[info] [ Debug  ]     thing = @unchecked @unchecked res._2.asInstanceOf[Mut[Thing[Int]]].t.asInstanceOf[Thing[Int]]
[info] [ Debug  ]   } else {
[info] [ Debug  ]     ()
[info] [ Debug  ]   })
[info] [ Debug  ]   res._1
[info] [ Debug  ]   assert(thing.field == 456)
[info] [ Debug  ]   var thing2: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   var res: (Unit, Mut[Thing[Int]]) = change_thing[Int](thing2, 789)
[info] [ Debug  ]   (if (res._2.isInstanceOf[Mut[Thing[Int]]]) {
[info] [ Debug  ]     thing2 = @unchecked Mut[Thing[Int]](@unchecked res._2.asInstanceOf[Mut[Thing[Int]]].t).asInstanceOf[Mut[Thing[Int]]]
[info] [ Debug  ]   } else {
[info] [ Debug  ]     ()
[info] [ Debug  ]   })
[info] [ Debug  ]   res._1
[info] [ Debug  ]   assert(thing.field == 789)
[info] [ Debug  ]   var thing3: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   thing3 = Mut[Thing[Int]](Thing[Int](0))
[info] [ Debug  ]   ()
[info] [ Debug  ]   assert(thing.field == 0)
[info] [ Debug  ]   ()
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] -------------Classes-------------
[info] [ Debug  ] case class Thing[T @mutable]((field: T @mutable) @var)
[info] [ Debug  ] 
[info] [ Debug  ] case class Mut[T @mutable]((t: T @mutable) @var)
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] Not printing symbols after ReturnElimination as they did not change
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] Ensuring well-formedness after phase ReturnElimination...
[info] [ Debug  ] => SUCCESS
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] Symbols before ImperativeCodeElimination
[info] [ Debug  ] 
[info] [ Debug  ] -------------Functions-------------
[info] [ Debug  ] def change_thing[T @mutable](thing: Mut[Thing[T @mutable]], t: T @mutable): (Unit, Mut[Thing[T @mutable]]) = {
[info] [ Debug  ]   var thing: Mut[Thing[T @mutable]] = thing
[info] [ Debug  ]   ({
[info] [ Debug  ]     thing = Mut[Thing[T @mutable]](Thing[T @mutable](freshCopy(t)))
[info] [ Debug  ]     ()
[info] [ Debug  ]   }, thing)
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] def main: Unit = {
[info] [ Debug  ]   var thing: Thing[Int] = Thing[Int](123)
[info] [ Debug  ]   var res: (Unit, Mut[Thing[Int]]) = change_thing[Int](Mut[Thing[Int]](thing), 456)
[info] [ Debug  ]   (if (res._2.isInstanceOf[Mut[Thing[Int]]]) {
[info] [ Debug  ]     thing = @unchecked @unchecked res._2.asInstanceOf[Mut[Thing[Int]]].t.asInstanceOf[Thing[Int]]
[info] [ Debug  ]   } else {
[info] [ Debug  ]     ()
[info] [ Debug  ]   })
[info] [ Debug  ]   res._1
[info] [ Debug  ]   assert(thing.field == 456)
[info] [ Debug  ]   var thing2: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   var res: (Unit, Mut[Thing[Int]]) = change_thing[Int](thing2, 789)
[info] [ Debug  ]   (if (res._2.isInstanceOf[Mut[Thing[Int]]]) {
[info] [ Debug  ]     thing2 = @unchecked Mut[Thing[Int]](@unchecked res._2.asInstanceOf[Mut[Thing[Int]]].t).asInstanceOf[Mut[Thing[Int]]]
[info] [ Debug  ]   } else {
[info] [ Debug  ]     ()
[info] [ Debug  ]   })
[info] [ Debug  ]   res._1
[info] [ Debug  ]   assert(thing.field == 789)
[info] [ Debug  ]   var thing3: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   thing3 = Mut[Thing[Int]](Thing[Int](0))
[info] [ Debug  ]   ()
[info] [ Debug  ]   assert(thing.field == 0)
[info] [ Debug  ]   ()
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] -------------Classes-------------
[info] [ Debug  ] case class Thing[T @mutable]((field: T @mutable) @var)
[info] [ Debug  ] 
[info] [ Debug  ] case class Mut[T @mutable]((t: T @mutable) @var)
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] Symbols after ImperativeCodeElimination
[info] [ Debug  ] 
[info] [ Debug  ] -------------Functions-------------
[info] [ Debug  ] def change_thing[T @mutable](thing: Mut[Thing[T @mutable]], t: T @mutable): (Unit, Mut[Thing[T @mutable]]) = {
[info] [ Debug  ]   val thing: Mut[Thing[T @mutable]] = thing
[info] [ Debug  ]   val thing: Mut[Thing[T @mutable]] = Mut[Thing[T @mutable]](Thing[T @mutable](t))
[info] [ Debug  ]   val tmp: Unit = ()
[info] [ Debug  ]   ((), thing)
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] def main: Unit = {
[info] [ Debug  ]   val thing: Thing[Int] = Thing[Int](123)
[info] [ Debug  ]   val res: (Unit, Mut[Thing[Int]]) = change_thing[Int](Mut[Thing[Int]](thing), 456)
[info] [ Debug  ]   val t: (Unit, Thing[Int]) = if (res._2.isInstanceOf[Mut[Thing[Int]]]) {
[info] [ Debug  ]     val thing: Thing[Int] = @unchecked @unchecked res._2.asInstanceOf[Mut[Thing[Int]]].t.asInstanceOf[Thing[Int]]
[info] [ Debug  ]     ((), thing)
[info] [ Debug  ]   } else {
[info] [ Debug  ]     ((), thing)
[info] [ Debug  ]   }
[info] [ Debug  ]   val res: Unit = t._1
[info] [ Debug  ]   val thing: Thing[Int] = t._2
[info] [ Debug  ]   val tmp: Unit = res
[info] [ Debug  ]   val tmp: Unit = res._1
[info] [ Debug  ]   assert(thing.field == 456)
[info] [ Debug  ]   val thing2: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   val res: (Unit, Mut[Thing[Int]]) = change_thing[Int](thing2, 789)
[info] [ Debug  ]   val t: (Unit, Mut[Thing[Int]]) = if (res._2.isInstanceOf[Mut[Thing[Int]]]) {
[info] [ Debug  ]     val thing2: Mut[Thing[Int]] = @unchecked Mut[Thing[Int]](@unchecked res._2.asInstanceOf[Mut[Thing[Int]]].t).asInstanceOf[Mut[Thing[Int]]]
[info] [ Debug  ]     ((), thing2)
[info] [ Debug  ]   } else {
[info] [ Debug  ]     ((), thing2)
[info] [ Debug  ]   }
[info] [ Debug  ]   val res: Unit = t._1
[info] [ Debug  ]   val thing2: Mut[Thing[Int]] = t._2
[info] [ Debug  ]   val tmp: Unit = res
[info] [ Debug  ]   val tmp: Unit = res._1
[info] [ Debug  ]   assert(thing.field == 789)
[info] [ Debug  ]   val thing3: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   val thing3: Mut[Thing[Int]] = Mut[Thing[Int]](Thing[Int](0))
[info] [ Debug  ]   val tmp: Unit = ()
[info] [ Debug  ]   val tmp: Unit = ()
[info] [ Debug  ]   assert(thing.field == 0)
[info] [ Debug  ]   ()
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] -------------Classes-------------
[info] [ Debug  ] case class Thing[T @mutable]((field: T @mutable) @var)
[info] [ Debug  ] 
[info] [ Debug  ] case class Mut[T @mutable]((t: T @mutable) @var)
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] Ensuring well-formedness after phase ImperativeCodeElimination...
[info] [ Debug  ] => SUCCESS
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] Symbols before ImperativeCleanup
[info] [ Debug  ] 
[info] [ Debug  ] -------------Functions-------------
[info] [ Debug  ] def change_thing[T @mutable](thing: Mut[Thing[T @mutable]], t: T @mutable): (Unit, Mut[Thing[T @mutable]]) = {
[info] [ Debug  ]   val thing: Mut[Thing[T @mutable]] = thing
[info] [ Debug  ]   val thing: Mut[Thing[T @mutable]] = Mut[Thing[T @mutable]](Thing[T @mutable](t))
[info] [ Debug  ]   val tmp: Unit = ()
[info] [ Debug  ]   ((), thing)
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] def main: Unit = {
[info] [ Debug  ]   val thing: Thing[Int] = Thing[Int](123)
[info] [ Debug  ]   val res: (Unit, Mut[Thing[Int]]) = change_thing[Int](Mut[Thing[Int]](thing), 456)
[info] [ Debug  ]   val t: (Unit, Thing[Int]) = if (res._2.isInstanceOf[Mut[Thing[Int]]]) {
[info] [ Debug  ]     val thing: Thing[Int] = @unchecked @unchecked res._2.asInstanceOf[Mut[Thing[Int]]].t.asInstanceOf[Thing[Int]]
[info] [ Debug  ]     ((), thing)
[info] [ Debug  ]   } else {
[info] [ Debug  ]     ((), thing)
[info] [ Debug  ]   }
[info] [ Debug  ]   val res: Unit = t._1
[info] [ Debug  ]   val thing: Thing[Int] = t._2
[info] [ Debug  ]   val tmp: Unit = res
[info] [ Debug  ]   val tmp: Unit = res._1
[info] [ Debug  ]   assert(thing.field == 456)
[info] [ Debug  ]   val thing2: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   val res: (Unit, Mut[Thing[Int]]) = change_thing[Int](thing2, 789)
[info] [ Debug  ]   val t: (Unit, Mut[Thing[Int]]) = if (res._2.isInstanceOf[Mut[Thing[Int]]]) {
[info] [ Debug  ]     val thing2: Mut[Thing[Int]] = @unchecked Mut[Thing[Int]](@unchecked res._2.asInstanceOf[Mut[Thing[Int]]].t).asInstanceOf[Mut[Thing[Int]]]
[info] [ Debug  ]     ((), thing2)
[info] [ Debug  ]   } else {
[info] [ Debug  ]     ((), thing2)
[info] [ Debug  ]   }
[info] [ Debug  ]   val res: Unit = t._1
[info] [ Debug  ]   val thing2: Mut[Thing[Int]] = t._2
[info] [ Debug  ]   val tmp: Unit = res
[info] [ Debug  ]   val tmp: Unit = res._1
[info] [ Debug  ]   assert(thing.field == 789)
[info] [ Debug  ]   val thing3: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   val thing3: Mut[Thing[Int]] = Mut[Thing[Int]](Thing[Int](0))
[info] [ Debug  ]   val tmp: Unit = ()
[info] [ Debug  ]   val tmp: Unit = ()
[info] [ Debug  ]   assert(thing.field == 0)
[info] [ Debug  ]   ()
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] -------------Classes-------------
[info] [ Debug  ] case class Thing[T @mutable]((field: T @mutable) @var)
[info] [ Debug  ] 
[info] [ Debug  ] case class Mut[T @mutable]((t: T @mutable) @var)
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] 
[info] [ Debug  ] Symbols after ImperativeCleanup
[info] [ Debug  ] 
[info] [ Debug  ] -------------Functions-------------
[info] [ Debug  ] def change_thing[T](thing: Mut[Thing[T]], t: T): (Unit, Mut[Thing[T]]) = {
[info] [ Debug  ]   val thing: Mut[Thing[T]] = thing
[info] [ Debug  ]   val thing: Mut[Thing[T]] = Mut[Thing[T]](Thing[T](t))
[info] [ Debug  ]   val tmp: Unit = ()
[info] [ Debug  ]   ((), thing)
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] def main: Unit = {
[info] [ Debug  ]   val thing: Thing[Int] = Thing[Int](123)
[info] [ Debug  ]   val res: (Unit, Mut[Thing[Int]]) = change_thing[Int](Mut[Thing[Int]](thing), 456)
[info] [ Debug  ]   val t: (Unit, Thing[Int]) = if (res._2.isInstanceOf[Mut[Thing[Int]]]) {
[info] [ Debug  ]     val thing: Thing[Int] = @unchecked @unchecked res._2.asInstanceOf[Mut[Thing[Int]]].t.asInstanceOf[Thing[Int]]
[info] [ Debug  ]     ((), thing)
[info] [ Debug  ]   } else {
[info] [ Debug  ]     ((), thing)
[info] [ Debug  ]   }
[info] [ Debug  ]   val res: Unit = t._1
[info] [ Debug  ]   val thing: Thing[Int] = t._2
[info] [ Debug  ]   val tmp: Unit = res
[info] [ Debug  ]   val tmp: Unit = res._1
[info] [ Debug  ]   assert(thing.field == 456)
[info] [ Debug  ]   val thing2: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   val res: (Unit, Mut[Thing[Int]]) = change_thing[Int](thing2, 789)
[info] [ Debug  ]   val t: (Unit, Mut[Thing[Int]]) = if (res._2.isInstanceOf[Mut[Thing[Int]]]) {
[info] [ Debug  ]     val thing2: Mut[Thing[Int]] = @unchecked Mut[Thing[Int]](@unchecked res._2.asInstanceOf[Mut[Thing[Int]]].t).asInstanceOf[Mut[Thing[Int]]]
[info] [ Debug  ]     ((), thing2)
[info] [ Debug  ]   } else {
[info] [ Debug  ]     ((), thing2)
[info] [ Debug  ]   }
[info] [ Debug  ]   val res: Unit = t._1
[info] [ Debug  ]   val thing2: Mut[Thing[Int]] = t._2
[info] [ Debug  ]   val tmp: Unit = res
[info] [ Debug  ]   val tmp: Unit = res._1
[info] [ Debug  ]   assert(thing.field == 789)
[info] [ Debug  ]   val thing3: Mut[Thing[Int]] = Mut[Thing[Int]](thing)
[info] [ Debug  ]   val thing3: Mut[Thing[Int]] = Mut[Thing[Int]](Thing[Int](0))
[info] [ Debug  ]   val tmp: Unit = ()
[info] [ Debug  ]   val tmp: Unit = ()
[info] [ Debug  ]   assert(thing.field == 0)
[info] [ Debug  ]   ()
[info] [ Debug  ] }
[info] [ Debug  ] 
[info] [ Debug  ] -------------Classes-------------
[info] [ Debug  ] case class Thing[T](field: T)
[info] [ Debug  ] 
[info] [ Debug  ] case class Mut[T](t: T)

About this issue

Original URL
State: closed
Created 3 years ago
Comments: 20 (6 by maintainers)

Commits related to this issue

Add more examples corresponding to issue #1090 about effects and aliasing — committed to jad-hamza/stainless by jad-hamza 3 years ago
Add more examples corresponding to issue #1090 about effects and aliasing — committed to jad-hamza/stainless by jad-hamza 3 years ago
Add more examples corresponding to issue #1090 about effects and aliasing — committed to jad-hamza/stainless by jad-hamza 3 years ago
Add more examples corresponding to issue #1090 about effects and aliasing — committed to epfl-lara/stainless by jad-hamza 3 years ago
Update Rust interop from master (#1107) * Duplicate frontends/benchmarks/imperative/invalid/ContainerTest.scala history in frontends/benchmarks/extraction/invalid/ history. * More traversal to che... — committed to epfl-lara/stainless by yannbolliger 3 years ago

Most upvoted comments

jad-hamza on Jun 7, 2021