diff --git a/build.sbt b/build.sbt
index 5c61eb89f7..c779bce6ad 100644
--- a/build.sbt
+++ b/build.sbt
@@ -225,7 +225,7 @@ val scriptSettings: Seq[Setting[_]] = Seq(
 def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
 
 // lazy val inox = RootProject(file("../inox"))
-lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "e477160170d83e6fa011dd3b413dab94a4918a1d")
+lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "2f66f5ab53f2ff63ef71bd67140b9532ee237e8b")
 //lazy val dotty = ghProject("git://github.com/lampepfl/dotty.git", "b3194406d8e1a28690faee12257b53f9dcf49506")
 
 // Allow integration test to use facilities from regular tests
diff --git a/core/src/main/scala/stainless/MainHelpers.scala b/core/src/main/scala/stainless/MainHelpers.scala
index d2ab62f967..885abdd8b0 100644
--- a/core/src/main/scala/stainless/MainHelpers.scala
+++ b/core/src/main/scala/stainless/MainHelpers.scala
@@ -218,7 +218,8 @@ trait MainHelpers extends inox.MainHelpers { self =>
           reporter.debug(e)(frontend.DebugSectionStack)
           reporter.error(e.getMessage)
       } finally {
-          compiler = newCompiler()
+        reporter.reset()
+        compiler = newCompiler()
       }
 
         if (isWatchModeOn(ctx)) {
diff --git a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala
index 64388e1538..75b8e47d38 100644
--- a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala
+++ b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala
@@ -280,8 +280,8 @@ trait AntiAliasing
             for (target1 <- targets1)
               for ((arg2, targets2) <- otherTargets)
                 for (target2 <- targets2)
-                  if (target1.prefixOf(target2) ||
-                      target2.prefixOf(target1))
+                  if (target1.maybePrefixOf(target2) ||
+                      target2.maybePrefixOf(target1))
                     throw MalformedStainlessCode(expr,
                       s"Illegal passing of aliased parameters ${arg1.asString} (with target: ${target1.asString}) " +
                       s"and ${arg2.asString} (with target: ${target2.asString})"
@@ -603,6 +603,9 @@ trait AntiAliasing
         case Target(receiver, None, path) =>
           rec(receiver, path.toSeq)
 
+        case Target(receiver, Some(condition), path) if effects(condition).nonEmpty =>
+          throw FatalError(s"Effects are not allowed in condition of effects: ${condition.asString}")
+
         case Target(receiver, Some(condition), path) =>
           Annotated(
             AsInstanceOf(
diff --git a/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala b/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala
index 66c0b659de..ab7ab47e5a 100644
--- a/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala
+++ b/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala
@@ -161,30 +161,37 @@ trait EffectsAnalyzer extends oo.CachingPhase {
 
   sealed abstract class Accessor {
     def asString(implicit ctx: inox.Context): String
+    def bind(x: ValDef, e: Expr): Accessor
   }
 
   case class ADTFieldAccessor(selector: Identifier) extends Accessor {
     def asString(implicit ctx: inox.Context) = s"ADTFieldAccessor(${selector.asString})"
+    def bind(x: ValDef, e: Expr): Accessor = this
   }
 
   case class ClassFieldAccessor(selector: Identifier) extends Accessor {
     def asString(implicit ctx: inox.Context) = s"ClassFieldAccessor(${selector.asString})"
+    def bind(x: ValDef, e: Expr): Accessor = this
   }
 
   case class ArrayAccessor(index: Expr) extends Accessor {
     def asString(implicit ctx: inox.Context) = s"ArrayAccessor(${index.asString})"
+    def bind(x: ValDef, e: Expr): Accessor = ArrayAccessor(bindNonValue(x, e, index))
   }
 
   case object UnknownArrayAccessor extends Accessor {
     def asString(implicit ctx: inox.Context) = s"UnknownArrayAccessor"
+    def bind(x: ValDef, e: Expr): Accessor = this
   }
 
   case class MutableMapAccessor(index: Expr) extends Accessor {
     def asString(implicit ctx: inox.Context) = s"MutableMapAccessor(${index.asString})"
+    def bind(x: ValDef, e: Expr): Accessor = ArrayAccessor(bindNonValue(x, e, index))
   }
 
   case class TupleFieldAccessor(index: Int) extends Accessor {
     def asString(implicit ctx: inox.Context) = s"TupleFieldAccessor($index)"
+    def bind(x: ValDef, e: Expr): Accessor = this
   }
 
   case class Path(path: Seq[Accessor]) {
@@ -197,7 +204,11 @@ trait EffectsAnalyzer extends oo.CachingPhase {
 
     def wrap(expr: Expr)(implicit symbols: Symbols) = Path.wrap(expr, path)
 
-    def prefixOf(that: Path): Boolean = {
+    def bind(x: ValDef, e: Expr) = Path(path.map(_.bind(x, e)))
+
+    // can return `true` even if `this` is not really a prefix of `that`
+    // (because of array and mutable map accessors)
+    def maybePrefixOf(that: Path): Boolean = {
       // TODO: more expressions can be added to be "provably different"
       def provablyDifferent(index1: Expr, index2: Expr): Boolean = (index1, index2) match {
         case (x1: Variable, Plus(x2: Variable, BVLiteral(_, _, size)))
@@ -227,6 +238,26 @@ trait EffectsAnalyzer extends oo.CachingPhase {
       rec(path, that.path)
     }
 
+    // can return `false` even if `this` is a prefix of `that`
+    def definitelyPrefixOf(that: Path): Boolean = {
+      def rec(p1: Seq[Accessor], p2: Seq[Accessor]): Boolean = (p1, p2) match {
+        case (Seq(), _) => true
+        case (ArrayAccessor(index1) +: xs1, ArrayAccessor(index2) +: xs2) if index1 == index2 =>
+          rec(xs1, xs2)
+        case (ADTFieldAccessor(id1) +: xs1, ADTFieldAccessor(id2) +: xs2) if id1 == id2 =>
+          rec(xs1, xs2)
+        case (ClassFieldAccessor(id1) +: xs1, ClassFieldAccessor(id2) +: xs2) if id1 == id2 =>
+          rec(xs1, xs2)
+        case (TupleFieldAccessor(id1) +: xs1, TupleFieldAccessor(id2) +: xs2) if id1 == id2 =>
+          rec(xs1, xs2)
+        case (MutableMapAccessor(k1) +: xs1, MutableMapAccessor(k2) +: xs2) if k1 == k2 =>
+          rec(xs1, xs2)
+        case _ => false
+      }
+
+      rec(path, that.path)
+    }
+
     def toSeq: Seq[Accessor] = path
 
     def asString(implicit printerOpts: PrinterOptions): String =
@@ -277,9 +308,29 @@ trait EffectsAnalyzer extends oo.CachingPhase {
 
   }
 
+  // values that do not need binding
+  private def isValue(e: Expr): Boolean = e match {
+    case _: Variable => true
+    case UnitLiteral() => true
+    case BooleanLiteral(_) => true
+    case IntegerLiteral(_) => true
+    case BVLiteral(_, _, _) => true
+    case Tuple(es) => es.forall(isValue)
+    case ADT(_, _, args) => args.forall(isValue)
+    case _ => false
+  }
+
+  def bindNonValue(x: ValDef, e: Expr, body: Expr): Expr = {
+    if (isValue(e)) exprOps.replaceFromSymbols(Map(x -> e), body)
+    else if (exprOps.variablesOf(body).contains(x.toVariable)) Let(x, e, body)
+    else body
+  }
+
   case class Target(receiver: Variable, condition: Option[Expr], path: Path) {
     def +(elem: Accessor): Target = Target(receiver, condition, path :+ elem)
 
+    def bind(x: ValDef, e: Expr) = Target(receiver, condition.map(cond => bindNonValue(x, e, cond)), path.bind(x, e))
+
     def append(that: Target): Target = (condition, that.condition) match {
       case (condition, None) =>
         Target(receiver, condition, path ++ that.path)
@@ -298,8 +349,11 @@ trait EffectsAnalyzer extends oo.CachingPhase {
       case CombinedKind => CombinedEffect(receiver, path)
     }
 
-    def prefixOf(that: Target): Boolean =
-      receiver == that.receiver && (path prefixOf that.path)
+    def maybePrefixOf(that: Target): Boolean =
+      receiver == that.receiver && (path maybePrefixOf that.path)
+
+    def definitelyPrefixOf(that: Target): Boolean =
+      receiver == that.receiver && (path definitelyPrefixOf that.path)
 
     def wrap(implicit symbols: Symbols): Option[Expr] = path.wrap(receiver)
 
@@ -387,8 +441,11 @@ trait EffectsAnalyzer extends oo.CachingPhase {
       res
     }
 
-    def prefixOf(that: Effect): Boolean =
-      receiver == that.receiver && (path prefixOf that.path)
+    def maybePrefixOf(that: Effect): Boolean =
+      receiver == that.receiver && (path maybePrefixOf that.path)
+
+    def definitelyPrefixOf(that: Effect): Boolean =
+      receiver == that.receiver && (path definitelyPrefixOf that.path)
 
     def toTarget: Target = Target(receiver, None, path)
 
@@ -490,18 +547,17 @@ trait EffectsAnalyzer extends oo.CachingPhase {
         And(cnd, e.setPos(cnd)).setPos(cnd)
       } getOrElse(cnd)
 
-      for {
-        t <- getTargets(thn, kind, path)
-        e <- getTargets(els, kind, path)
-        target <- Set(
-          Target(t.receiver, Some(conj(cnd, t.condition)), t.path),
-          Target(e.receiver, Some(notConj(cnd, e.condition)), e.path)
-        ) if target.isValid
-      } yield target
+      getTargets(thn, kind, path).map { t =>
+        Target(t.receiver, Some(conj(cnd, t.condition)),  t.path)
+      }.filter(_.isValid) ++
+      getTargets(els, kind, path).map { t =>
+        Target(t.receiver, Some(notConj(cnd, t.condition)),  t.path)
+      }.filter(_.isValid)
 
     case fi: FunctionInvocation if !symbols.isRecursive(fi.id) =>
-      BodyWithSpecs(symbols.simplifyLets(fi.inlined))
-        .bodyOpt
+      val specced = BodyWithSpecs(symbols.simplifyLets(fi.inlined))
+      specced.bodyOpt
+        .map(specced.wrapLets)
         .map(getTargets(_, kind, path))
         .getOrElse(Set.empty)
 
@@ -538,7 +594,7 @@ trait EffectsAnalyzer extends oo.CachingPhase {
     case Block(_, last) => getTargets(last, kind, path)
 
     case Let(vd, e, b) if !symbols.isMutableType(vd.tpe) =>
-      getTargets(b, kind, path)
+      getTargets(b, kind, path).map(_.bind(vd, e))
 
     case Let(vd, e, b) =>
       val eEffects = getTargets(e, kind, path)
@@ -803,11 +859,11 @@ trait EffectsAnalyzer extends oo.CachingPhase {
      * - a combined effect effect which is strict prefix of other effects remains a combined effect
      */
     val combinedEffects = truncatedEffects.flatMap { e =>
-      if (truncatedEffects.exists(e2 => e.path != e2.path && e2.prefixOf(e)))
+      if (truncatedEffects.exists(e2 => e.path != e2.path && e2.definitelyPrefixOf(e)))
         None // drop effects for which there is a strictly shorter (prefix) effect (regardless of effect kind)
       else if (truncatedEffects.exists(e2 => e.receiver == e2.receiver && e.path == e2.path && e.kind != e2.kind))
         Some(e.withKind(CombinedKind)) // different effects with the same receiver/path become combined effects
-      else if (truncatedEffects.exists(e2 => e.prefixOf(e2) && e.path != e2.path && e.kind == ReplacementKind))
+      else if (truncatedEffects.exists(e2 => e.definitelyPrefixOf(e2) && e.path != e2.path && e.kind == ReplacementKind))
         Some(e.withKind(CombinedKind)) // a top-level replacement, strict prefix of another effect, becomes a combined effect
       else
         Some(e)
diff --git a/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala b/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala
index 5431d6f0e5..55f36e4e5d 100644
--- a/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala
+++ b/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala
@@ -43,7 +43,7 @@ trait FunctionInlining extends CachingPhase with IdentitySorts { self =>
         case _ => super.transform(expr)
       }
 
-      // values that can be inlined directly, without being let-bound
+      // function bodies that can be inlined directly, without bindings
       private def isValue(e: Expr): Boolean = e match {
         case UnitLiteral() => true
         case BooleanLiteral(_) => true
diff --git a/core/src/main/scala/stainless/genc/CPrinter.scala b/core/src/main/scala/stainless/genc/CPrinter.scala
index f9ebac8c1f..e2ea1c12c0 100644
--- a/core/src/main/scala/stainless/genc/CPrinter.scala
+++ b/core/src/main/scala/stainless/genc/CPrinter.scala
@@ -23,7 +23,7 @@ class CPrinter(
       // We need to convert Set to Seq in order to use nary.
       val typeDefs = typeDefs0.toSeq
       val enums = enums0.toSeq.sortBy(_.id.name)
-      val functions = functions0.toSeq.sortBy(_.id.name)
+      val functions = functions0.toSeq.sortBy(_.id.name).filter(_.body != Right(""))
 
       def separator(s: String) = {
         "/* " + "-" * (43 - s.length) + " " + s + " " + "----- */\n\n"
diff --git a/core/src/main/scala/stainless/genc/ir/IR.scala b/core/src/main/scala/stainless/genc/ir/IR.scala
index bb8bdb8577..fec1f87275 100644
--- a/core/src/main/scala/stainless/genc/ir/IR.scala
+++ b/core/src/main/scala/stainless/genc/ir/IR.scala
@@ -51,6 +51,7 @@ private[genc] sealed trait IR { ir =>
   // Define a function body as either a regular AST or a manually defined
   // function using @cCode.function
   sealed abstract class FunBody
+  case object FunDropped extends FunBody // for @cCode.drop
   case class FunBodyAST(body: Expr) extends FunBody
   case class FunBodyManual(includes: Seq[String], body: String) extends FunBody // NOTE `body` is actually the whole function!
 
diff --git a/core/src/main/scala/stainless/genc/ir/Transformer.scala b/core/src/main/scala/stainless/genc/ir/Transformer.scala
index 3ba5d01272..8a6d0e6256 100644
--- a/core/src/main/scala/stainless/genc/ir/Transformer.scala
+++ b/core/src/main/scala/stainless/genc/ir/Transformer.scala
@@ -77,6 +77,7 @@ abstract class Transformer[From <: IR, To <: IR](final val from: From, final val
   }
 
   protected def rec(fb: FunBody)(implicit env: Env): to.FunBody = (fb: @unchecked) match {
+    case FunDropped => to.FunDropped
     case FunBodyAST(body) => to.FunBodyAST(rec(body))
     case FunBodyManual(includes, body) => to.FunBodyManual(includes, body)
   }
diff --git a/core/src/main/scala/stainless/genc/phases/ComputeDependenciesPhase.scala b/core/src/main/scala/stainless/genc/phases/ComputeDependenciesPhase.scala
index 4084dd2737..602a4c160b 100644
--- a/core/src/main/scala/stainless/genc/phases/ComputeDependenciesPhase.scala
+++ b/core/src/main/scala/stainless/genc/phases/ComputeDependenciesPhase.scala
@@ -82,13 +82,6 @@ trait ComputeDependenciesPhase extends LeonPipeline[Symbols, Dependencies] {
     def validateFunAnnotations(fd: FunDef): Unit = {
       val pos = fd.getPos
 
-      // Those next three tests could be carried out on all functions, not just dependencies
-      if (fd.isExtern && !fd.isManuallyDefined && !fd.isDropped)
-        reporter.fatalError(
-          pos,
-          s"Extern functions (${fd.id.asString}) need to be either manually defined or dropped"
-        )
-
       if (fd.isManuallyDefined && fd.isDropped)
         reporter.fatalError(
           pos,
@@ -106,13 +99,6 @@ trait ComputeDependenciesPhase extends LeonPipeline[Symbols, Dependencies] {
           pos,
           s"Generic functions (${fd.id.asString}) cannot be exported"
         )
-
-      // This last test is specific to dependencies.
-      if (fd.isDropped)
-        reporter.fatalError(
-          pos,
-          s"Dropped functions (${fd.id.asString}) shall not be used"
-        )
     }
 
     val finder = new ComputeDependenciesImpl(context)
diff --git a/core/src/main/scala/stainless/genc/phases/ExtraOps.scala b/core/src/main/scala/stainless/genc/phases/ExtraOps.scala
index 290b542e2b..19515b14e7 100644
--- a/core/src/main/scala/stainless/genc/phases/ExtraOps.scala
+++ b/core/src/main/scala/stainless/genc/phases/ExtraOps.scala
@@ -19,6 +19,8 @@ private[genc] object ExtraOps {
 
   implicit class FunAbsOps(val fa: FunAbstraction)  {
     def isManuallyDefined = hasAnnotation(manualDefAnnotation)
+    def isExtern = fa.flags contains Extern
+    def isDropped = hasAnnotation("cCode.drop") || fa.flags.contains(Ghost)
 
     def extAnnotations: Map[String, Seq[Any]] = fa.flags.collect {
       case Annotation(s, args) => s -> args
diff --git a/core/src/main/scala/stainless/genc/phases/IR2CPhase.scala b/core/src/main/scala/stainless/genc/phases/IR2CPhase.scala
index acf8d34de3..c68bec0cce 100644
--- a/core/src/main/scala/stainless/genc/phases/IR2CPhase.scala
+++ b/core/src/main/scala/stainless/genc/phases/IR2CPhase.scala
@@ -98,6 +98,8 @@ private class IR2CImpl(val ctx: inox.Context) {
     case FunBodyManual(includes, body) =>
       includes foreach { i => register(C.Include(i)) }
       Right(body)
+
+    case FunDropped => Right("")
   }
 
   private def rec(cd: ClassDef): Unit = {
diff --git a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala
index 8e0f3c7d67..de5d31fcf4 100644
--- a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala
+++ b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala
@@ -179,7 +179,7 @@ private class S2IRImpl(val context: inox.Context, val ctxDB: FunCtxDB, val deps:
   // Include the "nesting path" in case of generic functions to avoid ambiguity
   private def buildId(fa: FunAbstraction, tps: Seq[Type])(implicit tm: TypeMapping): CIR.Id = {
     val exported = fa.isInstanceOf[Outer] && fa.asInstanceOf[Outer].fd.isExported
-    rec(fa.id, withUnique = !exported) + (if (tps.nonEmpty) buildIdPostfix(tps) else buildIdFromTypeMapping(tm))
+    rec(fa.id, withUnique = !exported && !fa.isDropped) + (if (tps.nonEmpty) buildIdPostfix(tps) else buildIdFromTypeMapping(tm))
   }
 
   private def buildId(ct: ClassType)(implicit tm: TypeMapping): CIR.Id = {
@@ -511,6 +511,8 @@ private class S2IRImpl(val context: inox.Context, val ctxDB: FunCtxDB, val deps:
       if (fa.isManuallyDefined) {
         val impl = fa.getManualDefinition
         CIR.FunBodyManual(impl.includes, impl.code)
+      } else if (fa.isDropped) {
+        CIR.FunDropped
       } else {
         // Build the new environment from context and parameters
         val ctxKeys: Seq[(ValDef, Type)] = ctxDBAbs map { c => c.vd -> instantiateType(c.typ, tm1) }
@@ -725,7 +727,9 @@ private class S2IRImpl(val context: inox.Context, val ctxDB: FunCtxDB, val deps:
           CIR.Assign(CIR.Binding(vd), rec(expr))
 
         case ct: ClassType =>
-          CIR.Assign(CIR.FieldAccess(rec(obj), rec(fieldId, withUnique = !ct.tcd.cd.isExported)), rec(expr))
+          val cd = ct.tcd.cd
+          val mangling = !cd.isExported && !cd.isManuallyTyped
+          CIR.Assign(CIR.FieldAccess(rec(obj), rec(fieldId, withUnique = mangling)), rec(expr))
 
         case typ =>
           reporter.fatalError(e.getPos, s"Unexpected type $typ. Only class type are expected to update fields")
@@ -822,7 +826,7 @@ private class S2IRImpl(val context: inox.Context, val ctxDB: FunCtxDB, val deps:
         val vd = CIR.ValDef(rec(fieldId, withUnique = false), field2.typ, isVar = field2.isVar)
         CIR.Binding(vd)
       } else {
-        CIR.FieldAccess(rec(obj), rec(fieldId, withUnique = !cd.isExported))
+        CIR.FieldAccess(rec(obj), rec(fieldId, withUnique = !cd.isExported && !cd.isManuallyTyped))
       }
 
     case tuple @ Tuple(args0) =>
diff --git a/core/src/main/scala/stainless/verification/AssertionInjector.scala b/core/src/main/scala/stainless/verification/AssertionInjector.scala
index f475e90a73..bf84f262b1 100644
--- a/core/src/main/scala/stainless/verification/AssertionInjector.scala
+++ b/core/src/main/scala/stainless/verification/AssertionInjector.scala
@@ -287,11 +287,11 @@ trait AssertionInjector extends transformers.TreeTransformer {
 
     case BVTyped(signed, size, BVShift(rhs, recons)) if strictArithmetic =>
       bindIfCannotDuplicate(rhs, "rhs") { rhsx =>
-        val lt = t.LessThan(rhsx, t.BVLiteral(signed, size, size).copiedFrom(rhs)).copiedFrom(rhs)
+        val leq = t.LessEquals(rhsx, t.BVLiteral(signed, size, size).copiedFrom(rhs)).copiedFrom(rhs)
         // positivity check is only relevant for signed bitvectors
         val pos = t.GreaterEquals(rhsx, zero(true, size, rhs.getPos)).copiedFrom(rhs)
         // TODO: explain why `checkOverflow` here and `strictArithmetic` in the guard?
-        val range = if (signed && checkOverflow) t.And(pos, lt).copiedFrom(rhs) else lt
+        val range = if (signed && checkOverflow) t.And(pos, leq).copiedFrom(rhs) else leq
         // Ensure the operation doesn't shift more bits than there are.
         t.Assert(range, Some("Shift semantics"), recons(rhsx)).copiedFrom(e)
       }
diff --git a/frontends/benchmarks/extraction/invalid/IllegalAliasing2.scala b/frontends/benchmarks/extraction/invalid/IllegalAliasing2.scala
new file mode 100644
index 0000000000..d34ccae9aa
--- /dev/null
+++ b/frontends/benchmarks/extraction/invalid/IllegalAliasing2.scala
@@ -0,0 +1,15 @@
+object IllegalAliasing2 {
+
+  case class A(var x: Int)
+  def f(a1: A, a2: A): Unit = {
+  }
+
+  def zero: Int = 0
+
+  def g(a: Array[A]) = {
+    require(a.length > 0)
+
+    f(a(0), a(zero)) // Illegal passing of aliased parameters
+  }
+
+}
diff --git a/frontends/benchmarks/imperative/valid/ArrayAccess.scala b/frontends/benchmarks/imperative/valid/ArrayAccess.scala
new file mode 100644
index 0000000000..2e8b01326d
--- /dev/null
+++ b/frontends/benchmarks/imperative/valid/ArrayAccess.scala
@@ -0,0 +1,9 @@
+object ArrayAccess {
+  def zero: Int = 0
+
+  def reset(a: Array[Int]): Unit = {
+    require(a.length > 0)
+    a(zero) = 0
+    a(0) = 0
+  }
+}
diff --git a/frontends/benchmarks/imperative/valid/Issue1097.scala b/frontends/benchmarks/imperative/valid/Issue1097.scala
new file mode 100644
index 0000000000..44716c1151
--- /dev/null
+++ b/frontends/benchmarks/imperative/valid/Issue1097.scala
@@ -0,0 +1,30 @@
+import stainless.lang._
+import stainless.annotation._
+
+object Mutable {
+  sealed case class MutCell[@mutable T](var value: T)
+  sealed case class Container[T](field: MutCell[Option[T]])
+
+  sealed abstract class Option[@mutable T]
+  case class None[@mutable T]()               extends Option[T]
+  case class Some[@mutable T](_0: MutCell[T]) extends Option[T]
+
+  def get_mut[T](self: MutCell[Container[T]]): Option[T] =
+    self.value.field match {
+      case MutCell(Some(t)) => Some[T](t)
+      case _                => None[T]()
+    }
+
+  @pure def main: Unit = {
+    val target: MutCell[Container[Int]] = MutCell(
+      Container(MutCell(Some(MutCell(123))))
+    )
+    get_mut[Int](target) match {
+      case Some(v) => v.value = 456               // AntiAliasing replaces `v.value = 456` with `()`
+      case _       => error[Nothing]("no value")
+    }
+    assert(
+      target.value == Container(MutCell[Option[Int]](Some(MutCell(456))))
+    )
+  }
+}
diff --git a/frontends/benchmarks/imperative/valid/Issue1111.scala b/frontends/benchmarks/imperative/valid/Issue1111.scala
new file mode 100644
index 0000000000..5f7ed5c5d9
--- /dev/null
+++ b/frontends/benchmarks/imperative/valid/Issue1111.scala
@@ -0,0 +1,28 @@
+import stainless.annotation._
+
+object Issue1111 {
+  sealed abstract class Option[@mutable T]
+  case class None[@mutable T]()               extends Option[T]
+  case class Some[@mutable T](_0: MutCell[T]) extends Option[T]
+
+  sealed case class Tuple2[@mutable T0, @mutable T1](_0: MutCell[T0], _1: MutCell[T1])
+
+  case class MutCell[@mutable T](var value: T)
+
+  def get_mut[@mutable V](self: MutCell[Tuple2[String, V]], key: String): Option[V] =
+    if (self.value._0.value == key) Some[V](self.value._1)
+    else None[V]()
+
+  @pure
+  def main: Unit = {
+    val target = MutCell[Tuple2[String, Int]](
+      Tuple2[String, Int](MutCell[String]("bar"), MutCell[Int](0))
+    )
+    get_mut[Int](target, "foo") match {
+      case Some(v1) =>
+        v1.value = 123 // if this line is commented, all passes
+      case _ =>
+        ()
+    }
+  }
+}
diff --git a/frontends/benchmarks/imperative/valid/WrappedArray.scala b/frontends/benchmarks/imperative/valid/WrappedArray.scala
new file mode 100644
index 0000000000..7aa6c075f5
--- /dev/null
+++ b/frontends/benchmarks/imperative/valid/WrappedArray.scala
@@ -0,0 +1,23 @@
+object WrappingArray {
+
+  case class A(var x: Int)
+  case class Wrap(ar: Array[A])
+
+  def getA(w: Wrap, i: Int): A = {
+    require(0 <= i && i < w.ar.length)
+    w.ar(i)
+  }
+
+  def reset(a: A): Unit = { a.x = 0 }
+  def set(a: A, v: Int): Unit = { a.x = v }
+
+  def test(w: Wrap, i: Int): Unit = {
+    require(0 < i && i < w.ar.length)
+    reset(getA(w, 0))
+    set(getA(w, i), 100)
+    assert(w.ar(0).x == 0)
+    assert(w.ar(i).x == 100)
+    reset(getA(w, i))
+    assert(w.ar(i).x == 0)
+  }
+}