From 49f1e0e2bf0de1ed7244db9ddbf40210715d1354 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 24 Oct 2012 17:42:39 -0700
Subject: [PATCH] regression is now at the top level
---
testcases/regression/InfiniteLoop.scala | 12 ----
testcases/regression/README | 29 ----------
testcases/regression/error/Array1.scala | 8 ---
testcases/regression/error/Array10.scala | 12 ----
testcases/regression/error/Array2.scala | 9 ---
testcases/regression/error/Array3.scala | 12 ----
testcases/regression/error/Array4.scala | 8 ---
testcases/regression/error/Array5.scala | 10 ----
testcases/regression/error/Array6.scala | 10 ----
testcases/regression/error/Array7.scala | 9 ---
testcases/regression/error/Array8.scala | 7 ---
testcases/regression/error/Array9.scala | 11 ----
testcases/regression/error/InstanceOf1.scala | 23 --------
testcases/regression/invalid/Array1.scala | 9 ---
testcases/regression/invalid/Array2.scala | 9 ---
testcases/regression/invalid/Array3.scala | 16 ------
testcases/regression/invalid/Array4.scala | 9 ---
testcases/regression/invalid/Array5.scala | 10 ----
testcases/regression/invalid/Epsilon1.scala | 12 ----
testcases/regression/invalid/Epsilon2.scala | 11 ----
testcases/regression/invalid/Epsilon3.scala | 9 ---
testcases/regression/invalid/Epsilon4.scala | 27 ---------
testcases/regression/invalid/Epsilon5.scala | 9 ---
testcases/regression/invalid/Epsilon6.scala | 9 ---
testcases/regression/invalid/IfExpr1.scala | 13 -----
testcases/regression/invalid/IfExpr2.scala | 14 -----
testcases/regression/invalid/MyTuple1.scala | 11 ----
testcases/regression/invalid/MyTuple2.scala | 14 -----
testcases/regression/invalid/MyTuple3.scala | 7 ---
testcases/regression/invalid/Unit1.scala | 7 ---
testcases/regression/unifier_valid.scala | 60 --------------------
testcases/regression/valid/Array1.scala | 9 ---
testcases/regression/valid/Array10.scala | 9 ---
testcases/regression/valid/Array2.scala | 9 ---
testcases/regression/valid/Array3.scala | 16 ------
testcases/regression/valid/Array4.scala | 15 -----
testcases/regression/valid/Array5.scala | 20 -------
testcases/regression/valid/Array6.scala | 15 -----
testcases/regression/valid/Array7.scala | 17 ------
testcases/regression/valid/Array8.scala | 8 ---
testcases/regression/valid/Array9.scala | 15 -----
testcases/regression/valid/Assign1.scala | 12 ----
testcases/regression/valid/Epsilon1.scala | 9 ---
testcases/regression/valid/Epsilon2.scala | 13 -----
testcases/regression/valid/Epsilon3.scala | 9 ---
testcases/regression/valid/Epsilon4.scala | 32 -----------
testcases/regression/valid/Epsilon5.scala | 9 ---
testcases/regression/valid/Field1.scala | 11 ----
testcases/regression/valid/Field2.scala | 11 ----
testcases/regression/valid/IfExpr1.scala | 13 -----
testcases/regression/valid/IfExpr2.scala | 14 -----
testcases/regression/valid/IfExpr3.scala | 19 -------
testcases/regression/valid/IfExpr4.scala | 18 ------
testcases/regression/valid/InstanceOf1.scala | 18 ------
testcases/regression/valid/MyTuple1.scala | 11 ----
testcases/regression/valid/MyTuple2.scala | 14 -----
testcases/regression/valid/MyTuple3.scala | 8 ---
testcases/regression/valid/MyTuple4.scala | 14 -----
testcases/regression/valid/MyTuple5.scala | 16 ------
testcases/regression/valid/MyTuple6.scala | 8 ---
testcases/regression/valid/Nested1.scala | 15 -----
testcases/regression/valid/Nested10.scala | 14 -----
testcases/regression/valid/Nested11.scala | 14 -----
testcases/regression/valid/Nested12.scala | 17 ------
testcases/regression/valid/Nested13.scala | 21 -------
testcases/regression/valid/Nested14.scala | 11 ----
testcases/regression/valid/Nested2.scala | 13 -----
testcases/regression/valid/Nested3.scala | 15 -----
testcases/regression/valid/Nested4.scala | 19 -------
testcases/regression/valid/Nested5.scala | 12 ----
testcases/regression/valid/Nested6.scala | 14 -----
testcases/regression/valid/Nested7.scala | 19 -------
testcases/regression/valid/Nested8.scala | 43 --------------
testcases/regression/valid/Nested9.scala | 23 --------
testcases/regression/valid/NestedVar.scala | 17 ------
testcases/regression/valid/Unit1.scala | 7 ---
testcases/regression/valid/Unit2.scala | 7 ---
testcases/regression/valid/While1.scala | 13 -----
testcases/regression/valid/While2.scala | 13 -----
testcases/regression/valid/While3.scala | 13 -----
80 files changed, 1128 deletions(-)
delete mode 100644 testcases/regression/InfiniteLoop.scala
delete mode 100644 testcases/regression/README
delete mode 100644 testcases/regression/error/Array1.scala
delete mode 100644 testcases/regression/error/Array10.scala
delete mode 100644 testcases/regression/error/Array2.scala
delete mode 100644 testcases/regression/error/Array3.scala
delete mode 100644 testcases/regression/error/Array4.scala
delete mode 100644 testcases/regression/error/Array5.scala
delete mode 100644 testcases/regression/error/Array6.scala
delete mode 100644 testcases/regression/error/Array7.scala
delete mode 100644 testcases/regression/error/Array8.scala
delete mode 100644 testcases/regression/error/Array9.scala
delete mode 100644 testcases/regression/error/InstanceOf1.scala
delete mode 100644 testcases/regression/invalid/Array1.scala
delete mode 100644 testcases/regression/invalid/Array2.scala
delete mode 100644 testcases/regression/invalid/Array3.scala
delete mode 100644 testcases/regression/invalid/Array4.scala
delete mode 100644 testcases/regression/invalid/Array5.scala
delete mode 100644 testcases/regression/invalid/Epsilon1.scala
delete mode 100644 testcases/regression/invalid/Epsilon2.scala
delete mode 100644 testcases/regression/invalid/Epsilon3.scala
delete mode 100644 testcases/regression/invalid/Epsilon4.scala
delete mode 100644 testcases/regression/invalid/Epsilon5.scala
delete mode 100644 testcases/regression/invalid/Epsilon6.scala
delete mode 100644 testcases/regression/invalid/IfExpr1.scala
delete mode 100644 testcases/regression/invalid/IfExpr2.scala
delete mode 100644 testcases/regression/invalid/MyTuple1.scala
delete mode 100644 testcases/regression/invalid/MyTuple2.scala
delete mode 100644 testcases/regression/invalid/MyTuple3.scala
delete mode 100644 testcases/regression/invalid/Unit1.scala
delete mode 100644 testcases/regression/unifier_valid.scala
delete mode 100644 testcases/regression/valid/Array1.scala
delete mode 100644 testcases/regression/valid/Array10.scala
delete mode 100644 testcases/regression/valid/Array2.scala
delete mode 100644 testcases/regression/valid/Array3.scala
delete mode 100644 testcases/regression/valid/Array4.scala
delete mode 100644 testcases/regression/valid/Array5.scala
delete mode 100644 testcases/regression/valid/Array6.scala
delete mode 100644 testcases/regression/valid/Array7.scala
delete mode 100644 testcases/regression/valid/Array8.scala
delete mode 100644 testcases/regression/valid/Array9.scala
delete mode 100644 testcases/regression/valid/Assign1.scala
delete mode 100644 testcases/regression/valid/Epsilon1.scala
delete mode 100644 testcases/regression/valid/Epsilon2.scala
delete mode 100644 testcases/regression/valid/Epsilon3.scala
delete mode 100644 testcases/regression/valid/Epsilon4.scala
delete mode 100644 testcases/regression/valid/Epsilon5.scala
delete mode 100644 testcases/regression/valid/Field1.scala
delete mode 100644 testcases/regression/valid/Field2.scala
delete mode 100644 testcases/regression/valid/IfExpr1.scala
delete mode 100644 testcases/regression/valid/IfExpr2.scala
delete mode 100644 testcases/regression/valid/IfExpr3.scala
delete mode 100644 testcases/regression/valid/IfExpr4.scala
delete mode 100644 testcases/regression/valid/InstanceOf1.scala
delete mode 100644 testcases/regression/valid/MyTuple1.scala
delete mode 100644 testcases/regression/valid/MyTuple2.scala
delete mode 100644 testcases/regression/valid/MyTuple3.scala
delete mode 100644 testcases/regression/valid/MyTuple4.scala
delete mode 100644 testcases/regression/valid/MyTuple5.scala
delete mode 100644 testcases/regression/valid/MyTuple6.scala
delete mode 100644 testcases/regression/valid/Nested1.scala
delete mode 100644 testcases/regression/valid/Nested10.scala
delete mode 100644 testcases/regression/valid/Nested11.scala
delete mode 100644 testcases/regression/valid/Nested12.scala
delete mode 100644 testcases/regression/valid/Nested13.scala
delete mode 100644 testcases/regression/valid/Nested14.scala
delete mode 100644 testcases/regression/valid/Nested2.scala
delete mode 100644 testcases/regression/valid/Nested3.scala
delete mode 100644 testcases/regression/valid/Nested4.scala
delete mode 100644 testcases/regression/valid/Nested5.scala
delete mode 100644 testcases/regression/valid/Nested6.scala
delete mode 100644 testcases/regression/valid/Nested7.scala
delete mode 100644 testcases/regression/valid/Nested8.scala
delete mode 100644 testcases/regression/valid/Nested9.scala
delete mode 100644 testcases/regression/valid/NestedVar.scala
delete mode 100644 testcases/regression/valid/Unit1.scala
delete mode 100644 testcases/regression/valid/Unit2.scala
delete mode 100644 testcases/regression/valid/While1.scala
delete mode 100644 testcases/regression/valid/While2.scala
delete mode 100644 testcases/regression/valid/While3.scala
diff --git a/testcases/regression/InfiniteLoop.scala b/testcases/regression/InfiniteLoop.scala
deleted file mode 100644
index e9e5d0d5c..000000000
--- a/testcases/regression/InfiniteLoop.scala
+++ /dev/null
@@ -1,12 +0,0 @@
-object InfiniteLoop {
-
- def infinite(): Int = {
- var i = 0
- var sum = 0
- while (i < 10) {
- sum = sum + i
- }
- sum
- }
-
-}
diff --git a/testcases/regression/README b/testcases/regression/README
deleted file mode 100644
index 993f084ba..000000000
--- a/testcases/regression/README
+++ /dev/null
@@ -1,29 +0,0 @@
-Revision 1137, this morning 11:20, everything worked:
-====================================================
-mkInfiniteTree postcondition valid Unifier
-dumbInsert postcondition valid Unifier
-insert postcondition valid Unifier
-createRoot postcondition valid Unifier
-dumbInsertWithOrder postcondition valid Unifier
-====================================================
-
-Revision 1147, this evening 19:32, already broken:
-====================================================
-mkInfiniteTree postcondition valid Unifier
-dumbInsert postcondition unknown ---
-insert postcondition unknown ---
-createRoot postcondition valid Unifier
-dumbInsertWithOrder postcondition unknown ---
-====================================================
-
-Revision 1157, now, better again
-==================================================
-createRoot postcondition valid Unifier
-dumbInsert postcondition valid Unifier
-mkInfiniteTree postcondition valid Unifier
-dumbInsertWithOrder postcondition valid Unifier
-insert postcondition <BAPA seems to hang on conjunction 11>
-==================================================
-
-Okay, we're getting there..
-
diff --git a/testcases/regression/error/Array1.scala b/testcases/regression/error/Array1.scala
deleted file mode 100644
index d0056f188..000000000
--- a/testcases/regression/error/Array1.scala
+++ /dev/null
@@ -1,8 +0,0 @@
-object Array1 {
-
- def foo(): Int = {
- (Array.fill(5)(5))(2) = 3
- 0
- }
-
-}
diff --git a/testcases/regression/error/Array10.scala b/testcases/regression/error/Array10.scala
deleted file mode 100644
index 9973626b8..000000000
--- a/testcases/regression/error/Array10.scala
+++ /dev/null
@@ -1,12 +0,0 @@
-object Array10 {
-
- def foo(): Int = {
- val a = Array.fill(5)(0)
- def rec(): Array[Int] = {
- a
- }
- val b = rec()
- b(0)
- }
-
-}
diff --git a/testcases/regression/error/Array2.scala b/testcases/regression/error/Array2.scala
deleted file mode 100644
index 9154460c3..000000000
--- a/testcases/regression/error/Array2.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-object Array2 {
-
- def foo(): Int = {
- val a = Array.fill(5)(5)
- val b = a
- b(3)
- }
-
-}
diff --git a/testcases/regression/error/Array3.scala b/testcases/regression/error/Array3.scala
deleted file mode 100644
index a2c2fbd6d..000000000
--- a/testcases/regression/error/Array3.scala
+++ /dev/null
@@ -1,12 +0,0 @@
-object Array3 {
-
- def foo(): Int = {
- val a = Array.fill(5)(5)
- if(a.length > 2)
- a(1) = 2
- else
- 0
- 0
- }
-
-}
diff --git a/testcases/regression/error/Array4.scala b/testcases/regression/error/Array4.scala
deleted file mode 100644
index 5ab0115af..000000000
--- a/testcases/regression/error/Array4.scala
+++ /dev/null
@@ -1,8 +0,0 @@
-object Array4 {
-
- def foo(a: Array[Int]): Int = {
- val b = a
- b(3)
- }
-
-}
diff --git a/testcases/regression/error/Array5.scala b/testcases/regression/error/Array5.scala
deleted file mode 100644
index 005d3d389..000000000
--- a/testcases/regression/error/Array5.scala
+++ /dev/null
@@ -1,10 +0,0 @@
-object Array5 {
-
- def foo(a: Array[Int]): Int = {
- a(2) = 4
- a(2)
- }
-
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/testcases/regression/error/Array6.scala b/testcases/regression/error/Array6.scala
deleted file mode 100644
index 15c87a085..000000000
--- a/testcases/regression/error/Array6.scala
+++ /dev/null
@@ -1,10 +0,0 @@
-
-object Array6 {
-
- def foo(): Int = {
- val a = Array.fill(5)(5)
- var b = a
- b(0)
- }
-
-}
diff --git a/testcases/regression/error/Array7.scala b/testcases/regression/error/Array7.scala
deleted file mode 100644
index abb83e1c0..000000000
--- a/testcases/regression/error/Array7.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-object Array7 {
-
- def foo(): Int = {
- val a = Array.fill(5)(5)
- var b = a
- b(0)
- }
-
-}
diff --git a/testcases/regression/error/Array8.scala b/testcases/regression/error/Array8.scala
deleted file mode 100644
index 89af32efd..000000000
--- a/testcases/regression/error/Array8.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-object Array8 {
-
- def foo(a: Array[Int]): Array[Int] = {
- a
- }
-
-}
diff --git a/testcases/regression/error/Array9.scala b/testcases/regression/error/Array9.scala
deleted file mode 100644
index 5dc9d3aea..000000000
--- a/testcases/regression/error/Array9.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-object Array9 {
-
- def foo(a: Array[Int]): Int = {
- def rec(): Array[Int] = {
- a
- }
- val b = rec()
- b(0)
- }
-
-}
diff --git a/testcases/regression/error/InstanceOf1.scala b/testcases/regression/error/InstanceOf1.scala
deleted file mode 100644
index a1974b4bc..000000000
--- a/testcases/regression/error/InstanceOf1.scala
+++ /dev/null
@@ -1,23 +0,0 @@
-object InstanceOf1 {
-
- abstract class A
- case class B(i: Int) extends A
- case class C(i: Int) extends A
-
- abstract class Z
- case class Y(i: Int) extends Z
-
- def foo(): Int = {
- //require(3.isInstanceOf[Int])
- val b: A = B(2)
- if(b.isInstanceOf[Y])
- 0
- else
- -1
- } ensuring(_ == 0)
-
- def bar(): Int = foo()
-
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/testcases/regression/invalid/Array1.scala b/testcases/regression/invalid/Array1.scala
deleted file mode 100644
index a8451250c..000000000
--- a/testcases/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/testcases/regression/invalid/Array2.scala b/testcases/regression/invalid/Array2.scala
deleted file mode 100644
index 54ab5e3c2..000000000
--- a/testcases/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/testcases/regression/invalid/Array3.scala b/testcases/regression/invalid/Array3.scala
deleted file mode 100644
index 0c1bb76fd..000000000
--- a/testcases/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/testcases/regression/invalid/Array4.scala b/testcases/regression/invalid/Array4.scala
deleted file mode 100644
index 5b5e74061..000000000
--- a/testcases/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/testcases/regression/invalid/Array5.scala b/testcases/regression/invalid/Array5.scala
deleted file mode 100644
index ecb003349..000000000
--- a/testcases/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/testcases/regression/invalid/Epsilon1.scala b/testcases/regression/invalid/Epsilon1.scala
deleted file mode 100644
index c3c0a48be..000000000
--- a/testcases/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/testcases/regression/invalid/Epsilon2.scala b/testcases/regression/invalid/Epsilon2.scala
deleted file mode 100644
index 20699fc42..000000000
--- a/testcases/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/testcases/regression/invalid/Epsilon3.scala b/testcases/regression/invalid/Epsilon3.scala
deleted file mode 100644
index 5ff47b6d6..000000000
--- a/testcases/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/testcases/regression/invalid/Epsilon4.scala b/testcases/regression/invalid/Epsilon4.scala
deleted file mode 100644
index 6619e59d6..000000000
--- a/testcases/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/testcases/regression/invalid/Epsilon5.scala b/testcases/regression/invalid/Epsilon5.scala
deleted file mode 100644
index b96fa7564..000000000
--- a/testcases/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/testcases/regression/invalid/Epsilon6.scala b/testcases/regression/invalid/Epsilon6.scala
deleted file mode 100644
index bc5aca78c..000000000
--- a/testcases/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/testcases/regression/invalid/IfExpr1.scala b/testcases/regression/invalid/IfExpr1.scala
deleted file mode 100644
index 25ae2a210..000000000
--- a/testcases/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/testcases/regression/invalid/IfExpr2.scala b/testcases/regression/invalid/IfExpr2.scala
deleted file mode 100644
index 1284904b5..000000000
--- a/testcases/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/testcases/regression/invalid/MyTuple1.scala b/testcases/regression/invalid/MyTuple1.scala
deleted file mode 100644
index f2b06b5b2..000000000
--- a/testcases/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/testcases/regression/invalid/MyTuple2.scala b/testcases/regression/invalid/MyTuple2.scala
deleted file mode 100644
index 22b62dc75..000000000
--- a/testcases/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/testcases/regression/invalid/MyTuple3.scala b/testcases/regression/invalid/MyTuple3.scala
deleted file mode 100644
index da9f85b16..000000000
--- a/testcases/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/testcases/regression/invalid/Unit1.scala b/testcases/regression/invalid/Unit1.scala
deleted file mode 100644
index 789a8f058..000000000
--- a/testcases/regression/invalid/Unit1.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-object Unit1 {
-
- def foo(u: Unit): Unit = ({
- u
- }) ensuring(_ != ())
-
-}
diff --git a/testcases/regression/unifier_valid.scala b/testcases/regression/unifier_valid.scala
deleted file mode 100644
index d201527ce..000000000
--- a/testcases/regression/unifier_valid.scala
+++ /dev/null
@@ -1,60 +0,0 @@
-import scala.collection.immutable.Set
-
-object BinarySearchTree {
-
- /* Data types and the catamorphism */
-
- sealed abstract class Tree
- case class Node(left: Tree, value: Int, right: Tree) extends Tree
- case class Leaf() extends Tree
-
- def contents(tree: Tree): Set[Int] = tree match {
- case Leaf() => Set.empty[Int]
- case Node(l, v, r) => contents(l) ++ Set(v) ++ contents(r)
- }
-
- /* Tests */
-
- def insert(tree: Tree, value: Int): Node = {
- tree match {
- case Leaf() => Node(Leaf(), value, Leaf())
- case n@Node(l, v, r) => if (v < value) {
- Node(l, v, insert(r, value))
- } else if (v > value) {
- Node(insert(l, value), v, r)
- } else {
- n
- }
- }
- } ensuring (contents(_) == contents(tree) ++ Set(value))
-
-
- def dumbInsert(tree: Tree): Node = {
- tree match {
- case Leaf() => Node(Leaf(), 0, Leaf())
- case Node(l, e, r) => Node(dumbInsert(l), e, r)
- }
- } ensuring (contents(_) == contents(tree) ++ Set(0))
-
-
- def dumbInsertWithOrder(tree: Tree): Node = {
- tree match {
- case Leaf() => Node(Leaf(), 0, Leaf())
- case Node(l, e, r) => Node(dumbInsert(l), e, r)
- }
- } ensuring (res => {val S = contents(res); S == contents(tree) ++ Set(0) && S.min <= 0 && S.max >= 0})
-
-
- def createRoot(v: Int): Node = {
- Node(Leaf(), v, Leaf())
- } ensuring (contents(_) == Set(v))
-
-
- def mkInfiniteTree(x: Int): Node = {
- Node(mkInfiniteTree(x), x, mkInfiniteTree(x))
- } ensuring (res =>
- res.left != Leaf() && res.right != Leaf()
- )
-
-}
-
diff --git a/testcases/regression/valid/Array1.scala b/testcases/regression/valid/Array1.scala
deleted file mode 100644
index 3815f0344..000000000
--- a/testcases/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/testcases/regression/valid/Array10.scala b/testcases/regression/valid/Array10.scala
deleted file mode 100644
index ebb60ad6e..000000000
--- a/testcases/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/testcases/regression/valid/Array2.scala b/testcases/regression/valid/Array2.scala
deleted file mode 100644
index 4f149a930..000000000
--- a/testcases/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/testcases/regression/valid/Array3.scala b/testcases/regression/valid/Array3.scala
deleted file mode 100644
index bbb1845b8..000000000
--- a/testcases/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/testcases/regression/valid/Array4.scala b/testcases/regression/valid/Array4.scala
deleted file mode 100644
index fd76e02fa..000000000
--- a/testcases/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/testcases/regression/valid/Array5.scala b/testcases/regression/valid/Array5.scala
deleted file mode 100644
index 14bed6eff..000000000
--- a/testcases/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/testcases/regression/valid/Array6.scala b/testcases/regression/valid/Array6.scala
deleted file mode 100644
index bdd6b0c5d..000000000
--- a/testcases/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/testcases/regression/valid/Array7.scala b/testcases/regression/valid/Array7.scala
deleted file mode 100644
index 55bbbb729..000000000
--- a/testcases/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/testcases/regression/valid/Array8.scala b/testcases/regression/valid/Array8.scala
deleted file mode 100644
index 270b18122..000000000
--- a/testcases/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/testcases/regression/valid/Array9.scala b/testcases/regression/valid/Array9.scala
deleted file mode 100644
index f49333236..000000000
--- a/testcases/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/testcases/regression/valid/Assign1.scala b/testcases/regression/valid/Assign1.scala
deleted file mode 100644
index 0506c6afb..000000000
--- a/testcases/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/testcases/regression/valid/Epsilon1.scala b/testcases/regression/valid/Epsilon1.scala
deleted file mode 100644
index 2ae7201dd..000000000
--- a/testcases/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/testcases/regression/valid/Epsilon2.scala b/testcases/regression/valid/Epsilon2.scala
deleted file mode 100644
index 36e5268e2..000000000
--- a/testcases/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/testcases/regression/valid/Epsilon3.scala b/testcases/regression/valid/Epsilon3.scala
deleted file mode 100644
index f652016d2..000000000
--- a/testcases/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/testcases/regression/valid/Epsilon4.scala b/testcases/regression/valid/Epsilon4.scala
deleted file mode 100644
index 174042863..000000000
--- a/testcases/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/testcases/regression/valid/Epsilon5.scala b/testcases/regression/valid/Epsilon5.scala
deleted file mode 100644
index 0427cf086..000000000
--- a/testcases/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/testcases/regression/valid/Field1.scala b/testcases/regression/valid/Field1.scala
deleted file mode 100644
index 116557ab7..000000000
--- a/testcases/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/testcases/regression/valid/Field2.scala b/testcases/regression/valid/Field2.scala
deleted file mode 100644
index 9a9661023..000000000
--- a/testcases/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/testcases/regression/valid/IfExpr1.scala b/testcases/regression/valid/IfExpr1.scala
deleted file mode 100644
index 82db13d52..000000000
--- a/testcases/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/testcases/regression/valid/IfExpr2.scala b/testcases/regression/valid/IfExpr2.scala
deleted file mode 100644
index 7a681bc72..000000000
--- a/testcases/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/testcases/regression/valid/IfExpr3.scala b/testcases/regression/valid/IfExpr3.scala
deleted file mode 100644
index 86d4e494a..000000000
--- a/testcases/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/testcases/regression/valid/IfExpr4.scala b/testcases/regression/valid/IfExpr4.scala
deleted file mode 100644
index 94b99fde3..000000000
--- a/testcases/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/testcases/regression/valid/InstanceOf1.scala b/testcases/regression/valid/InstanceOf1.scala
deleted file mode 100644
index 1c52338bb..000000000
--- a/testcases/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/testcases/regression/valid/MyTuple1.scala b/testcases/regression/valid/MyTuple1.scala
deleted file mode 100644
index 48383898e..000000000
--- a/testcases/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/testcases/regression/valid/MyTuple2.scala b/testcases/regression/valid/MyTuple2.scala
deleted file mode 100644
index 9fd21eb20..000000000
--- a/testcases/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/testcases/regression/valid/MyTuple3.scala b/testcases/regression/valid/MyTuple3.scala
deleted file mode 100644
index 2e14c067b..000000000
--- a/testcases/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/testcases/regression/valid/MyTuple4.scala b/testcases/regression/valid/MyTuple4.scala
deleted file mode 100644
index 6fcfed661..000000000
--- a/testcases/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/testcases/regression/valid/MyTuple5.scala b/testcases/regression/valid/MyTuple5.scala
deleted file mode 100644
index 6a55bc8c9..000000000
--- a/testcases/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/testcases/regression/valid/MyTuple6.scala b/testcases/regression/valid/MyTuple6.scala
deleted file mode 100644
index a54710fbb..000000000
--- a/testcases/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/testcases/regression/valid/Nested1.scala b/testcases/regression/valid/Nested1.scala
deleted file mode 100644
index 7745f794f..000000000
--- a/testcases/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/testcases/regression/valid/Nested10.scala b/testcases/regression/valid/Nested10.scala
deleted file mode 100644
index b3c4f8653..000000000
--- a/testcases/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/testcases/regression/valid/Nested11.scala b/testcases/regression/valid/Nested11.scala
deleted file mode 100644
index 0316fc5f2..000000000
--- a/testcases/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/testcases/regression/valid/Nested12.scala b/testcases/regression/valid/Nested12.scala
deleted file mode 100644
index 05ac1569f..000000000
--- a/testcases/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/testcases/regression/valid/Nested13.scala b/testcases/regression/valid/Nested13.scala
deleted file mode 100644
index ccb742494..000000000
--- a/testcases/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/testcases/regression/valid/Nested14.scala b/testcases/regression/valid/Nested14.scala
deleted file mode 100644
index 9a79a4f6e..000000000
--- a/testcases/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/testcases/regression/valid/Nested2.scala b/testcases/regression/valid/Nested2.scala
deleted file mode 100644
index cc7220b02..000000000
--- a/testcases/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/testcases/regression/valid/Nested3.scala b/testcases/regression/valid/Nested3.scala
deleted file mode 100644
index be6e6d04a..000000000
--- a/testcases/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/testcases/regression/valid/Nested4.scala b/testcases/regression/valid/Nested4.scala
deleted file mode 100644
index ea1e6066c..000000000
--- a/testcases/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/testcases/regression/valid/Nested5.scala b/testcases/regression/valid/Nested5.scala
deleted file mode 100644
index 6ba128f41..000000000
--- a/testcases/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/testcases/regression/valid/Nested6.scala b/testcases/regression/valid/Nested6.scala
deleted file mode 100644
index 1c0220c04..000000000
--- a/testcases/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/testcases/regression/valid/Nested7.scala b/testcases/regression/valid/Nested7.scala
deleted file mode 100644
index 62f5a567f..000000000
--- a/testcases/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/testcases/regression/valid/Nested8.scala b/testcases/regression/valid/Nested8.scala
deleted file mode 100644
index e8a05e40e..000000000
--- a/testcases/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/testcases/regression/valid/Nested9.scala b/testcases/regression/valid/Nested9.scala
deleted file mode 100644
index 3344a2c79..000000000
--- a/testcases/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/testcases/regression/valid/NestedVar.scala b/testcases/regression/valid/NestedVar.scala
deleted file mode 100644
index a26b7312b..000000000
--- a/testcases/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/testcases/regression/valid/Unit1.scala b/testcases/regression/valid/Unit1.scala
deleted file mode 100644
index a7b890d76..000000000
--- a/testcases/regression/valid/Unit1.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-object Unit1 {
-
- def foo(): Unit = ({
- ()
- }) ensuring(_ == ())
-
-}
diff --git a/testcases/regression/valid/Unit2.scala b/testcases/regression/valid/Unit2.scala
deleted file mode 100644
index ac659589a..000000000
--- a/testcases/regression/valid/Unit2.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-object Unit2 {
-
- def foo(u: Unit): Unit = {
- u
- } ensuring(_ == ())
-
-}
diff --git a/testcases/regression/valid/While1.scala b/testcases/regression/valid/While1.scala
deleted file mode 100644
index 0d868b399..000000000
--- a/testcases/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/testcases/regression/valid/While2.scala b/testcases/regression/valid/While2.scala
deleted file mode 100644
index e841ed40e..000000000
--- a/testcases/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/testcases/regression/valid/While3.scala b/testcases/regression/valid/While3.scala
deleted file mode 100644
index da85d5dfa..000000000
--- a/testcases/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)
-
-}
--
GitLab