diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index 0663193777e31031faad28e4bcfae31e46f495f2..8a5f627a778dd520bc6605c7210c00cb5a06ad85 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -1,5 +1,4 @@
 /* Copyright 2009-2015 EPFL, Lausanne */
-
 package leon.xlang
 
 import leon.TransformationPhase
@@ -177,6 +176,10 @@ object AntiAliasingPhase extends TransformationPhase {
                 args.zipWithIndex.filter{ case (arg, i) => fiEffects.contains(i) }
                     .map(_._1.asInstanceOf[Variable])
 
+              val duplicatedParams = modifiedArgs.diff(modifiedArgs.distinct).distinct
+              if(duplicatedParams.nonEmpty) 
+                ctx.reporter.fatalError(fi.getPos, "Illegal passing of aliased parameter: " + duplicatedParams.head)
+
               val freshRes = FreshIdentifier("res", nfd.returnType)
 
               val extractResults = Block(
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing5.scala b/src/test/resources/regression/xlang/error/ArrayAliasing5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b9363d1ab5a627df29e6a0f0018c73850dcbb529
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing5.scala
@@ -0,0 +1,18 @@
+import leon.lang._
+
+object ArrayAliasing5 {
+
+
+  def f1(a: Array[BigInt], b: Array[BigInt]): Unit = {
+    require(a.length > 0 && b.length > 0)
+    a(0) = 10
+    b(0) = 20
+  } ensuring(_ => a(0) == 10 && b(0) == 20)
+
+
+  def callWithAliases(): Unit = {
+    val a = Array[BigInt](0,0,0,0)
+    f1(a, a)
+  }
+
+}