AntiAliasing: restore var binding in mapApplication

.larabot.conf

@@ -1,6 +1,6 @@
 commands = [
     "sbt -batch -Dtestsuite-parallelism=5 test"
-    "sbt -batch -Dtestsuite-parallelism=3 -Dtestcase-parallelism=5 \"stainless-dotty / IntegrationTest / testOnly stainless.GhostRewriteSuite stainless.GenCSuite stainless.LibrarySuite stainless.verification.VerificationSuite stainless.verification.UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.termination.TerminationSuite stainless.evaluators.EvaluatorComponentTest\""
+    "sbt -batch -Dtestsuite-parallelism=3 -Dtestcase-parallelism=5 \"stainless-dotty / IntegrationTest / testOnly stainless.DottyExtractionSuite stainless.GhostRewriteSuite stainless.GenCSuite stainless.LibrarySuite stainless.verification.VerificationSuite stainless.verification.UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.termination.TerminationSuite stainless.evaluators.EvaluatorComponentTest\""
 ]
 
 nightly {

core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala

@@ -256,6 +256,17 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
         }
 
         // NOTE: `args` must refer to the arguments of the function invocation before transformation (the original args)
+        // IMPORTANT NOTICE:
+        // In the `Let` case transformation of `transform`, we need to compute the targets of the transformed binding.
+        // If this binding happens to contain a function call, the returned targets may be invalid because
+        // `getTargets` works on functions prior to the AntiAliasing function purification, not after (as it's done it this `Let` case).
+        //
+        // It turns out that if we bind the result of the function call to a `var` (for mutable type) the target computation
+        // will fail which will result in rejection (with the message "Unsupported `val` definition in AntiAliasing").
+        // Not doing so will very likely result in a crash later on in unrelated part of the code (due to invalid targets being applied).
+        //
+        // To properly fix this, we would need to distinguish pre/post transformation `getTargets` computation,
+        // which would require significant changes to EffectsAnalyzer.
         def mapApplication(formalArgs: Seq[ValDef], args: Seq[Expr], nfi: Expr, nfiType: Type, fiEffects: Set[Effect], isOpaqueOrExtern: Boolean, env: Env): Expr = {
 
           def affectedBindings(updTarget: Target, isReplacement: Boolean): Map[ValDef, Set[Target]] = {
@@ -436,7 +447,15 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
             }
 
             val extractResults = Block(assgns, TupleSelect(freshRes.toVariable, 1))
-            Let(freshRes, nfi, extractResults)
+            // FIXME: This should be `Let` and not `LetVar`, however doing so will cause a crash in e.g. `MapAliasing1`
+            //  because `getAllTargetsDealiased` in the `Let` case will result in an invalid target due to
+            //  this function not supporting targets computation on function application *post-transformation*
+            // (see important notice on above).
+            if (isMutableType(nfiType)) {
+              LetVar(freshRes, nfi, extractResults)
+            } else {
+              Let(freshRes, nfi, extractResults)
+            }
           } else {
             nfi
           }