diff --git a/src/test/resources/regression/verification/purescala/invalid/Array1.scala b/src/test/resources/regression/verification/purescala/invalid/Array1.scala index b9120da13a85b3bc2cb764ac22bfe1af8bb31aa2..7d1276d56bf3f7b16e062263a7956f2e3c013992 100644 --- a/src/test/resources/regression/verification/purescala/invalid/Array1.scala +++ b/src/test/resources/regression/verification/purescala/invalid/Array1.scala @@ -2,7 +2,7 @@ import leon.lang._ -object Array4 { +object Array1 { def foo(a: Array[Int]): Int = { a(2) diff --git a/src/test/resources/regression/verification/purescala/invalid/Array2.scala b/src/test/resources/regression/verification/purescala/invalid/Array2.scala index 0806854c697d0ac5b4d0402db8f0b715fbfdf85f..6764616629e1306690a7d51a5bcb1007c31b5392 100644 --- a/src/test/resources/regression/verification/purescala/invalid/Array2.scala +++ b/src/test/resources/regression/verification/purescala/invalid/Array2.scala @@ -2,7 +2,7 @@ import leon.lang._ -object Array4 { +object Array2 { def foo(a: Array[Int]): Int = { require(a.length > 2) diff --git a/src/test/resources/regression/verification/purescala/invalid/Array3.scala b/src/test/resources/regression/verification/purescala/invalid/Array3.scala index b7be061e3444ecfbb3ac44760cd15e2ac8c65e76..2646acfd0f8feff9f33f7dac196e29ec15eddb3f 100644 --- a/src/test/resources/regression/verification/purescala/invalid/Array3.scala +++ b/src/test/resources/regression/verification/purescala/invalid/Array3.scala @@ -2,8 +2,7 @@ import leon.lang._ -object Test { - +object Array3 { def find(c: Array[Int], i: Int): Int = { require(i >= 0) if(c(i) == i) diff --git a/src/test/resources/regression/verification/purescala/invalid/Asserts1.scala b/src/test/resources/regression/verification/purescala/invalid/Asserts1.scala index 4860603fcfc6f84c332c8cbfc553b2e28233e18b..33ed13652535df2f725f1937516c78c18dee718a 100644 --- a/src/test/resources/regression/verification/purescala/invalid/Asserts1.scala +++ b/src/test/resources/regression/verification/purescala/invalid/Asserts1.scala @@ -2,7 +2,7 @@ import leon.lang._ import leon.annotation._ import leon._ -object Operators { +object Asserts1 { def foo(a: Int): Int = { require(a > 0) diff --git a/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala b/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala index 2ce16db2d26694cd1a20b97033ea41a316114a81..c009a24e0630437802db70408e0a2806ecd4fb97 100644 --- a/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala +++ b/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala @@ -2,7 +2,7 @@ import leon.lang._ -object FiniteSorting { +object FiniteSort { // These finite sorting functions essentially implement insertion sort. def sort2(x : Int, y : Int) : (Int,Int) = { diff --git a/src/test/resources/regression/verification/purescala/invalid/Generics.scala b/src/test/resources/regression/verification/purescala/invalid/Generics.scala index 1c8566937e7c3a1c56edaf62aa6bfb4a7db9a099..c444946eedfbfcbb2b068bfc3a07e554aa14309f 100644 --- a/src/test/resources/regression/verification/purescala/invalid/Generics.scala +++ b/src/test/resources/regression/verification/purescala/invalid/Generics.scala @@ -2,7 +2,7 @@ import leon.lang._ -object Generics1 { +object Generics { abstract class List[T] case class Cons[A](head: A, tail: List[A]) extends List[A] case class Nil[B]() extends List[B] diff --git a/src/test/resources/regression/verification/purescala/invalid/Generics2.scala b/src/test/resources/regression/verification/purescala/invalid/Generics2.scala index 56dc25fd4fd8573039deab177c4e88f536475579..0f5d336eaee16aa8f175bc02c8abcdeeac14e50b 100644 --- a/src/test/resources/regression/verification/purescala/invalid/Generics2.scala +++ b/src/test/resources/regression/verification/purescala/invalid/Generics2.scala @@ -2,7 +2,7 @@ import leon.lang._ -object Generics1 { +object Generics2 { abstract class List[T] case class Cons[A](head: A, tail: List[A]) extends List[A] case class Nil[B]() extends List[B] diff --git a/src/test/resources/regression/verification/purescala/invalid/Lists.scala b/src/test/resources/regression/verification/purescala/invalid/Lists.scala index 3286fd638dcf3af111bb77343a44498a2c97378a..ce72b940d49fed6ace47edf154f22629e00928ce 100644 --- a/src/test/resources/regression/verification/purescala/invalid/Lists.scala +++ b/src/test/resources/regression/verification/purescala/invalid/Lists.scala @@ -1,6 +1,6 @@ import leon.lang._ -object Lists4 { +object Lists { abstract class List[T] case class Cons[T](head: T, tail: List[T]) extends List[T] case class Nil[T]() extends List[T] diff --git a/src/test/resources/regression/verification/purescala/valid/Generics.scala b/src/test/resources/regression/verification/purescala/valid/Generics.scala index 7e1b2359f35b7b197738397782b20d0a73a32df6..f4c5c1b20bf0b6183e94d34d7c51de8eac7aa499 100644 --- a/src/test/resources/regression/verification/purescala/valid/Generics.scala +++ b/src/test/resources/regression/verification/purescala/valid/Generics.scala @@ -2,7 +2,7 @@ import leon.lang._ -object Generics1 { +object Generics { abstract class List[T] case class Cons[A](head: A, tail: List[A]) extends List[A] case class Nil[B]() extends List[B] diff --git a/src/test/resources/regression/verification/purescala/valid/MyTuple5.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple5.scala index 0b573500d64e383c822a4244001afd80a3a47423..a427c410debc8c87f89377bf404ac3d43d8b1a92 100644 --- a/src/test/resources/regression/verification/purescala/valid/MyTuple5.scala +++ b/src/test/resources/regression/verification/purescala/valid/MyTuple5.scala @@ -1,6 +1,6 @@ /* Copyright 2009-2014 EPFL, Lausanne */ -object MyTuple1 { +object MyTuple5 { abstract class A case class B(t: (Int, Int)) extends A diff --git a/src/test/resources/regression/verification/purescala/valid/Sets2.scala b/src/test/resources/regression/verification/purescala/valid/Sets2.scala index f25449028f2a5c5975d46ff889ee3a352b13d941..244f5bebff8032d4fe685be216ee48a1533faab5 100644 --- a/src/test/resources/regression/verification/purescala/valid/Sets2.scala +++ b/src/test/resources/regression/verification/purescala/valid/Sets2.scala @@ -1,6 +1,6 @@ import leon.lang._ -object Sets1 { +object Sets2 { def set(i: Int): Int => Boolean = x => x == i def complement(s: Int => Boolean): Int => Boolean = x => !s(x) diff --git a/src/test/resources/regression/verification/purescala/valid/Subtyping2.scala b/src/test/resources/regression/verification/purescala/valid/Subtyping2.scala index b51c6017316396618390fbad6108f3ea038329d6..bc96d0617a8bf2361e16c35316a15c8895eb71a2 100644 --- a/src/test/resources/regression/verification/purescala/valid/Subtyping2.scala +++ b/src/test/resources/regression/verification/purescala/valid/Subtyping2.scala @@ -2,7 +2,7 @@ import leon.lang._ -object Test { +object Subtyping2 { abstract class List case class Nil() extends List diff --git a/src/test/resources/regression/verification/xlang/invalid/Array5.scala b/src/test/resources/regression/verification/xlang/invalid/Array5.scala index 0806854c697d0ac5b4d0402db8f0b715fbfdf85f..c906cb2be6eab272e929cd3fc58cd4819e1e00ba 100644 --- a/src/test/resources/regression/verification/xlang/invalid/Array5.scala +++ b/src/test/resources/regression/verification/xlang/invalid/Array5.scala @@ -2,7 +2,7 @@ import leon.lang._ -object Array4 { +object Array5 { def foo(a: Array[Int]): Int = { require(a.length > 2) diff --git a/src/test/resources/regression/verification/xlang/invalid/Array6.scala b/src/test/resources/regression/verification/xlang/invalid/Array6.scala index 7cadad30def7f7097d0317880fb47ee30f4bed1e..e327f1e755adf2b2bd9e7457bc9f4d0d57375884 100644 --- a/src/test/resources/regression/verification/xlang/invalid/Array6.scala +++ b/src/test/resources/regression/verification/xlang/invalid/Array6.scala @@ -2,7 +2,7 @@ import leon.lang._ -object Array4 { +object Array6 { def foo(a: Array[Int]): Int = { require(a.length > 0) diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala index 45c4adf7939124d36c083fce717c97ab172c6d1d..756356422806fd68fea8c1f374a7179c0ceee02a 100644 --- a/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala +++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala @@ -3,7 +3,7 @@ import leon.lang._ import leon.lang.xlang._ -object Epsilon1 { +object Epsilon2 { def rand3(x: Int): Int = epsilon((y: Int) => x == x) diff --git a/src/test/resources/regression/verification/xlang/valid/Choose1.scala b/src/test/resources/regression/verification/xlang/valid/Choose1.scala index 893db3e784b2abc9e607fef274f41ed426a33c48..24d80897c547eb4799a563a3ca2c1c7e8dec48cd 100644 --- a/src/test/resources/regression/verification/xlang/valid/Choose1.scala +++ b/src/test/resources/regression/verification/xlang/valid/Choose1.scala @@ -3,7 +3,7 @@ import leon.lang._ import leon.lang.synthesis._ -object Test { +object Choose1 { def test(x: Int): Int = { diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala index 289bdd4d114f43defcb6134340eae9be42595784..d3c805ceab72c9701cee7f5281fa4382beab1535 100644 --- a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala +++ b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala @@ -3,7 +3,7 @@ import leon.lang._ import leon.lang.xlang._ -object Epsilon1 { +object Epsilon2 { def rand(): Int = epsilon((x: Int) => true) diff --git a/src/test/resources/regression/verification/xlang/valid/IfExpr3.scala b/src/test/resources/regression/verification/xlang/valid/IfExpr3.scala index 46f4264d31f42ecc47ec3ad9be233e56bbde0ea7..18e4bd7627e10711e83222406a5dd4b36c173719 100644 --- a/src/test/resources/regression/verification/xlang/valid/IfExpr3.scala +++ b/src/test/resources/regression/verification/xlang/valid/IfExpr3.scala @@ -1,6 +1,6 @@ /* Copyright 2009-2014 EPFL, Lausanne */ -object IfExpr1 { +object IfExpr3 { def foo(a: Int): Int = { diff --git a/src/test/resources/regression/verification/xlang/valid/Nested6.scala b/src/test/resources/regression/verification/xlang/valid/Nested6.scala index f7bfa772fa2f31ac30efa8fd3c1be5be6813318b..fac37a152767eefcdffbb5aab493a4d559f86723 100644 --- a/src/test/resources/regression/verification/xlang/valid/Nested6.scala +++ b/src/test/resources/regression/verification/xlang/valid/Nested6.scala @@ -1,6 +1,6 @@ /* Copyright 2009-2014 EPFL, Lausanne */ -object Nested5 { +object Nested6 { def foo(a: BigInt): BigInt = { require(a >= 0) diff --git a/src/test/resources/regression/verification/xlang/valid/Nested7.scala b/src/test/resources/regression/verification/xlang/valid/Nested7.scala index 4187e7b0fb31affe67314cb072be128ef386ca5b..ebc4c663f096a9008bab6e71904fcb42f0446834 100644 --- a/src/test/resources/regression/verification/xlang/valid/Nested7.scala +++ b/src/test/resources/regression/verification/xlang/valid/Nested7.scala @@ -1,6 +1,6 @@ /* Copyright 2009-2014 EPFL, Lausanne */ -object Nested2 { +object Nested7 { def foo(a: BigInt): BigInt = { require(a >= 0) diff --git a/src/test/resources/regression/verification/xlang/valid/Nested9.scala b/src/test/resources/regression/verification/xlang/valid/Nested9.scala index 148ba3a589cf1d61003bd9f79d4a7d04f994416f..c652e6f79d9e3a29c583e8dcfc48b4f3c73311ee 100644 --- a/src/test/resources/regression/verification/xlang/valid/Nested9.scala +++ b/src/test/resources/regression/verification/xlang/valid/Nested9.scala @@ -1,6 +1,6 @@ /* Copyright 2009-2014 EPFL, Lausanne */ -object Nested4 { +object Nested9 { def foo(a: BigInt, a2: BigInt): BigInt = { require(a >= 0 && a <= 50) diff --git a/src/test/resources/regression/verification/xlang/valid/While2.scala b/src/test/resources/regression/verification/xlang/valid/While2.scala index 841724ab4e6628070f89d489503533ad68f34127..df125cf1dcda4f9c63141dabd0a94a46db380d58 100644 --- a/src/test/resources/regression/verification/xlang/valid/While2.scala +++ b/src/test/resources/regression/verification/xlang/valid/While2.scala @@ -1,6 +1,6 @@ /* Copyright 2009-2014 EPFL, Lausanne */ -object While1 { +object While2 { def foo(): Int = { var a = 0