Assertion error when using var with Map.updated

[EmmeliBlomkvist]

Stainless (version 0ae6a9d) crashes when running

import stainless.lang._
import stainless.collection._

def foo(): Unit = {
  var i = 0
  Map[Int, BigInt]().updated(i, BigInt(0))
}

Stack trace:

java.lang.AssertionError: assertion failed: i is not referentially transparent
	at scala.runtime.Scala3RunTime$.assertFailed(Scala3RunTime.scala:8)
	at stainless.extraction.imperative.AntiAliasing$TransformerImpl$1.assertReferentiallyTransparent(AntiAliasing.scala:1053)
	at stainless.extraction.imperative.AntiAliasing$TransformerImpl$1.transform(AntiAliasing.scala:998)
	at stainless.extraction.imperative.AntiAliasing$TransformerImpl$1.transform$$anonfun$11(AntiAliasing.scala:1002)
	at scala.collection.immutable.List.map(List.scala:247)
	at scala.collection.immutable.List.map(List.scala:79)
	at stainless.extraction.imperative.AntiAliasing$TransformerImpl$1.transform(AntiAliasing.scala:1002)
	at stainless.extraction.imperative.AntiAliasing$TransformerImpl$1.transform$$anonfun$11(AntiAliasing.scala:1002)
	at scala.collection.immutable.List.map(List.scala:251)
	at scala.collection.immutable.List.map(List.scala:79)
	at stainless.extraction.imperative.AntiAliasing$TransformerImpl$1.transform(AntiAliasing.scala:1002)
	at stainless.extraction.imperative.AntiAliasing.makeSideEffectsExplicit$1(AntiAliasing.scala:1067)
	at stainless.extraction.imperative.AntiAliasing.stainless$extraction$imperative$AntiAliasing$$_$updateFunction$1(AntiAliasing.scala:130)
	at stainless.extraction.imperative.AntiAliasing.extractFunction(AntiAliasing.scala:1684)
	at stainless.extraction.imperative.AntiAliasing.extractFunction(AntiAliasing.scala:89)
	at stainless.extraction.CachingPhase.$anonfun$1$$anonfun$1(ExtractionPipeline.scala:133)
	at stainless.extraction.utils.ConcurrentCache.cached(ConcurrentCaches.scala:26)
	at stainless.extraction.ExtractionCaches$ExtractionCache.cached(ExtractionCaches.scala:165)
	at stainless.extraction.CachingPhase.$anonfun$1(ExtractionPipeline.scala:133)
	at scala.collection.Iterator$$anon$9.next(Iterator.scala:584)
	at scala.collection.immutable.List.prependedAll(List.scala:153)
	at scala.collection.immutable.List$.from(List.scala:685)
	at scala.collection.immutable.List$.from(List.scala:682)
	at scala.collection.IterableFactory$Delegate.from(Factory.scala:288)
	at scala.collection.immutable.Iterable$.from(Iterable.scala:35)
	at scala.collection.immutable.Iterable$.from(Iterable.scala:32)
	at scala.collection.IterableFactory$Delegate.from(Factory.scala:288)
	at scala.collection.IterableOps.map(Iterable.scala:684)
	at scala.collection.IterableOps.map$(Iterable.scala:684)
	at scala.collection.AbstractIterable.map(Iterable.scala:935)
	at stainless.extraction.CachingPhase.extractSymbols(ExtractionPipeline.scala:132)
	at stainless.extraction.CachingPhase.extractSymbols$(ExtractionPipeline.scala:105)
	at stainless.extraction.imperative.AntiAliasing.stainless$extraction$oo$CachingPhase$$super$extractSymbols(AntiAliasing.scala:11)
	at stainless.extraction.imperative.AntiAliasing.stainless$extraction$oo$CachingPhase$$super$extractSymbols(AntiAliasing.scala:11)
	at stainless.extraction.oo.CachingPhase.extractSymbols(ExtractionPipeline.scala:36)
	at stainless.extraction.oo.CachingPhase.extractSymbols$(ExtractionPipeline.scala:13)
	at stainless.extraction.imperative.AntiAliasing.extractSymbols(AntiAliasing.scala:11)
	at stainless.extraction.imperative.AntiAliasing.extractSymbols(AntiAliasing.scala:11)
	at stainless.extraction.CachingPhase.extract(ExtractionPipeline.scala:126)
	at stainless.extraction.CachingPhase.extract$(ExtractionPipeline.scala:105)
	at stainless.extraction.imperative.AntiAliasing.extract(AntiAliasing.scala:11)
	at stainless.extraction.utils.NamedPipeline.extract$$anonfun$1$$anonfun$1(NamedPipeline.scala:141)
	at scala.util.Try$.apply(Try.scala:217)
	at inox.utils.TimerStorage.runAndGetTime(Timer.scala:84)
	at inox.utils.TimerStorage.run(Timer.scala:78)
	at stainless.extraction.utils.NamedPipeline.extract$$anonfun$1(NamedPipeline.scala:141)
	at stainless.extraction.utils.DebugSymbols.debug(NamedPipeline.scala:64)
	at stainless.extraction.utils.DebugSymbols.debug$(NamedPipeline.scala:29)
	at stainless.extraction.utils.NamedPipeline.debug(NamedPipeline.scala:127)
	at stainless.extraction.utils.NamedPipeline.extract(NamedPipeline.scala:142)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:48)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:48)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.ComponentRun.extract(Component.scala:75)
	at stainless.ComponentRun.extract$(Component.scala:35)
	at stainless.verification.VerificationRun.extract(VerificationComponent.scala:48)
	at stainless.ComponentRun.apply(Component.scala:85)
	at stainless.ComponentRun.apply$(Component.scala:35)
	at stainless.verification.VerificationRun.apply(VerificationComponent.scala:48)
	at stainless.frontend.SplitCallBack.$anonfun$10(SplitCallBack.scala:199)
	at scala.collection.immutable.List.map(List.scala:247)
	at scala.collection.immutable.List.map(List.scala:79)
	at stainless.frontend.SplitCallBack.processFunctionsSymbols(SplitCallBack.scala:198)
	at stainless.frontend.SplitCallBack.$anonfun$9(SplitCallBack.scala:172)
	at stainless.extraction.utils.ConcurrentCache.getOrElseUpdate(ConcurrentCaches.scala:15)
	at stainless.frontend.SplitCallBack.processFunctions(SplitCallBack.scala:172)
	at stainless.frontend.SplitCallBack.processSymbols(SplitCallBack.scala:158)
	at stainless.frontend.SplitCallBack.endExtractions(SplitCallBack.scala:80)
	at stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:36)
	at java.base/java.lang.Thread.run(Thread.java:840)

[vkuncak]

@EmmeliBlomkvist this is indeed unfortunate and would be good to fix, but you can work around it always by introducing a local val, right?

import stainless.lang.*
import stainless.collection.*

def foo(): Unit =
  var i = 0
  val i1 = i
  Map[Int, BigInt]().updated(i1, BigInt(0))

[EmmeliBlomkvist]

@vkuncak Yes, that works!