detect multiple passing same argument

src/main/scala/leon/xlang/AntiAliasingPhase.scala

 /* 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(

src/test/resources/regression/xlang/error/ArrayAliasing5.scala

+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)
+  }
+
+}