disallow array equality

src/main/scala/leon/frontends/scalac/CodeExtraction.scala

@@ -1387,6 +1387,9 @@ trait CodeExtraction extends ASTExtractors {
           val rr = extractTree(r)
 
           (rl, rr) match {
+            case (IsTyped(_, ArrayType(_)), IsTyped(_, ArrayType(_))) =>
+              outOfSubsetError(tr, "Leon does not support array comparison")
+
             case (IsTyped(_, rt), IsTyped(_, lt)) if typesCompatible(lt, rt) =>
               Not(Equals(rl, rr))
 
@@ -1405,6 +1408,9 @@ trait CodeExtraction extends ASTExtractors {
           val rr = extractTree(r)
 
           (rl, rr) match {
+            case (IsTyped(_, ArrayType(_)), IsTyped(_, ArrayType(_))) =>
+              outOfSubsetError(tr, "Leon does not support array comparison")
+
             case (IsTyped(_, rt), IsTyped(_, lt)) if typesCompatible(lt, rt) =>
               Equals(rl, rr)
 

src/test/resources/regression/frontends/error/simple/ArrayEquals1.scala

+package leon.lang._
+
+object ArrayEqual1 {
+
+  def f: Boolean = {
+    Array(1,2,3) == Array(1,2,3)
+  } ensuring(res => res)
+
+}
+

src/test/resources/regression/frontends/error/simple/ArrayEquals2.scala

+package leon.lang._
+
+object ArrayEqual2 {
+
+  def f: Boolean = {
+    Array(1,2,3) != Array(1,2,3)
+  } ensuring(res => !res)
+
+}
+