diff --git a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala
index 7107b71cc..d0c915851 100644
--- a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala
+++ b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala
@@ -525,99 +525,122 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
 
             val newExpr = transform(e, env)
             val targets = getAllTargetsDealiased(newExpr, env)
+            targets match {
+              case Some(targets) =>
+                // This branch handles all cases when targets can be precisely computed, namely when
+                // 1. newExpr is a fresh expression
+                // 2. newExpr is a precise alias to existing variable(s)
+                // 3. A combination of 1. and 2. (e.g. val y = if (cond) x else Ref(123))
+
+                // Targets with a false condition are those that are never accessed, we can remove them.
+                val targs = targets.filterNot(_.condition == Some(BooleanLiteral(false)))
+                // If there are more than one target, then it must be the case that their conditions are all disjoint,
+                // due to the way they are computed by `getTargets`.
+                // (here, we use a weaker prop. that asserts that all their condition are defined, for sanity checks)
+                assert(targs.size <= 1 || targs.forall(_.condition.isDefined))
+
+                // extraTarget: whether we should treat `vd` as a new target or not.
+                val extraTarget = {
+                  if (targs.isEmpty) {
+                    // newExpr is a fresh expression (case 1), so `vd` is introducing a new target.
+                    Seq(Target(vd.toVariable, None, Path.empty))
+                  } else if (targs.size == 1 && targs.head.condition.isEmpty) {
+                    // newExpr is a precise and unconditional alias to an existing variable - no new targets (case 2).
+                    Seq.empty[Target]
+                  } else {
+                    // Here, we have >= 1 targets and all of them are conditional:
+                    //   cond1 -> target1
+                    //   ...
+                    //   condn -> targetn
+                    // If cond1 && ... && condn provably cover all possible cases, then we know that `newExpr` is
+                    // a precise alias to n existing variables, so there are no new targets to consider (case 2).
+                    // Otherwise, it may be the case that `newExpr` refer to fresh expression and alias existing variables (case 3),
+                    // such as in the following example:
+                    //   val y = if (cond1) x else Ref(123)
+                    // Here, the targets of `y` would be the targets of x, with condition cond1.
+                    // But it also conditionally introduce a new target, namely Ref(123) when !cond1.
+                    // In such case, we introduce `y` as a new target, with condition !cond1.
+                    assert(targs.forall(_.condition.isDefined))
+                    val disj = simplifyOr(targs.map(_.condition.get).toSeq)
+                    val negatedConds = simpleNot(disj)
+                    if (negatedConds == BooleanLiteral(false)) Seq.empty[Target]
+                    else Seq(Target(vd.toVariable, Some(negatedConds), Path.empty))
+                  }
+                }
 
-            if (targets.isDefined) {
-              // This branch handles all cases when targets can be precisely computed, namely when
-              // 1. newExpr is a fresh expression
-              // 2. newExpr is a precise alias to existing variable(s)
-              // 3. A combination of 1. and 2. (e.g. val y = if (cond) x else Ref(123))
-
-              // Targets with a false condition are those that are never accessed, we can remove them.
-              val targs = targets.get.filterNot(_.condition == Some(BooleanLiteral(false)))
-              // If there are more than one target, then it must be the case that their conditions are all disjoint,
-              // due to the way they are computed by `getTargets`.
-              // (here, we use a weaker prop. that asserts that all their condition are defined, for sanity checks)
-              assert(targs.size <= 1 || targs.forall(_.condition.isDefined))
-
-              // extraTarget: whether we should treat `vd` as a new target or not.
-              val extraTarget = {
-                if (targs.isEmpty) {
-                  // newExpr is a fresh expression (case 1), so `vd` is introducing a new target.
-                  Seq(Target(vd.toVariable, None, Path.empty))
-                } else if (targs.size == 1 && targs.head.condition.isEmpty) {
-                  // newExpr is a precise and unconditional alias to an existing variable - no new targets (case 2).
-                  Seq.empty[Target]
+                val newBody = transform(b, env.withTargets(vd, targs ++ extraTarget).withBinding(vd))
+                // Note: even though there are no effects on `vd`, we still need to re-assign it
+                // in case it aliases a target that gets updated.
+                // As such, we use appearsInAssignment (on the transformed body) instead of checking for effects (on the original body)
+                val canLetVal = !appearsInAssignment(vd.toVariable, newBody)
+                if (canLetVal) Let(vd, newExpr, newBody).copiedFrom(l)
+                else LetVar(vd, newExpr, newBody).copiedFrom(l)
+              case None =>
+                // In this scenario, where we cannot precisely compute the targets of `e`, we can observe that
+                // if the (dealiased) variables appearing in `e` and those appearing in `b` (dealiased as well)
+                // are disjoint, then we can be sure that `b` will not *directly* modify the variables in `e`.
+                // On the other hand, `b` is of course allowed to modify `vd`, for which we must
+                // apply the effects afterwards (represented below as `copyEffects`).
+                //
+                // We can further refine this observation by noting that (dealised) variables in `e` *may* appear
+                // in `b` as well as long as they are not constituting the evaluation result of `e`, or in other
+                // terms, that they do not appear in a terminal position, which is recursively define as follows:
+                //   -Terminal of let v = e in b is the terminal in b
+                //   -Terminal of v is v itself
+                //   -Terminals of if (b) e1 else e2 is terminals of e1 and e2
+                //   -and so on
+                // Indeed, these occurrences will properly be updated by the recursive transformation.
+                // The test `imperative/valid/TargetMutation8` illustrates this refinement.
+                val eVars = terminalVarsOfExprDealiased(e, env)
+                val bVars = varsOfExprDealiased(b, env)
+                val commonMutable = (eVars & bVars).filter(v => isMutableType(v.tpe))
+                if (commonMutable.isEmpty) {
+                  // The above condition is similar to the one in EffectsChecker#check#traverser#traverse#Let, with the
+                  // difference that we also account for rewrites (which may introduce other variables, as in i1099.scala).
+                  val newBody = transform(b, env withBinding vd)
+
+                  // for all effects of `b` whose receiver is `vd`
+                  val copyEffects = effects(b).filter(_.receiver == vd.toVariable).flatMap { eff =>
+                    // we apply the effect on the bound expression (after transformation)
+                    eff.on(newExpr).map { case (eff2, cond2) => makeAssignment(l.getPos, eff.receiver, eff.path.path, eff2.toTarget(cond2)) }
+                  }
+                  val resVd = ValDef.fresh("res", b.getType).copiedFrom(b)
+
+                  // What we would like is the following:
+                  //   var vd = newExpr
+                  //   val resVd = newBody
+                  //   copyEffects // must happen after newBody and newExpr
+                  //   resVd
+                  // However, newBody may contain an `Ensuring` clause which would get "lost" in the newBody:
+                  //   var vd = newExpr
+                  //   val resVd = {
+                  //      newBody'
+                  //   }.ensuring(...) // oh no :(
+                  //   copyEffects
+                  //   resVd
+                  // What we would like is something as follows:
+                  //   var vd = newExpr
+                  //   {
+                  //      newBodyBlocks // e.g. assignments etc.
+                  //      val resVd = newBodyLastExpr
+                  //      copyEffect
+                  //      resVd
+                  //    }.ensuring(...)
+                  // To achieve this, we "drill" a hole in newBody using the normalizer object,
+                  // insert copyEffect and plug it with resVd. This should get us something like the above.
+                  val (newBodyCtx, newBodyLastExpr) = normalizer.drill(newBody)
+                  val (copyEffectCtx, copyEffectLastExpr) = normalizer.normalizeBlock(Block(copyEffects.toSeq, resVd.toVariable).copiedFrom(l))(using normalizer.BlockNorm.Standard)
+                  assert(copyEffectLastExpr == resVd.toVariable) // To be sure we are on the good track.
+                  val combined =
+                    newBodyCtx(let(resVd, newBodyLastExpr, copyEffectCtx(resVd.toVariable)))
+                  LetVar(vd, newExpr, combined).copiedFrom(l)
                 } else {
-                  // Here, we have >= 1 targets and all of them are conditional:
-                  //   cond1 -> target1
-                  //   ...
-                  //   condn -> targetn
-                  // If cond1 && ... && condn provably cover all possible cases, then we know that `newExpr` is
-                  // a precise alias to n existing variables, so there are no new targets to consider (case 2).
-                  // Otherwise, it may be the case that `newExpr` refer to fresh expression and alias existing variables (case 3),
-                  // such as in the following example:
-                  //   val y = if (cond1) x else Ref(123)
-                  // Here, the targets of `y` would be the targets of x, with condition cond1.
-                  // But it also conditionally introduce a new target, namely Ref(123) when !cond1.
-                  // In such case, we introduce `y` as a new target, with condition !cond1.
-                  assert(targs.forall(_.condition.isDefined))
-                  val disj = simplifyOr(targs.map(_.condition.get).toSeq)
-                  val negatedConds = simpleNot(disj)
-                  if (negatedConds == BooleanLiteral(false)) Seq.empty[Target]
-                  else Seq(Target(vd.toVariable, Some(negatedConds), Path.empty))
+                  val msg =
+                    s"""Unsupported `val` definition in AntiAliasing
+                       |The following variables of mutable types are shared between the binding and the body:
+                       |  ${commonMutable.toSeq.sortBy(_.id.name).map(v => s"${v.id}: ${v.tpe}").mkString(", ")}""".stripMargin
+                  throw MalformedStainlessCode(l, msg)
                 }
-              }
-
-              val newBody = transform(b, env.withTargets(vd, targs ++ extraTarget).withBinding(vd))
-              // Note: even though there are no effects on `vd`, we still need to re-assign it
-              // in case it aliases a target that gets updated.
-              // As such, we use appearsInAssignment (on the transformed body) instead of checking for effects (on the original body)
-              val canLetVal = !appearsInAssignment(vd.toVariable, newBody)
-              if (canLetVal) Let(vd, newExpr, newBody).copiedFrom(l)
-              else LetVar(vd, newExpr, newBody).copiedFrom(l)
-            } else if ((varsOfExprDealiased(e, env) & varsOfExprDealiased(b, env)).forall(v => !isMutableType(v.tpe))) {
-              // The above condition is similar to the one in EffectsChecker#check#traverser#traverse#Let, with the
-              // difference that we also account for rewrites (which may introduce other variables, as in i1099.scala).
-              val newBody = transform(b, env withBinding vd)
-
-              // for all effects of `b` whose receiver is `vd`
-              val copyEffects = effects(b).filter(_.receiver == vd.toVariable).flatMap { eff =>
-                // we apply the effect on the bound expression (after transformation)
-                eff.on(newExpr).map { case (eff2, cond2) => makeAssignment(l.getPos, eff.receiver, eff.path.path, eff2.toTarget(cond2)) }
-              }
-
-              val resVd = ValDef.fresh("res", b.getType).copiedFrom(b)
-
-              // What we would like is the following:
-              //   var vd = newExpr
-              //   val resVd = newBody
-              //   copyEffects // must happen after newBody and newExpr
-              //   resVd
-              // However, newBody may contain an `Ensuring` clause which would get "lost" in the newBody:
-              //   var vd = newExpr
-              //   val resVd = {
-              //      newBody'
-              //   }.ensuring(...) // oh no :(
-              //   copyEffects
-              //   resVd
-              // What we would like is something as follows:
-              //   var vd = newExpr
-              //   {
-              //      newBodyBlocks // e.g. assignments etc.
-              //      val resVd = newBodyLastExpr
-              //      copyEffect
-              //      resVd
-              //    }.ensuring(...)
-              // To achieve this, we "drill" a hole in newBody using the normalizer object,
-              // insert copyEffect and plug it with resVd. This should get us something like the above.
-              val (newBodyCtx, newBodyLastExpr) = normalizer.drill(newBody)
-              val (copyEffectCtx, copyEffectLastExpr) = normalizer.normalizeBlock(Block(copyEffects.toSeq, resVd.toVariable).copiedFrom(l))(using normalizer.BlockNorm.Standard)
-              assert(copyEffectLastExpr == resVd.toVariable) // To be sure we are on the good track.
-              val combined =
-                newBodyCtx(let(resVd, newBodyLastExpr, copyEffectCtx(resVd.toVariable)))
-              LetVar(vd, newExpr, combined).copiedFrom(l)
-            } else {
-              throw MalformedStainlessCode(l, "Unsupported `val` definition in AntiAliasing (couldn't compute targets and there are mutable variables shared between the binding and the body)")
             }
 
           case l @ LetVar(vd, e, b) if isMutableType(vd.tpe) =>
@@ -790,6 +813,44 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
           }
         }
 
+        def terminalVarsOfExprDealiased(expr: Expr, env: Env): Set[Variable] = {
+          // Like `varsOfExprDealiased` but takes into account local binding in `vars`
+          def varsOfExprDealiasedWithLocalBdgs(e: Expr, vars: Map[Variable, Set[Variable]]): Set[Variable] = {
+            for {
+              v <- exprOps.variablesOf(e)
+              v1 <- vars.getOrElse(v, Set(v))
+              v2 <- env.targets.get(v1.toVal).map(_.map(_.receiver)).getOrElse(Set(v1))
+            } yield v2
+          }
+          // Note: we do not have to worry about reassignment (via FieldAssignment, ArrayUpdate, etc.)
+          // because these must be fresh expressions and therefore cannot add further aliasing.
+          def go(e: Expr, vars: Map[Variable, Set[Variable]]): Set[Variable] = e match {
+            case Let(vd, df, body) =>
+              val dfTargets = getAllTargetsDealiased(df, env)
+              val dfVars = dfTargets match {
+                case Some(dfTargets) =>
+                  dfTargets.flatMap(t => vars.getOrElse(t.receiver, Set(t.receiver)))
+                case None => varsOfExprDealiasedWithLocalBdgs(df, vars)
+              }
+              go(body, vars + (vd.toVariable -> dfVars))
+            case LetVar(vd, _, body) =>
+              assert(!isMutableType(vd.tpe))
+              // No special handling is needed since `vd` is immutable
+              go(body, vars)
+            case Block(_, last) => go(last, vars)
+            case LetRec(_, body) => go(body, vars)
+            case Ensuring(body, _) => go(body, vars)
+            case Assert(_, _, body) => go(body, vars)
+            case Assume(_, body) => go(body, vars)
+            case Decreases(_, body) => go(body, vars)
+            case Require(_, body) => go(body, vars)
+            case IfExpr(_, thn, elze) => go(thn, vars) ++ go(elze, vars)
+            case MatchExpr(_, cases) => cases.flatMap(mc => go(mc.rhs, vars)).toSet
+            case _ => varsOfExprDealiasedWithLocalBdgs(e, vars)
+          }
+          go(expr, Map.empty)
+        }
+
         def assertReferentiallyTransparent(expr: Expr): Unit = {
           assert(isReferentiallyTransparent(expr), s"${expr.asString} is not referentially transparent")
         }
diff --git a/core/src/main/scala/stainless/extraction/innerfuns/Definitions.scala b/core/src/main/scala/stainless/extraction/innerfuns/Definitions.scala
index 2371e11ae..7ebfdb11d 100644
--- a/core/src/main/scala/stainless/extraction/innerfuns/Definitions.scala
+++ b/core/src/main/scala/stainless/extraction/innerfuns/Definitions.scala
@@ -101,7 +101,7 @@ trait Definitions extends extraction.Trees { self: Trees =>
     def unapply(i: Outer): Some[FunDef] = Some(i.fd)
   }
 
-  // We do not define Inner as a case class because the inherited `copy` method conflics with the compiler-generated one.
+  // We do not define Inner as a case class because the inherited `copy` method conflicts with the compiler-generated one.
   class Inner(val fd: LocalFunDef) extends FunAbstraction(
     fd.id, fd.tparams, fd.params, fd.returnType, fd.fullBody, fd.flags) {
     setPos(fd)
diff --git a/frontends/benchmarks/extraction/invalid/IllegalAliasing4.check b/frontends/benchmarks/extraction/invalid/IllegalAliasing4.check
new file mode 100644
index 000000000..88329b4d2
--- /dev/null
+++ b/frontends/benchmarks/extraction/invalid/IllegalAliasing4.check
@@ -0,0 +1,5 @@
+[ Error  ] IllegalAliasing4.scala:15:5: Unsupported `val` definition in AntiAliasing
+[ Error  ] The following variables of mutable types are shared between the binding and the body:
+[ Error  ]   counter: A
+               val b = {
+               ^^^^^^^^^...
\ No newline at end of file
diff --git a/frontends/benchmarks/extraction/invalid/IllegalAliasing4.scala b/frontends/benchmarks/extraction/invalid/IllegalAliasing4.scala
new file mode 100644
index 000000000..1c160f514
--- /dev/null
+++ b/frontends/benchmarks/extraction/invalid/IllegalAliasing4.scala
@@ -0,0 +1,26 @@
+object IllegalAliasing4 {
+
+  case class A(var i: BigInt)
+  case class B(a: A)
+  case class C(a: A, b: B)
+
+  def createA(i: BigInt, counter: A): A = {
+    counter.i += 1
+    A(i)
+  }
+
+  def test(n: BigInt, counter: A): Unit = {
+    val origCount = counter.i
+    val alias = counter
+    val b = {
+      if (n > 0) {
+        createA(n, alias)
+        B(alias)
+      }
+      else B(A(0))
+    }
+    b.a.i += 1
+    assert(n <= 0 || counter.i == origCount + 2)
+    assert(n > 0 || counter.i == origCount + 1)
+  }
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/extraction/invalid/Initialization1.scalac.check b/frontends/benchmarks/extraction/invalid/Initialization1.scalac.check
index b790f8f57..087185069 100644
--- a/frontends/benchmarks/extraction/invalid/Initialization1.scalac.check
+++ b/frontends/benchmarks/extraction/invalid/Initialization1.scalac.check
@@ -1,4 +1,5 @@
 [ Error  ] Initialization1.scala:3:5: Not well formed definition @private
+[ Error  ] @final
 [ Error  ] @field
 [ Error  ] @fieldDefPosition(1)
 [ Error  ] @method(InitA)
diff --git a/frontends/benchmarks/extraction/invalid/Initialization2.scalac.check b/frontends/benchmarks/extraction/invalid/Initialization2.scalac.check
index 53b434003..d98ba75dd 100644
--- a/frontends/benchmarks/extraction/invalid/Initialization2.scalac.check
+++ b/frontends/benchmarks/extraction/invalid/Initialization2.scalac.check
@@ -1,4 +1,5 @@
 [ Error  ] Initialization2.scala:3:5: Not well formed definition @private
+[ Error  ] @final
 [ Error  ] @field
 [ Error  ] @fieldDefPosition(1)
 [ Error  ] @method(Hello)
diff --git a/frontends/benchmarks/extraction/invalid/Initialization3.scalac.check b/frontends/benchmarks/extraction/invalid/Initialization3.scalac.check
index 474e579b7..17072d51a 100644
--- a/frontends/benchmarks/extraction/invalid/Initialization3.scalac.check
+++ b/frontends/benchmarks/extraction/invalid/Initialization3.scalac.check
@@ -1,4 +1,5 @@
 [ Error  ] Initialization3.scala:3:5: Not well formed definition @private
+[ Error  ] @final
 [ Error  ] @field
 [ Error  ] @fieldDefPosition(1)
 [ Error  ] @method(NoThis)
diff --git a/frontends/benchmarks/extraction/invalid/Initialization4.scalac.check b/frontends/benchmarks/extraction/invalid/Initialization4.scalac.check
index d8db39db0..829851277 100644
--- a/frontends/benchmarks/extraction/invalid/Initialization4.scalac.check
+++ b/frontends/benchmarks/extraction/invalid/Initialization4.scalac.check
@@ -1,4 +1,5 @@
 [ Error  ] Initialization4.scala:3:5: Not well formed definition @private
+[ Error  ] @final
 [ Error  ] @field
 [ Error  ] @fieldDefPosition(1)
 [ Error  ] @method(NoThis)
diff --git a/frontends/benchmarks/extraction/invalid/Initialization5.scalac.check b/frontends/benchmarks/extraction/invalid/Initialization5.scalac.check
index 8d8dea676..1e01a8627 100644
--- a/frontends/benchmarks/extraction/invalid/Initialization5.scalac.check
+++ b/frontends/benchmarks/extraction/invalid/Initialization5.scalac.check
@@ -1,4 +1,5 @@
 [ Error  ] Initialization5.scala:3:5: Not well formed definition @private
+[ Error  ] @final
 [ Error  ] @field
 [ Error  ] @fieldDefPosition(1)
 [ Error  ] @method(NoThis)
diff --git a/frontends/benchmarks/extraction/invalid/MapAliasing1.check b/frontends/benchmarks/extraction/invalid/MapAliasing1.check
index 662bdc005..962812b80 100644
--- a/frontends/benchmarks/extraction/invalid/MapAliasing1.check
+++ b/frontends/benchmarks/extraction/invalid/MapAliasing1.check
@@ -1,3 +1,5 @@
-[ Error  ] MapAliasing1.scala:17:5: Unsupported `val` definition in AntiAliasing (couldn't compute targets and there are mutable variables shared between the binding and the body)
+[ Error  ] MapAliasing1.scala:17:5: Unsupported `val` definition in AntiAliasing
+[ Error  ] The following variables of mutable types are shared between the binding and the body:
+[ Error  ]   m: MutableMap[BigInt,A]
                val a = f(m, 123)
                ^^^^^^^^^^^^^^^^^
\ No newline at end of file
diff --git a/frontends/benchmarks/extraction/invalid/MapAliasing2.check b/frontends/benchmarks/extraction/invalid/MapAliasing2.check
index 81ca98ec7..380c8f016 100644
--- a/frontends/benchmarks/extraction/invalid/MapAliasing2.check
+++ b/frontends/benchmarks/extraction/invalid/MapAliasing2.check
@@ -1,3 +1,5 @@
-[ Error  ] MapAliasing2.scala:15:5: Unsupported `val` definition in AntiAliasing (couldn't compute targets and there are mutable variables shared between the binding and the body)
+[ Error  ] MapAliasing2.scala:15:5: Unsupported `val` definition in AntiAliasing
+[ Error  ] The following variables of mutable types are shared between the binding and the body:
+[ Error  ]   m: MutableMap[BigInt,A]
                val a = f(m, 123)
                ^^^^^^^^^^^^^^^^^
\ No newline at end of file
diff --git a/frontends/benchmarks/extraction/invalid/i1099a.check b/frontends/benchmarks/extraction/invalid/i1099a.check
index a34ecd832..f78d308ca 100644
--- a/frontends/benchmarks/extraction/invalid/i1099a.check
+++ b/frontends/benchmarks/extraction/invalid/i1099a.check
@@ -1,3 +1,5 @@
-[ Error  ] i1099a.scala:9:5: Unsupported `val` definition in AntiAliasing (couldn't compute targets and there are mutable variables shared between the binding and the body)
+[ Error  ] i1099a.scala:9:5: Unsupported `val` definition in AntiAliasing
+[ Error  ] The following variables of mutable types are shared between the binding and the body:
+[ Error  ]   a1: A
                val c = C(a2)
                ^^^^^^^^^^^^^
\ No newline at end of file
diff --git a/frontends/benchmarks/extraction/invalid/i1099b.check b/frontends/benchmarks/extraction/invalid/i1099b.check
index 04cfc6c0c..48dae75bb 100644
--- a/frontends/benchmarks/extraction/invalid/i1099b.check
+++ b/frontends/benchmarks/extraction/invalid/i1099b.check
@@ -1,3 +1,5 @@
-[ Error  ] i1099b.scala:9:5: Unsupported `val` definition in AntiAliasing (couldn't compute targets and there are mutable variables shared between the binding and the body)
+[ Error  ] i1099b.scala:9:5: Unsupported `val` definition in AntiAliasing
+[ Error  ] The following variables of mutable types are shared between the binding and the body:
+[ Error  ]   a1: A
                val c = C(a2)
                ^^^^^^^^^^^^^
\ No newline at end of file
diff --git a/frontends/benchmarks/extraction/invalid/i1099c.check b/frontends/benchmarks/extraction/invalid/i1099c.check
index dae1cbc43..561113648 100644
--- a/frontends/benchmarks/extraction/invalid/i1099c.check
+++ b/frontends/benchmarks/extraction/invalid/i1099c.check
@@ -1,3 +1,5 @@
-[ Error  ] i1099c.scala:19:5: Unsupported `val` definition in AntiAliasing (couldn't compute targets and there are mutable variables shared between the binding and the body)
+[ Error  ] i1099c.scala:19:5: Unsupported `val` definition in AntiAliasing
+[ Error  ] The following variables of mutable types are shared between the binding and the body:
+[ Error  ]   a1: A
                val c = C(a3)
                ^^^^^^^^^^^^^
\ No newline at end of file
diff --git a/frontends/benchmarks/extraction/invalid/i1099d.check b/frontends/benchmarks/extraction/invalid/i1099d.check
new file mode 100644
index 000000000..6f67d2c24
--- /dev/null
+++ b/frontends/benchmarks/extraction/invalid/i1099d.check
@@ -0,0 +1,5 @@
+[ Error  ] i1099d.scala:9:5: Unsupported `val` definition in AntiAliasing
+[ Error  ] The following variables of mutable types are shared between the binding and the body:
+[ Error  ]   a0: A, a1: A
+               val c = C(a2)
+               ^^^^^^^^^^^^^
\ No newline at end of file
diff --git a/frontends/benchmarks/extraction/invalid/i1099d.scala b/frontends/benchmarks/extraction/invalid/i1099d.scala
new file mode 100644
index 000000000..deea7b157
--- /dev/null
+++ b/frontends/benchmarks/extraction/invalid/i1099d.scala
@@ -0,0 +1,14 @@
+object i1099d {
+  case class A(var x: Int)
+  case class C(a: A)
+
+  def f(a0: A, a1: A, cond: Boolean) = {
+    require(a0.x == 0 && a1.x == 1)
+    val a2 = if (cond) a0 else a1
+    // Illegal aliasing
+    val c = C(a2)
+    c.a.x += 1
+    val useA0 = a0
+    val useA1 = a1
+  }
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/imperative/valid/TargetMutation3.scala b/frontends/benchmarks/imperative/valid/TargetMutation3.scala
index 7e165ad17..eb9acb742 100644
--- a/frontends/benchmarks/imperative/valid/TargetMutation3.scala
+++ b/frontends/benchmarks/imperative/valid/TargetMutation3.scala
@@ -6,7 +6,7 @@ object TargetMutation3 {
   case class Box(var value: Int)
 
   def mutate(b: Box, v: Int): Unit = {
-    b.value = v;
+    b.value = v
   }
 
   def badManners(arr: Array[Box], otherArr: Array[Box], b1: Box, b2: Box, b3: Box, cond1: Boolean, cond2: Boolean, i: Int): Unit = {
diff --git a/frontends/benchmarks/imperative/valid/TargetMutation4.scala b/frontends/benchmarks/imperative/valid/TargetMutation4.scala
index 14b3b6023..d426878a0 100644
--- a/frontends/benchmarks/imperative/valid/TargetMutation4.scala
+++ b/frontends/benchmarks/imperative/valid/TargetMutation4.scala
@@ -7,7 +7,7 @@ object TargetMutation4 {
   case class Box(var value: Int)
 
   def mutate(b: Box, v: Int): Unit = {
-    b.value = v;
+    b.value = v
   }
 
   def h1(x: Box, cond: Boolean): Unit = {
diff --git a/frontends/benchmarks/imperative/valid/TargetMutation5.scala b/frontends/benchmarks/imperative/valid/TargetMutation5.scala
index 303c9f574..f7e3b6a29 100644
--- a/frontends/benchmarks/imperative/valid/TargetMutation5.scala
+++ b/frontends/benchmarks/imperative/valid/TargetMutation5.scala
@@ -6,12 +6,12 @@ object TargetMutation5 {
   case class Box(var value1: Int, var value2: Int, var value3: Int)
 
   def mutate(b: Box, v: Int): Unit = {
-    b.value1 = v;
+    b.value1 = v
   }
 
   def mmutate(b: Box, v1: Int, v2: Int): Unit = {
-    b.value1 = v1;
-    b.value2 = v2;
+    b.value1 = v1
+    b.value2 = v2
   }
 
   def t1(arr: Array[Box], i: Int): Unit = {
diff --git a/frontends/benchmarks/imperative/valid/TargetMutation6.scala b/frontends/benchmarks/imperative/valid/TargetMutation6.scala
index 1d856ac07..c35331687 100644
--- a/frontends/benchmarks/imperative/valid/TargetMutation6.scala
+++ b/frontends/benchmarks/imperative/valid/TargetMutation6.scala
@@ -6,7 +6,7 @@ object TargetMutation6 {
   case class RefRef(var lhs: Ref, var rhs: Ref)
 
   def replaceLhs(rr: RefRef, v: Int): Unit = {
-    rr.lhs = Ref(v);
+    rr.lhs = Ref(v)
   }
 
   def t1(arr1: Array[Ref], arr2: Array[Ref], i: Int, j: Int, k: Int, cond: Boolean, gra: Ref): Unit = {
diff --git a/frontends/benchmarks/imperative/valid/TargetMutation7.scala b/frontends/benchmarks/imperative/valid/TargetMutation7.scala
new file mode 100644
index 000000000..7933eacd2
--- /dev/null
+++ b/frontends/benchmarks/imperative/valid/TargetMutation7.scala
@@ -0,0 +1,70 @@
+object TargetMutation7 {
+
+  case class A(var i: BigInt)
+  case class B(var a1: A, var a2: A)
+  case class C(var a: A, var b: B)
+
+  def createA(i: BigInt, counter: A): A = {
+    counter.i += 1
+    A(i)
+  }
+
+  def test1(n: BigInt, counter: A): C = {
+    val origCount = counter.i
+    val a0 = A(1234)
+    val b = {
+      if (n > 0) {
+        val b = B(A(0), A(1))
+        b.a1 = createA(1, counter)
+        b
+      } else B(A(123), A(456))
+    }
+    val a = createA(2, counter)
+    assert(n <= 0 || counter.i == origCount + 2)
+    assert(n > 0 || counter.i == origCount + 1)
+    C(a, b)
+  }
+
+  def test2(n: BigInt, counter: A): Unit = {
+    val origCount = counter.i
+    val alias = counter
+    val b = {
+      if (n > 0) B(A(0), createA(n, alias))
+      else B(A(0), A(0))
+    }
+    b.a2.i += 1
+    assert(n <= 0 || counter.i == origCount + 1)
+    assert(n > 0 || counter.i == origCount)
+  }
+
+
+  def test3(n: BigInt, counter: A): Unit = {
+    val origCount = counter.i
+    val alias = counter
+    val b = {
+      if (n > 0) {
+        createA(n, alias)
+        B(A(0), alias)
+      }
+      else B(A(0), alias)
+    }
+    b.a2.i += 1
+    assert(n <= 0 || b.a2.i == origCount + 2)
+    assert(n > 0 || b.a2.i == origCount + 1)
+  }
+
+  def test4(n: BigInt, counter: A): Unit = {
+    val origCount = counter.i
+    val alias = counter
+    val b = {
+      if (n > 0) {
+        createA(n, alias)
+        B(A(0), counter)
+      }
+      else B(A(0), alias)
+    }
+    b.a2.i += 1
+    assert(n <= 0 || b.a2.i == origCount + 2)
+    assert(n > 0 || b.a2.i == origCount + 1)
+  }
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/imperative/valid/TargetMutation8.scala b/frontends/benchmarks/imperative/valid/TargetMutation8.scala
new file mode 100644
index 000000000..00e859cae
--- /dev/null
+++ b/frontends/benchmarks/imperative/valid/TargetMutation8.scala
@@ -0,0 +1,32 @@
+object TargetMutation8 {
+
+  case class A(var i: BigInt)
+  case class B(arr: Array[A])
+  case class C(a: A, b: B)
+
+  def createA(i: BigInt, counter: A): A = {
+    counter.i += 1
+    A(i)
+  }
+
+  def test(n: BigInt, counter: A): C = {
+    val origCount = counter.i
+    // This triggers AntiAliasing 2nd case for Let binding of mutable types
+    // *without* triggering EffectsChecker#check#traverser#traverse#Let
+    // because:
+    // -`b` is bound to a fresh expression (passes EffectsChecker#check#traverser#traverse#Let check)
+    // -the transformation of `b` produces an expression whose target cannot be computed
+    // -there are no sharing between the terminal variables of `b` and the rest of the body
+    val b = {
+      if (n > 0) {
+        val b = B(Array.fill(5)(A(0)))
+        b.arr(0) = createA(1, counter)
+        b
+      } else B(Array.fill(5)(A(0)))
+    }
+    val a = createA(2, counter)
+    assert(n <= 0 || counter.i == origCount + 2)
+    assert(n > 0 || counter.i == origCount + 1)
+    C(a, b)
+  }
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/imperative/valid/TargetMutation9.scala b/frontends/benchmarks/imperative/valid/TargetMutation9.scala
new file mode 100644
index 000000000..8f5565cde
--- /dev/null
+++ b/frontends/benchmarks/imperative/valid/TargetMutation9.scala
@@ -0,0 +1,58 @@
+object TargetMutation9 {
+
+  case class A(var x: BigInt)
+  case class C(a: A)
+  case class D(c: C)
+
+  def test1(n: BigInt): Unit = {
+    val a = A(n)
+    val c = C(a)
+    c.a.x = 3
+    assert(c.a.x == 3)
+  }
+
+  def test2(n: BigInt): Unit = {
+    val a = A(n)
+    if (n == 0) {
+      val c = C(a)
+      c.a.x = 3
+      // `a` will be updated here by AntiAliasing (`copyEffects`)
+    }
+    assert(n != 0 || a.x == 3)
+  }
+
+  def test3(n: BigInt): Unit = {
+    val a = A(n)
+    if (n == 0) {
+      val c = C(a)
+      val c2 = c
+      c2.a.x = 3
+      // `a` will be updated here by AntiAliasing (`copyEffects`)
+    }
+    assert(n != 0 || a.x == 3)
+  }
+
+  def test4(n: BigInt): Unit = {
+    val a = A(n)
+    if (n == 0) {
+      val c = C(a)
+      val d = D(c)
+      d.c.a.x = 3
+      // `a` will be updated here by AntiAliasing (`copyEffects`)
+    }
+    assert(n != 0 || a.x == 3)
+  }
+
+  def test5(n: BigInt): Unit = {
+    val a = A(n)
+    if (n == 0) {
+      val c = C(a)
+      val d = D(c)
+      d.c.a.x = 3
+      // `a` will be updated here by AntiAliasing (`copyEffects`)
+    }
+    a.x += 1
+    assert(n != 0 || a.x == 4)
+    assert(n == 0 || a.x == n + 1)
+  }
+}
\ No newline at end of file