diff --git a/regression/invalid/Array1.scala b/regression/invalid/Array1.scala
deleted file mode 100644
index a8451250c8f9e9c95684b4ea10490aced2a23f6e..0000000000000000000000000000000000000000
--- a/regression/invalid/Array1.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-object Array1 {
-
- def foo(): Int = {
- val a = Array.fill(5)(0)
- a(2) = 3
- a(2)
- } ensuring(_ == 0)
-
-}
diff --git a/regression/invalid/Array2.scala b/regression/invalid/Array2.scala
deleted file mode 100644
index 54ab5e3c27918596af58c427fabedd2016a33db9..0000000000000000000000000000000000000000
--- a/regression/invalid/Array2.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-object Array2 {
-
- def foo(): Int = {
- val a = Array.fill(5)(0)
- a(2) = 3
- a.length
- } ensuring(_ == 4)
-
-}
diff --git a/regression/invalid/Array3.scala b/regression/invalid/Array3.scala
deleted file mode 100644
index 0c1bb76fdce099bd095c59d8c03fe8e6508a9776..0000000000000000000000000000000000000000
--- a/regression/invalid/Array3.scala
+++ /dev/null
@@ -1,16 +0,0 @@
-import leon.Utils._
-
-object Array3 {
-
- def foo(): Int = {
- val a = Array.fill(5)(3)
- var i = 0
- var sum = 0
- (while(i <= a.length) {
- sum = sum + a(i)
- i = i + 1
- }) invariant(i >= 0)
- sum
- } ensuring(_ == 15)
-
-}
diff --git a/regression/invalid/Array4.scala b/regression/invalid/Array4.scala
deleted file mode 100644
index 5b5e7406165ad214a7d5d5fffd85d2d4fce226e0..0000000000000000000000000000000000000000
--- a/regression/invalid/Array4.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-import leon.Utils._
-
-object Array4 {
-
- def foo(a: Array[Int]): Int = {
- a(2)
- }
-
-}
diff --git a/regression/invalid/Array5.scala b/regression/invalid/Array5.scala
deleted file mode 100644
index ecb00334971f3ecf19f3b6e6f9c25a5082f2d2d7..0000000000000000000000000000000000000000
--- a/regression/invalid/Array5.scala
+++ /dev/null
@@ -1,10 +0,0 @@
-import leon.Utils._
-
-object Array4 {
-
- def foo(a: Array[Int]): Int = {
- require(a.length > 2)
- a(2)
- } ensuring(_ == 0)
-
-}
diff --git a/regression/invalid/Epsilon1.scala b/regression/invalid/Epsilon1.scala
deleted file mode 100644
index c3c0a48be96f594fe725518a7289333bb587ef40..0000000000000000000000000000000000000000
--- a/regression/invalid/Epsilon1.scala
+++ /dev/null
@@ -1,12 +0,0 @@
-import leon.Utils._
-
-object Epsilon1 {
-
- def rand2(x: Int): Int = epsilon((y: Int) => true)
-
- //this should not hold
- def property2(x: Int): Boolean = {
- rand2(x) == rand2(x+1)
- } holds
-
-}
diff --git a/regression/invalid/Epsilon2.scala b/regression/invalid/Epsilon2.scala
deleted file mode 100644
index 20699fc427e7dce9025e578767f5364ae19aaf88..0000000000000000000000000000000000000000
--- a/regression/invalid/Epsilon2.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-import leon.Utils._
-
-object Epsilon1 {
-
- def rand3(x: Int): Int = epsilon((y: Int) => x == x)
-
- //this should not hold
- def property3(x: Int): Boolean = {
- rand3(x) == rand3(x+1)
- } holds
-}
diff --git a/regression/invalid/Epsilon3.scala b/regression/invalid/Epsilon3.scala
deleted file mode 100644
index 5ff47b6d638cc7270640f0bba95f4cd572f8201a..0000000000000000000000000000000000000000
--- a/regression/invalid/Epsilon3.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-import leon.Utils._
-
-object Epsilon3 {
-
- def posWrong(): Int = {
- epsilon((y: Int) => y >= 0)
- } ensuring(_ > 0)
-
-}
diff --git a/regression/invalid/Epsilon4.scala b/regression/invalid/Epsilon4.scala
deleted file mode 100644
index 6619e59d6f9d9721c4bc7587b47dac79f48bf437..0000000000000000000000000000000000000000
--- a/regression/invalid/Epsilon4.scala
+++ /dev/null
@@ -1,27 +0,0 @@
-import leon.Utils._
-
-object Epsilon4 {
-
- sealed abstract class MyList
- case class MyCons(head: Int, tail: MyList) extends MyList
- case class MyNil() extends MyList
-
- def size(lst: MyList): Int = (lst match {
- case MyNil() => 0
- case MyCons(_, xs) => 1 + size(xs)
- })
-
- def toSet(lst: MyList): Set[Int] = lst match {
- case MyCons(x, xs) => toSet(xs) ++ Set(x)
- case MyNil() => Set[Int]()
- }
-
- def toList(set: Set[Int]): MyList = if(set == Set.empty[Int]) MyNil() else {
- val elem = epsilon((x : Int) => set contains x)
- MyCons(elem, toList(set -- Set[Int](elem)))
- }
-
-
- def wrongProperty0(lst: MyList): Boolean = (size(toList(toSet(lst))) == size(lst)) holds
- //def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds
-}
diff --git a/regression/invalid/Epsilon5.scala b/regression/invalid/Epsilon5.scala
deleted file mode 100644
index b96fa7564e5dba8a44aeb9d750034153b362ebfe..0000000000000000000000000000000000000000
--- a/regression/invalid/Epsilon5.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-import leon.Utils._
-
-object Epsilon5 {
-
- def fooWrong(x: Int, y: Int): Int = {
- epsilon((z: Int) => z >= x && z <= y)
- } ensuring(_ > x)
-
-}
diff --git a/regression/invalid/Epsilon6.scala b/regression/invalid/Epsilon6.scala
deleted file mode 100644
index bc5aca78c3818a94df43146aba16077ffab50a71..0000000000000000000000000000000000000000
--- a/regression/invalid/Epsilon6.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-import leon.Utils._
-
-object Epsilon6 {
-
- def greaterWrong(x: Int): Int = {
- epsilon((y: Int) => y >= x)
- } ensuring(_ > x)
-
-}
diff --git a/regression/invalid/IfExpr1.scala b/regression/invalid/IfExpr1.scala
deleted file mode 100644
index 25ae2a2103b1e2cfd8bf886442adeabf12bb6dc3..0000000000000000000000000000000000000000
--- a/regression/invalid/IfExpr1.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-object IfExpr1 {
-
- def foo(): Int = {
- var a = 1
- var b = 2
- if({a = a + 1; a != b})
- a = a + 3
- else
- b = a + b
- a
- } ensuring(_ == 3)
-
-}
diff --git a/regression/invalid/IfExpr2.scala b/regression/invalid/IfExpr2.scala
deleted file mode 100644
index 1284904b5c7dfda8f601e130b6346680538aa99a..0000000000000000000000000000000000000000
--- a/regression/invalid/IfExpr2.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-object IfExpr2 {
-
- def foo(): Int = {
- var a = 1
- var b = 2
- if(a < b) {
- a = a + 3
- b = b + 2
- a = a + b
- }
- a
- } ensuring(_ == 0)
-
-}
diff --git a/regression/invalid/MyTuple1.scala b/regression/invalid/MyTuple1.scala
deleted file mode 100644
index f2b06b5b28e405bfb2487875c8e964b8f212792c..0000000000000000000000000000000000000000
--- a/regression/invalid/MyTuple1.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-object MyTuple1 {
-
- def foo(): Int = {
- val t = (1, true, 3)
- val a1 = t._1
- val a2 = t._2
- val a3 = t._3
- a3
- } ensuring( _ == 1)
-
-}
diff --git a/regression/invalid/MyTuple2.scala b/regression/invalid/MyTuple2.scala
deleted file mode 100644
index 22b62dc75b75b3193cb2f304118a89afbc90eb91..0000000000000000000000000000000000000000
--- a/regression/invalid/MyTuple2.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-object MyTuple2 {
-
- abstract class A
- case class B(i: Int) extends A
- case class C(a: A) extends A
-
- def foo(): Int = {
- val t = (B(2), C(B(3)))
- t match {
- case (B(x), C(y)) => x
- }
- } ensuring( _ == 3)
-
-}
diff --git a/regression/invalid/MyTuple3.scala b/regression/invalid/MyTuple3.scala
deleted file mode 100644
index da9f85b16a48f0676d1f15741ad47536e14b57ab..0000000000000000000000000000000000000000
--- a/regression/invalid/MyTuple3.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-object MyTuple3 {
-
- def foo(t: (Int, Int)): (Int, Int) = {
- t
- } ensuring(res => res._1 > 0 && res._2 > 1)
-
-}
diff --git a/regression/invalid/Unit1.scala b/regression/invalid/Unit1.scala
deleted file mode 100644
index 789a8f058cd8145a0dd3b7bb0d72d44fb92ee94e..0000000000000000000000000000000000000000
--- a/regression/invalid/Unit1.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-object Unit1 {
-
- def foo(u: Unit): Unit = ({
- u
- }) ensuring(_ != ())
-
-}
diff --git a/regression/valid/Array1.scala b/regression/valid/Array1.scala
deleted file mode 100644
index 3815f03443448a28fb60475b49c09c981a1377f9..0000000000000000000000000000000000000000
--- a/regression/valid/Array1.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-object Array1 {
-
- def foo(): Int = {
- val a = Array.fill(5)(0)
- a(2) = 3
- a(2)
- } ensuring(_ == 3)
-
-}
diff --git a/regression/valid/Array10.scala b/regression/valid/Array10.scala
deleted file mode 100644
index ebb60ad6e0ba7556c55c74e1b1b624e6c34b4311..0000000000000000000000000000000000000000
--- a/regression/valid/Array10.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-object Array10 {
-
- def foo(a: Array[Int]): Int = {
- require(a.length > 0)
- val b = a.clone
- b(0)
- } ensuring(res => res == a(0))
-
-}
diff --git a/regression/valid/Array2.scala b/regression/valid/Array2.scala
deleted file mode 100644
index 4f149a9305cb4b53a4a9353b82e25468c898bdc8..0000000000000000000000000000000000000000
--- a/regression/valid/Array2.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-object Array2 {
-
- def foo(): Int = {
- val a = Array.fill(5)(0)
- a(2) = 3
- a.length
- } ensuring(_ == 5)
-
-}
diff --git a/regression/valid/Array3.scala b/regression/valid/Array3.scala
deleted file mode 100644
index bbb1845b80c0ca747cb0c830828bacdc9668943f..0000000000000000000000000000000000000000
--- a/regression/valid/Array3.scala
+++ /dev/null
@@ -1,16 +0,0 @@
-import leon.Utils._
-
-object Array3 {
-
- def foo(): Int = {
- val a = Array.fill(5)(3)
- var i = 0
- var sum = 0
- (while(i < a.length) {
- sum = sum + a(i)
- i = i + 1
- }) invariant(i >= 0)
- sum
- } ensuring(_ == 15)
-
-}
diff --git a/regression/valid/Array4.scala b/regression/valid/Array4.scala
deleted file mode 100644
index fd76e02faa83f8fd1bda5fef7c91e7df7fc29864..0000000000000000000000000000000000000000
--- a/regression/valid/Array4.scala
+++ /dev/null
@@ -1,15 +0,0 @@
-import leon.Utils._
-
-object Array4 {
-
- def foo(a: Array[Int]): Int = {
- var i = 0
- var sum = 0
- (while(i < a.length) {
- sum = sum + a(i)
- i = i + 1
- }) invariant(i >= 0)
- sum
- }
-
-}
diff --git a/regression/valid/Array5.scala b/regression/valid/Array5.scala
deleted file mode 100644
index 14bed6eff332db69600353001488c46a3e56aa5d..0000000000000000000000000000000000000000
--- a/regression/valid/Array5.scala
+++ /dev/null
@@ -1,20 +0,0 @@
-import leon.Utils._
-
-object Array5 {
-
- def foo(a: Array[Int]): Int = {
- var i = 0
- var sum = 0
- (while(i < a.length) {
- sum = sum + a(i)
- i = i + 1
- }) invariant(i >= 0)
- sum
- }
-
- def bar(): Int = {
- val a = Array.fill(5)(5)
- foo(a)
- }
-
-}
diff --git a/regression/valid/Array6.scala b/regression/valid/Array6.scala
deleted file mode 100644
index bdd6b0c5d9bee06eec14b9f5917762c67af4751b..0000000000000000000000000000000000000000
--- a/regression/valid/Array6.scala
+++ /dev/null
@@ -1,15 +0,0 @@
-import leon.Utils._
-
-object Array6 {
-
- def foo(a: Array[Int]): Int = {
- require(a.length > 2 && a(2) == 5)
- a(2)
- } ensuring(_ == 5)
-
- def bar(): Int = {
- val a = Array.fill(5)(5)
- foo(a)
- }
-
-}
diff --git a/regression/valid/Array7.scala b/regression/valid/Array7.scala
deleted file mode 100644
index 55bbbb72908e2b192152162d82d2ed9fea67923b..0000000000000000000000000000000000000000
--- a/regression/valid/Array7.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-import leon.Utils._
-
-object Array7 {
-
- def foo(a: Array[Int]): Array[Int] = {
- require(a.length > 0)
- val a2 = Array.fill(a.length)(0)
- var i = 0
- (while(i < a.length) {
- a2(i) = a(i)
- i = i + 1
- }) invariant(a.length == a2.length && i >= 0 && (if(i > 0) a2(0) == a(0) else true))
- a2
- } ensuring(_(0) == a(0))
-
-
-}
diff --git a/regression/valid/Array8.scala b/regression/valid/Array8.scala
deleted file mode 100644
index 270b181220b55af1588f63e7953221ae71f9bde3..0000000000000000000000000000000000000000
--- a/regression/valid/Array8.scala
+++ /dev/null
@@ -1,8 +0,0 @@
-object Array8 {
-
- def foo(a: Array[Int]): Array[Int] = {
- require(a.length >= 2)
- a.updated(1, 3)
- } ensuring(res => res.length == a.length && res(1) == 3)
-
-}
diff --git a/regression/valid/Array9.scala b/regression/valid/Array9.scala
deleted file mode 100644
index f49333236abfaf63caa278405a89670b1c9c115d..0000000000000000000000000000000000000000
--- a/regression/valid/Array9.scala
+++ /dev/null
@@ -1,15 +0,0 @@
-object Array9 {
-
- def foo(i: Int): Array[Int] = {
- require(i > 0)
- val a = Array.fill(i)(0)
- a
- } ensuring(res => res.length == i)
-
- def bar(i: Int): Int = {
- require(i > 0)
- val b = foo(i)
- b(0)
- }
-
-}
diff --git a/regression/valid/Assign1.scala b/regression/valid/Assign1.scala
deleted file mode 100644
index 0506c6afb39b49ac5a15c77dc10ab60f54de9ee6..0000000000000000000000000000000000000000
--- a/regression/valid/Assign1.scala
+++ /dev/null
@@ -1,12 +0,0 @@
-object Assign1 {
-
- def foo(): Int = {
- var a = 0
- val tmp = a + 1
- a = a + 2
- a = a + tmp
- a = a + 4
- a
- } ensuring(_ == 7)
-
-}
diff --git a/regression/valid/Epsilon1.scala b/regression/valid/Epsilon1.scala
deleted file mode 100644
index 2ae7201dd933e345fa71a6218b48599a61110f44..0000000000000000000000000000000000000000
--- a/regression/valid/Epsilon1.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-import leon.Utils._
-
-object Epsilon1 {
-
- def greater(x: Int): Int = {
- epsilon((y: Int) => y > x)
- } ensuring(_ >= x)
-
-}
diff --git a/regression/valid/Epsilon2.scala b/regression/valid/Epsilon2.scala
deleted file mode 100644
index 36e5268e2b1ccdbc710dc8d6410ce6968231c7d1..0000000000000000000000000000000000000000
--- a/regression/valid/Epsilon2.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-import leon.Utils._
-
-object Epsilon1 {
-
- def rand(): Int = epsilon((x: Int) => true)
-
- //this should hold, that is the expected semantic of our epsilon
- def property1(): Boolean = {
- rand() == rand()
- } holds
-
-
-}
diff --git a/regression/valid/Epsilon3.scala b/regression/valid/Epsilon3.scala
deleted file mode 100644
index f652016d28976d0b7e110b009a0802a7aac10c99..0000000000000000000000000000000000000000
--- a/regression/valid/Epsilon3.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-import leon.Utils._
-
-object Epsilon3 {
-
- def pos(): Int = {
- epsilon((y: Int) => y > 0)
- } ensuring(_ >= 0)
-
-}
diff --git a/regression/valid/Epsilon4.scala b/regression/valid/Epsilon4.scala
deleted file mode 100644
index 174042863a690067fae5a2fd4aaf55f95bf29129..0000000000000000000000000000000000000000
--- a/regression/valid/Epsilon4.scala
+++ /dev/null
@@ -1,32 +0,0 @@
-import leon.Utils._
-
-object Epsilon4 {
-
- sealed abstract class MyList
- case class MyCons(head: Int, tail: MyList) extends MyList
- case class MyNil() extends MyList
-
- def size(lst: MyList): Int = (lst match {
- case MyNil() => 0
- case MyCons(_, xs) => 1 + size(xs)
- })
-
- def toSet(lst: MyList): Set[Int] = lst match {
- case MyCons(x, xs) => toSet(xs) ++ Set(x)
- case MyNil() => Set[Int]()
- }
-
- def toList(set: Set[Int]): MyList = if(set == Set.empty[Int]) MyNil() else {
- val elem = epsilon((x : Int) => set contains x)
- MyCons(elem, toList(set -- Set[Int](elem)))
- }
-
- //timeout, but this probably means that it is valid as expected
- //def property(lst: MyList): Boolean = (size(toList(toSet(lst))) <= size(lst)) holds
-
- def propertyBase(lst: MyList): Boolean = ({
- require(lst match { case MyNil() => true case _ => false})
- size(toList(toSet(lst))) <= size(lst)
- }) holds
-
-}
diff --git a/regression/valid/Epsilon5.scala b/regression/valid/Epsilon5.scala
deleted file mode 100644
index 0427cf086ba1050226ae8a3e28d6177a9904b460..0000000000000000000000000000000000000000
--- a/regression/valid/Epsilon5.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-import leon.Utils._
-
-object Epsilon5 {
-
- def foo(x: Int, y: Int): Int = {
- epsilon((z: Int) => z > x && z < y)
- } ensuring(_ >= x)
-
-}
diff --git a/regression/valid/Field1.scala b/regression/valid/Field1.scala
deleted file mode 100644
index 116557ab7b883d01a10168aeaf529d5300ee5f19..0000000000000000000000000000000000000000
--- a/regression/valid/Field1.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-object Field1 {
-
- abstract sealed class A
- case class B(size: Int) extends A
-
- def foo(): Int = {
- val b = B(3)
- b.size
- } ensuring(_ == 3)
-
-}
diff --git a/regression/valid/Field2.scala b/regression/valid/Field2.scala
deleted file mode 100644
index 9a96610235a68754b84e58f73f5e435ce642ebc9..0000000000000000000000000000000000000000
--- a/regression/valid/Field2.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-object Field2 {
-
- abstract sealed class A
- case class B(length: Int) extends A
-
- def foo(): Int = {
- val b = B(3)
- b.length
- } ensuring(_ == 3)
-
-}
diff --git a/regression/valid/IfExpr1.scala b/regression/valid/IfExpr1.scala
deleted file mode 100644
index 82db13d5285bc3c779010fd3e62b6e9e68e84e84..0000000000000000000000000000000000000000
--- a/regression/valid/IfExpr1.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-object IfExpr1 {
-
- def foo(): Int = {
- var a = 1
- var b = 2
- if({a = a + 1; a != b})
- a = a + 3
- else
- b = a + b
- a
- } ensuring(_ == 2)
-
-}
diff --git a/regression/valid/IfExpr2.scala b/regression/valid/IfExpr2.scala
deleted file mode 100644
index 7a681bc7276d07e41884147342dc0874d0bbf93d..0000000000000000000000000000000000000000
--- a/regression/valid/IfExpr2.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-object IfExpr2 {
-
- def foo(): Int = {
- var a = 1
- var b = 2
- if(a < b) {
- a = a + 3
- b = b + 2
- a = a + b
- }
- a
- } ensuring(_ == 8)
-
-}
diff --git a/regression/valid/IfExpr3.scala b/regression/valid/IfExpr3.scala
deleted file mode 100644
index 86d4e494a7ce8fd22024020bb9580b393af8377a..0000000000000000000000000000000000000000
--- a/regression/valid/IfExpr3.scala
+++ /dev/null
@@ -1,19 +0,0 @@
-object IfExpr1 {
-
- def foo(a: Int): Int = {
-
- if(a > 0) {
- var a = 1
- var b = 2
- a = 3
- a + b
- } else {
- 5
- //var a = 3
- //var b = 1
- //b = b + 1
- //a + b
- }
- } ensuring(_ == 5)
-
-}
diff --git a/regression/valid/IfExpr4.scala b/regression/valid/IfExpr4.scala
deleted file mode 100644
index 94b99fde39e6f7e10b1c898548d60592023ffbd6..0000000000000000000000000000000000000000
--- a/regression/valid/IfExpr4.scala
+++ /dev/null
@@ -1,18 +0,0 @@
-object IfExpr4 {
-
- def foo(a: Int): Int = {
-
- if(a > 0) {
- var a = 1
- var b = 2
- a = 3
- a + b
- } else {
- var a = 3
- var b = 1
- b = b + 1
- a + b
- }
- } ensuring(_ == 5)
-
-}
diff --git a/regression/valid/InstanceOf1.scala b/regression/valid/InstanceOf1.scala
deleted file mode 100644
index 1c52338bbda859f82ef7ea619af088b9c1a1812d..0000000000000000000000000000000000000000
--- a/regression/valid/InstanceOf1.scala
+++ /dev/null
@@ -1,18 +0,0 @@
-object InstanceOf1 {
-
- abstract class A
- case class B(i: Int) extends A
- case class C(i: Int) extends A
-
- def foo(): Int = {
- require(C(3).isInstanceOf[C])
- val b: A = B(2)
- if(b.isInstanceOf[B])
- 0
- else
- -1
- } ensuring(_ == 0)
-
- def bar(): Int = foo()
-
-}
diff --git a/regression/valid/MyTuple1.scala b/regression/valid/MyTuple1.scala
deleted file mode 100644
index 48383898e203c723751a7a53869ac6c8c69ae3b5..0000000000000000000000000000000000000000
--- a/regression/valid/MyTuple1.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-object MyTuple1 {
-
- def foo(): Int = {
- val t = (1, true, 3)
- val a1 = t._1
- val a2 = t._2
- val a3 = t._3
- a3
- } ensuring( _ == 3)
-
-}
diff --git a/regression/valid/MyTuple2.scala b/regression/valid/MyTuple2.scala
deleted file mode 100644
index 9fd21eb20b14350d86d06071800ec3b86acc1a84..0000000000000000000000000000000000000000
--- a/regression/valid/MyTuple2.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-object MyTuple2 {
-
- abstract class A
- case class B(i: Int) extends A
- case class C(a: A) extends A
-
- def foo(): Int = {
- val t = (B(2), C(B(3)))
- t match {
- case (B(x), C(y)) => x
- }
- } ensuring(_ == 2)
-
-}
diff --git a/regression/valid/MyTuple3.scala b/regression/valid/MyTuple3.scala
deleted file mode 100644
index 2e14c067b78d86d4d915eb72178169d641e9755a..0000000000000000000000000000000000000000
--- a/regression/valid/MyTuple3.scala
+++ /dev/null
@@ -1,8 +0,0 @@
-object MyTuple3 {
-
- def foo(): Int = {
- val t = ((2, 3), true)
- t._1._2
- } ensuring( _ == 3)
-
-}
diff --git a/regression/valid/MyTuple4.scala b/regression/valid/MyTuple4.scala
deleted file mode 100644
index 6fcfed661beca0487da4b02db71677e2dbaac60e..0000000000000000000000000000000000000000
--- a/regression/valid/MyTuple4.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-
-object MyTuple4 {
-
- abstract class A
- case class B(i: Int) extends A
- case class C(a: A) extends A
-
- def foo(): Int = {
- val t = (1, (C(B(4)), 2), 3)
- val (a1, (C(B(x)), a2), a3) = t
- x
- } ensuring( _ == 4)
-
-}
diff --git a/regression/valid/MyTuple5.scala b/regression/valid/MyTuple5.scala
deleted file mode 100644
index 6a55bc8c9cdbc4f70be7a6b79c8d11137ecb0d71..0000000000000000000000000000000000000000
--- a/regression/valid/MyTuple5.scala
+++ /dev/null
@@ -1,16 +0,0 @@
-object MyTuple1 {
-
- abstract class A
- case class B(t: (Int, Int)) extends A
- case class C(a: A) extends A
-
- def foo(): Int = {
- val t: (Int, (A, Int), Int) = (1, (C(B((4, 5))), 2), 3)
- t match {
- case (_, (B((x, y)), _), _) => x
- case (_, (C(B((_, x))), _), y) => x
- case (_, _, x) => x
- }
- } ensuring( _ == 5)
-
-}
diff --git a/regression/valid/MyTuple6.scala b/regression/valid/MyTuple6.scala
deleted file mode 100644
index a54710fbbe54d9532a5ab4d2ba9906a48ad37acc..0000000000000000000000000000000000000000
--- a/regression/valid/MyTuple6.scala
+++ /dev/null
@@ -1,8 +0,0 @@
-object MyTuple6 {
-
- def foo(t: (Int, Int)): (Int, Int) = {
- require(t._1 > 0 && t._2 > 1)
- t
- } ensuring(res => res._1 > 0 && res._2 > 1)
-
-}
diff --git a/regression/valid/Nested1.scala b/regression/valid/Nested1.scala
deleted file mode 100644
index 7745f794f369cf59b529133fa6c73383466acec8..0000000000000000000000000000000000000000
--- a/regression/valid/Nested1.scala
+++ /dev/null
@@ -1,15 +0,0 @@
-object Nested1 {
-
- def foo(i: Int): Int = {
- val n = 2
- def rec1(j: Int) = i + j + n
- def rec2(j: Int) = {
- def rec3(k: Int) = k + j + i
- rec3(5)
- }
- rec2(2)
- } ensuring(i + 7 == _)
-
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/regression/valid/Nested10.scala b/regression/valid/Nested10.scala
deleted file mode 100644
index b3c4f865367ca84a52091e89b655ac6438dc65a2..0000000000000000000000000000000000000000
--- a/regression/valid/Nested10.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-object Nested10 {
-
- def foo(i: Int): Int = {
- val n = 2
- def rec1(j: Int) = {
- i + j + n
- }
- def rec2(j: Int) = {
- rec1(j)
- }
- rec2(2)
- } ensuring(i + 4 == _)
-
-}
diff --git a/regression/valid/Nested11.scala b/regression/valid/Nested11.scala
deleted file mode 100644
index 0316fc5f2ba3497691bc48b1d573933ba2cea027..0000000000000000000000000000000000000000
--- a/regression/valid/Nested11.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-object Nested11 {
-
- abstract class A
- case class B(b: Int) extends A
-
- def foo(i: Int): Int = {
- val b: A = B(3)
- def rec1(j: Int) = b match {
- case B(b) => i + j + b
- }
- rec1(2)
- } ensuring(i + 5 == _)
-
-}
diff --git a/regression/valid/Nested12.scala b/regression/valid/Nested12.scala
deleted file mode 100644
index 05ac1569f630f1fc905a84f0550cbbaa42047906..0000000000000000000000000000000000000000
--- a/regression/valid/Nested12.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-object Nested12 {
-
- abstract class A
- case class B(b: Int) extends A
-
- def foo(i: Int): Int = {
- val b: A = B(3)
- def rec1(a: A, j: Int, j2: Int) = a match {
- case B(b) => i + j + j2 + b
- }
- def rec2(a: A, k: Int) = a match {
- case B(b) => rec1(a, b, k)
- }
- rec2(b, 2)
- } ensuring(i + 8 == _)
-
-}
diff --git a/regression/valid/Nested13.scala b/regression/valid/Nested13.scala
deleted file mode 100644
index ccb742494564433dffe096210fac07b37a663dfe..0000000000000000000000000000000000000000
--- a/regression/valid/Nested13.scala
+++ /dev/null
@@ -1,21 +0,0 @@
-object Nested13 {
-
- abstract class D
- case class E(e: Int) extends D
- case class F(d: D, f: Int) extends D
-
- def foo(a : Int): Int = {
-
- def rec1(d: D, j: Int): Int = d match {
- case E(e) => j + e + a
- case F(dNext, f) => f + rec1(dNext, j)
- }
-
- def rec2(d: D, i : Int) : Int = d match {
- case E(e) => e
- case F(dNext, f) => rec1(d, i)
- }
-
- rec2(F(E(2), 3), 0)
- } ensuring(a + 5 == _)
-}
diff --git a/regression/valid/Nested14.scala b/regression/valid/Nested14.scala
deleted file mode 100644
index 9a79a4f6e4e7c28aa860d0636487a60a06e9e2ba..0000000000000000000000000000000000000000
--- a/regression/valid/Nested14.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-object Nested14 {
-
- def foo(i: Int): Int = {
- def rec1(j: Int): Int = {
- def rec2(k: Int): Int = if(k == 0) 0 else rec1(j-1)
- rec2(j)
- }
- rec1(3)
- } ensuring(0 == _)
-
-}
diff --git a/regression/valid/Nested2.scala b/regression/valid/Nested2.scala
deleted file mode 100644
index cc7220b02109c394e71c127e4cd3f53d6714ed7f..0000000000000000000000000000000000000000
--- a/regression/valid/Nested2.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-object Nested2 {
-
- def foo(a: Int): Int = {
- require(a >= 0)
- val b = a + 2
- def rec1(c: Int): Int = {
- require(c >= 0)
- b + c
- }
- rec1(2)
- } ensuring(_ > 0)
-
-}
diff --git a/regression/valid/Nested3.scala b/regression/valid/Nested3.scala
deleted file mode 100644
index be6e6d04a335d12d079a9e3dc1a4b14ec0164014..0000000000000000000000000000000000000000
--- a/regression/valid/Nested3.scala
+++ /dev/null
@@ -1,15 +0,0 @@
-object Nested3 {
-
- def foo(a: Int): Int = {
- require(a >= 0 && a <= 50)
- val b = a + 2
- val c = a + b
- def rec1(d: Int): Int = {
- require(d >= 0 && d <= 50)
- val e = d + b + c
- e
- }
- rec1(2)
- } ensuring(_ > 0)
-
-}
diff --git a/regression/valid/Nested4.scala b/regression/valid/Nested4.scala
deleted file mode 100644
index ea1e6066c6f4b7aaf6df23065e3011b86471b7f4..0000000000000000000000000000000000000000
--- a/regression/valid/Nested4.scala
+++ /dev/null
@@ -1,19 +0,0 @@
-object Nested4 {
-
- def foo(a: Int, a2: Int): Int = {
- require(a >= 0 && a <= 50)
- val b = a + 2
- val c = a + b
- if(a2 > a) {
- def rec1(d: Int): Int = {
- require(d >= 0 && d <= 50)
- val e = d + b + c + a2
- e
- } ensuring(_ > 0)
- rec1(2)
- } else {
- 5
- }
- } ensuring(_ > 0)
-
-}
diff --git a/regression/valid/Nested5.scala b/regression/valid/Nested5.scala
deleted file mode 100644
index 6ba128f415ecc3c61ebcccb42b65100d15373982..0000000000000000000000000000000000000000
--- a/regression/valid/Nested5.scala
+++ /dev/null
@@ -1,12 +0,0 @@
-object Nested5 {
-
- def foo(a: Int): Int = {
- require(a >= 0)
- def bar(b: Int): Int = {
- require(b > 0)
- b + 3
- } ensuring(a >= 0 && _ == b + 3)
- bar(2)
- } ensuring(a >= 0 && _ == 5)
-
-}
diff --git a/regression/valid/Nested6.scala b/regression/valid/Nested6.scala
deleted file mode 100644
index 1c0220c0447dba10ccd710d60e5f19b1c1ec6e18..0000000000000000000000000000000000000000
--- a/regression/valid/Nested6.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-object Nested5 {
-
- def foo(a: Int): Int = {
- require(a >= 0)
- def bar(b: Int): Int = {
- require(b > 0)
- b + 3
- } ensuring(prop(a, b) && a >= 0 && _ == b + 3)
- bar(2)
- } ensuring(a >= 0 && _ == 5)
-
- def prop(x: Int, y: Int): Boolean = x + y > 0
-
-}
diff --git a/regression/valid/Nested7.scala b/regression/valid/Nested7.scala
deleted file mode 100644
index 62f5a567f49be174873a24711e630f69e8469a22..0000000000000000000000000000000000000000
--- a/regression/valid/Nested7.scala
+++ /dev/null
@@ -1,19 +0,0 @@
-object Nested2 {
-
- def foo(a: Int): Int = {
- require(a >= 0)
- val b = a + 2
- def rec1(c: Int): Int = {
- require(c >= 0)
- b + c + bar(a) + bar(b) + bar(c)
- }
- rec1(2) + bar(a)
- } ensuring(_ > 0)
-
-
- def bar(x: Int): Int = {
- require(x >= 0)
- x
- } ensuring(_ >= 0)
-
-}
diff --git a/regression/valid/Nested8.scala b/regression/valid/Nested8.scala
deleted file mode 100644
index e8a05e40e6cd1b2428e03bcf1a9f96c67797c698..0000000000000000000000000000000000000000
--- a/regression/valid/Nested8.scala
+++ /dev/null
@@ -1,43 +0,0 @@
-import leon.Utils._
-
-object Nested8 {
-
- def foo(a: Int): Int = {
- require(a > 0)
-
- def bar(b: Int): Int = {
- if(a < b) {
- def rec(c: Int): Int = {
- require(c > 0)
- c + b
- } ensuring(_ > 0)
- rec(2)
- } else 3
- }
- bar(1)
- } ensuring(_ > 0)
-
- /*
- def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
- require(l1 >= 0 && u1 < l2 && u2 < size)
- if(l2 > u2 || l1 > u1)
- true
- else {
- var i = l1
- var j = l2
- var isPartitionned = true
- (while(i <= u1) {
- j = l2
- (while(j <= u2) {
- if(a(i) > a(j))
- isPartitionned = false
- j = j + 1
- }) invariant(j >= l2 && i <= u1)
- i = i + 1
- }) invariant(i >= l1)
- isPartitionned
- }
- }
- */
-
-}
diff --git a/regression/valid/Nested9.scala b/regression/valid/Nested9.scala
deleted file mode 100644
index 3344a2c7973bed9da2c42208742c34c184b458ac..0000000000000000000000000000000000000000
--- a/regression/valid/Nested9.scala
+++ /dev/null
@@ -1,23 +0,0 @@
-object Nested4 {
-
- def foo(a: Int, a2: Int): Int = {
- require(a >= 0 && a <= 50)
- val b = a + 2
- val c = a + b
- if(a2 > a) {
- def rec1(d: Int): Int = {
- require(d >= 0 && d <= 50)
- val e = d + b + c + a2
- def rec2(f: Int): Int = {
- require(f >= c)
- f + e
- } ensuring(_ > 0)
- rec2(c+1)
- } ensuring(_ > 0)
- rec1(2)
- } else {
- 5
- }
- } ensuring(_ > 0)
-
-}
diff --git a/regression/valid/NestedVar.scala b/regression/valid/NestedVar.scala
deleted file mode 100644
index a26b7312b2f5f85509c6e55cc706fb29845202b1..0000000000000000000000000000000000000000
--- a/regression/valid/NestedVar.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-object NestedVar {
-
- def foo(): Int = {
- val a = 3
- def rec(x: Int): Int = {
- var b = 3
- var c = 3
- if(x > 0)
- b = 2
- else
- c = 2
- c+b
- }
- rec(a)
- } ensuring(_ == 5)
-
-}
diff --git a/regression/valid/Unit1.scala b/regression/valid/Unit1.scala
deleted file mode 100644
index a7b890d762648cba480c817506c7eee22259860d..0000000000000000000000000000000000000000
--- a/regression/valid/Unit1.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-object Unit1 {
-
- def foo(): Unit = ({
- ()
- }) ensuring(_ == ())
-
-}
diff --git a/regression/valid/Unit2.scala b/regression/valid/Unit2.scala
deleted file mode 100644
index ac659589af503a8a79f261f9eb05be095e2e0943..0000000000000000000000000000000000000000
--- a/regression/valid/Unit2.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-object Unit2 {
-
- def foo(u: Unit): Unit = {
- u
- } ensuring(_ == ())
-
-}
diff --git a/regression/valid/While1.scala b/regression/valid/While1.scala
deleted file mode 100644
index 0d868b399330c91342bd4ed26f7166f6b40dae5f..0000000000000000000000000000000000000000
--- a/regression/valid/While1.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-object While1 {
-
- def foo(): Int = {
- var a = 0
- var i = 0
- while(i < 10) {
- a = a + 1
- i = i + 1
- }
- a
- } ensuring(_ == 10)
-
-}
diff --git a/regression/valid/While2.scala b/regression/valid/While2.scala
deleted file mode 100644
index e841ed40ebf045e5545b584b5c16e80bfc11396a..0000000000000000000000000000000000000000
--- a/regression/valid/While2.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-object While1 {
-
- def foo(): Int = {
- var a = 0
- var i = 0
- while(i < 10) {
- a = a + i
- i = i + 1
- }
- a
- } ensuring(_ == 45)
-
-}
diff --git a/regression/valid/While3.scala b/regression/valid/While3.scala
deleted file mode 100644
index da85d5dfab90410eb4d2ee23cea90627d1d40c93..0000000000000000000000000000000000000000
--- a/regression/valid/While3.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-object While3 {
-
- def foo(): Int = {
- var a = 0
- var i = 0
- while({i = i+2; i <= 10}) {
- a = a + i
- i = i - 1
- }
- a
- } ensuring(_ == 54)
-
-}
diff --git a/run-tests.sh b/run-tests.sh
deleted file mode 100755
index 15852d10f97f27a322dc6fee842d07fed1b848f1..0000000000000000000000000000000000000000
--- a/run-tests.sh
+++ /dev/null
@@ -1,47 +0,0 @@
-#!/bin/bash
-
-base=./regression
-nbtests=$(ls -l $base/{valid,invalid,error}/*.scala | wc -l)
-nbsuccess=0
-failedtests=""
-
-for f in $base/valid/*.scala; do
- echo -n "Running $f, expecting VALID, got: "
- res=`./leon --xlang --noLuckyTests --timeout=10 --oneline "$f"`
- echo $res | tr [a-z] [A-Z]
- if [ $res = valid ]; then
- nbsuccess=$((nbsuccess + 1))
- else
- failedtests="$failedtests $f"
- fi
-done
-
-for f in $base/invalid/*.scala; do
- echo -n "Running $f, expecting INVALID, got: "
- res=`./leon --xlang --noLuckyTests --timeout=10 --oneline "$f"`
- echo $res | tr [a-z] [A-Z]
- if [ $res = invalid ]; then
- nbsuccess=$((nbsuccess + 1))
- else
- failedtests="$failedtests $f"
- fi
-done
-
-for f in $base/error/*.scala; do
- echo -n "Running $f, expecting ERROR, got: "
- res=`./leon --xlang --noLuckyTests --timeout=10 --oneline "$f"`
- echo $res | tr [a-z] [A-Z]
- if [ $res = error ]; then
- nbsuccess=$((nbsuccess + 1))
- else
- failedtests="$failedtests $f"
- fi
-done
-
-echo "$nbsuccess out of $nbtests tests were successful"
-if [ $nbtests -eq $nbsuccess ]; then
- echo "PASSED"
-else
- echo "ERROR. The following test did not run as expected:"
- for f in $failedtests; do echo $f; done
-fi