diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala index 54494713006989f356b8174088a79402c5b1e4b0..aa1e07e3c0c98834a538c633558be2c37875794b 100644 --- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala +++ b/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) diff --git a/src/test/resources/regression/frontends/error/simple/ArrayEquals1.scala b/src/test/resources/regression/frontends/error/simple/ArrayEquals1.scala new file mode 100644 index 0000000000000000000000000000000000000000..39a9c4b2be2fd3a581ee3209f0d83f16dc8e03b7 --- /dev/null +++ b/src/test/resources/regression/frontends/error/simple/ArrayEquals1.scala @@ -0,0 +1,10 @@ +package leon.lang._ + +object ArrayEqual1 { + + def f: Boolean = { + Array(1,2,3) == Array(1,2,3) + } ensuring(res => res) + +} + diff --git a/src/test/resources/regression/frontends/error/simple/ArrayEquals2.scala b/src/test/resources/regression/frontends/error/simple/ArrayEquals2.scala new file mode 100644 index 0000000000000000000000000000000000000000..2035e0d45c3cc8236009c5b70f0c0e2ac3b95124 --- /dev/null +++ b/src/test/resources/regression/frontends/error/simple/ArrayEquals2.scala @@ -0,0 +1,10 @@ +package leon.lang._ + +object ArrayEqual2 { + + def f: Boolean = { + Array(1,2,3) != Array(1,2,3) + } ensuring(res => !res) + +} +