diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index 70163481fd0ba71740ce917b7944fcc2a7a10aa9..9eaf5eb3395e9996e20a7b5732815d6e70592d6b 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -332,8 +332,11 @@ object AntiAliasingPhase extends TransformationPhase {
   def checkAliasing(fd: FunDef)(ctx: LeonContext): Unit = {
     def checkReturnValue(body: Expr, bindings: Set[Identifier]): Unit = {
       getReturnedExpr(body).foreach{
-        case IsTyped(v@Variable(id), tpe) if isMutableType(tpe) && bindings.contains(id) =>
-          ctx.reporter.fatalError(v.getPos, "Cannot return a shared reference to a mutable object: " + v)
+        case expr if isMutableType(expr.getType) => 
+          findReceiverId(expr).foreach(id =>
+            if(bindings.contains(id))
+              ctx.reporter.fatalError(expr.getPos, "Cannot return a shared reference to a mutable object: " + expr)
+          )
         case _ => ()
       }
     }
diff --git a/src/test/resources/regression/xlang/error/ObjectAliasing5.scala b/src/test/resources/regression/xlang/error/ObjectAliasing5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c94656fdb9fba7d52b8eef76a7acb547682a2cdc
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ObjectAliasing5.scala
@@ -0,0 +1,12 @@
+import leon.lang._
+
+object ObjectAliasing5 {
+
+  case class A(var x: Int)
+  case class B(a: A)
+
+  def f1(b: B): A = {
+    b.a
+  }
+
+}
diff --git a/src/test/resources/regression/xlang/error/ObjectAliasing6.scala b/src/test/resources/regression/xlang/error/ObjectAliasing6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..793b9815d35635ae7539268e9b2d8878bc6a985d
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ObjectAliasing6.scala
@@ -0,0 +1,14 @@
+import leon.lang._
+
+object ObjectAliasing6 {
+
+  case class A(var x: Int)
+  case class B(a: A)
+
+  def f1(b: B): Int = {
+    val a = b.a
+    a.x = 12
+    b.a.x
+  } ensuring(_ == 12)
+
+}
diff --git a/src/test/resources/regression/xlang/error/ObjectAliasing7.scala b/src/test/resources/regression/xlang/error/ObjectAliasing7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ea28fa5bb2e01970d64c0259fc4c8d97a6878584
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ObjectAliasing7.scala
@@ -0,0 +1,22 @@
+package test.resources.regression.xlang.error
+
+import leon.lang._
+
+object ObjectAliasing7 {
+
+  case class A(var x: Int)
+  case class B(a: A)
+
+  def f1(a1: A, a2: A): Int = {
+    val tmp = a1.x
+    a2.x = a1.x
+    a1.x = tmp
+    a1.x + a2.x
+  }
+
+  def f(): Int = {
+    val b = B(A(10))
+    f1(b.a, b.a)
+  } ensuring(_ == 20)
+
+}