diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index f9610904ce4d8af594cec320532f435d4d6fdadc..0663193777e31031faad28e4bcfae31e46f495f2 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -60,6 +60,12 @@ object AntiAliasingPhase extends TransformationPhase {
       case _ => None
     }.map(_.id)
 
+    fd.body.foreach(body => getReturnedExpr(body).foreach{
+      case v@Variable(id) if aliasedParams.contains(id) =>
+        ctx.reporter.fatalError(v.getPos, "Cannot return a shared reference to a mutable object")
+      case _ => ()
+    })
+
     val newReturnType: TypeTree = if(aliasedParams.isEmpty) fd.returnType else {
       tupleTypeWrap(fd.returnType +: aliasedParams.map(_.getType))
     }
@@ -280,4 +286,17 @@ object AntiAliasingPhase extends TransformationPhase {
   }
 
 
+  /*
+   * A bit hacky, but not sure of the best way to do something like that
+   * currently.
+   */
+  private def getReturnedExpr(expr: Expr): Seq[Expr] = expr match {
+    case Let(_, _, rest) => getReturnedExpr(rest)
+    case LetVar(_, _, rest) => getReturnedExpr(rest)
+    case Block(_, rest) => getReturnedExpr(rest)
+    case IfExpr(_, thenn, elze) => getReturnedExpr(thenn) ++ getReturnedExpr(elze)
+    case MatchExpr(_, cses) => cses.flatMap{ cse => getReturnedExpr(cse.rhs) }
+    case e => Seq(expr)
+  }
+
 }
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing4.scala b/src/test/resources/regression/xlang/error/ArrayAliasing4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2632782c39e853744744b66309ef10342bee386b
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing4.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+
+object ArrayAliasing4 {
+
+  def f1(a: Array[BigInt]): Array[BigInt] = {
+    require(a.length > 0)
+    a(0) = 10
+    a
+  } ensuring(res => res(0) == 10)
+
+}