diff --git a/regression/error/Array1.scala b/regression/error/Array1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d0056f18864ba168abb5735daf0db1e0bb76eda5
--- /dev/null
+++ b/regression/error/Array1.scala
@@ -0,0 +1,8 @@
+object Array1 {
+
+ def foo(): Int = {
+ (Array.fill(5)(5))(2) = 3
+ 0
+ }
+
+}
diff --git a/regression/error/Array10.scala b/regression/error/Array10.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9973626b83a01c7a8a944bcf808274d7989b3a66
--- /dev/null
+++ b/regression/error/Array10.scala
@@ -0,0 +1,12 @@
+object Array10 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ def rec(): Array[Int] = {
+ a
+ }
+ val b = rec()
+ b(0)
+ }
+
+}
diff --git a/regression/error/Array2.scala b/regression/error/Array2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9154460c37237761b6c8f2d0ecb0b34fb3ec0bf6
--- /dev/null
+++ b/regression/error/Array2.scala
@@ -0,0 +1,9 @@
+object Array2 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(5)
+ val b = a
+ b(3)
+ }
+
+}
diff --git a/regression/error/Array3.scala b/regression/error/Array3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a2c2fbd6ddfde2b3cca2dcc08fb61a79f0ae471c
--- /dev/null
+++ b/regression/error/Array3.scala
@@ -0,0 +1,12 @@
+object Array3 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(5)
+ if(a.length > 2)
+ a(1) = 2
+ else
+ 0
+ 0
+ }
+
+}
diff --git a/regression/error/Array4.scala b/regression/error/Array4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5ab0115af5e8737c6baab851822643490e79334f
--- /dev/null
+++ b/regression/error/Array4.scala
@@ -0,0 +1,8 @@
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ val b = a
+ b(3)
+ }
+
+}
diff --git a/regression/error/Array5.scala b/regression/error/Array5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..005d3d389dd1e748d139283a6fbdcb93aa8d525c
--- /dev/null
+++ b/regression/error/Array5.scala
@@ -0,0 +1,10 @@
+object Array5 {
+
+ def foo(a: Array[Int]): Int = {
+ a(2) = 4
+ a(2)
+ }
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/regression/error/Array6.scala b/regression/error/Array6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..15c87a08554c7e9563cbad9b47a881376e45a4c5
--- /dev/null
+++ b/regression/error/Array6.scala
@@ -0,0 +1,10 @@
+
+object Array6 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(5)
+ var b = a
+ b(0)
+ }
+
+}
diff --git a/regression/error/Array7.scala b/regression/error/Array7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..abb83e1c0bd931bf1d41a132fef6fb74ea25318b
--- /dev/null
+++ b/regression/error/Array7.scala
@@ -0,0 +1,9 @@
+object Array7 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(5)
+ var b = a
+ b(0)
+ }
+
+}
diff --git a/regression/error/Array8.scala b/regression/error/Array8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..89af32efdb89273ecf6b275b5a8f2f787bb73a1f
--- /dev/null
+++ b/regression/error/Array8.scala
@@ -0,0 +1,7 @@
+object Array8 {
+
+ def foo(a: Array[Int]): Array[Int] = {
+ a
+ }
+
+}
diff --git a/regression/error/Array9.scala b/regression/error/Array9.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5dc9d3aea24f7c38b8a374659058c9d0ca7fb336
--- /dev/null
+++ b/regression/error/Array9.scala
@@ -0,0 +1,11 @@
+object Array9 {
+
+ def foo(a: Array[Int]): Int = {
+ def rec(): Array[Int] = {
+ a
+ }
+ val b = rec()
+ b(0)
+ }
+
+}
diff --git a/regression/error/InstanceOf1.scala b/regression/error/InstanceOf1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a1974b4bcf8c92f320f8357297536a6053c11b98
--- /dev/null
+++ b/regression/error/InstanceOf1.scala
@@ -0,0 +1,23 @@
+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/regression/invalid/Array1.scala b/regression/invalid/Array1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a8451250c8f9e9c95684b4ea10490aced2a23f6e
--- /dev/null
+++ b/regression/invalid/Array1.scala
@@ -0,0 +1,9 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..54ab5e3c27918596af58c427fabedd2016a33db9
--- /dev/null
+++ b/regression/invalid/Array2.scala
@@ -0,0 +1,9 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..0c1bb76fdce099bd095c59d8c03fe8e6508a9776
--- /dev/null
+++ b/regression/invalid/Array3.scala
@@ -0,0 +1,16 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..5b5e7406165ad214a7d5d5fffd85d2d4fce226e0
--- /dev/null
+++ b/regression/invalid/Array4.scala
@@ -0,0 +1,9 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..ecb00334971f3ecf19f3b6e6f9c25a5082f2d2d7
--- /dev/null
+++ b/regression/invalid/Array5.scala
@@ -0,0 +1,10 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..c3c0a48be96f594fe725518a7289333bb587ef40
--- /dev/null
+++ b/regression/invalid/Epsilon1.scala
@@ -0,0 +1,12 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..20699fc427e7dce9025e578767f5364ae19aaf88
--- /dev/null
+++ b/regression/invalid/Epsilon2.scala
@@ -0,0 +1,11 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..5ff47b6d638cc7270640f0bba95f4cd572f8201a
--- /dev/null
+++ b/regression/invalid/Epsilon3.scala
@@ -0,0 +1,9 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..6619e59d6f9d9721c4bc7587b47dac79f48bf437
--- /dev/null
+++ b/regression/invalid/Epsilon4.scala
@@ -0,0 +1,27 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..b96fa7564e5dba8a44aeb9d750034153b362ebfe
--- /dev/null
+++ b/regression/invalid/Epsilon5.scala
@@ -0,0 +1,9 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..bc5aca78c3818a94df43146aba16077ffab50a71
--- /dev/null
+++ b/regression/invalid/Epsilon6.scala
@@ -0,0 +1,9 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..25ae2a2103b1e2cfd8bf886442adeabf12bb6dc3
--- /dev/null
+++ b/regression/invalid/IfExpr1.scala
@@ -0,0 +1,13 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..1284904b5c7dfda8f601e130b6346680538aa99a
--- /dev/null
+++ b/regression/invalid/IfExpr2.scala
@@ -0,0 +1,14 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..f2b06b5b28e405bfb2487875c8e964b8f212792c
--- /dev/null
+++ b/regression/invalid/MyTuple1.scala
@@ -0,0 +1,11 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..22b62dc75b75b3193cb2f304118a89afbc90eb91
--- /dev/null
+++ b/regression/invalid/MyTuple2.scala
@@ -0,0 +1,14 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..da9f85b16a48f0676d1f15741ad47536e14b57ab
--- /dev/null
+++ b/regression/invalid/MyTuple3.scala
@@ -0,0 +1,7 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..789a8f058cd8145a0dd3b7bb0d72d44fb92ee94e
--- /dev/null
+++ b/regression/invalid/Unit1.scala
@@ -0,0 +1,7 @@
+object Unit1 {
+
+ def foo(u: Unit): Unit = ({
+ u
+ }) ensuring(_ != ())
+
+}
diff --git a/regression/valid/Array1.scala b/regression/valid/Array1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3815f03443448a28fb60475b49c09c981a1377f9
--- /dev/null
+++ b/regression/valid/Array1.scala
@@ -0,0 +1,9 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..ebb60ad6e0ba7556c55c74e1b1b624e6c34b4311
--- /dev/null
+++ b/regression/valid/Array10.scala
@@ -0,0 +1,9 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..4f149a9305cb4b53a4a9353b82e25468c898bdc8
--- /dev/null
+++ b/regression/valid/Array2.scala
@@ -0,0 +1,9 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..bbb1845b80c0ca747cb0c830828bacdc9668943f
--- /dev/null
+++ b/regression/valid/Array3.scala
@@ -0,0 +1,16 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..fd76e02faa83f8fd1bda5fef7c91e7df7fc29864
--- /dev/null
+++ b/regression/valid/Array4.scala
@@ -0,0 +1,15 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..14bed6eff332db69600353001488c46a3e56aa5d
--- /dev/null
+++ b/regression/valid/Array5.scala
@@ -0,0 +1,20 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..bdd6b0c5d9bee06eec14b9f5917762c67af4751b
--- /dev/null
+++ b/regression/valid/Array6.scala
@@ -0,0 +1,15 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..55bbbb72908e2b192152162d82d2ed9fea67923b
--- /dev/null
+++ b/regression/valid/Array7.scala
@@ -0,0 +1,17 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..270b181220b55af1588f63e7953221ae71f9bde3
--- /dev/null
+++ b/regression/valid/Array8.scala
@@ -0,0 +1,8 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..f49333236abfaf63caa278405a89670b1c9c115d
--- /dev/null
+++ b/regression/valid/Array9.scala
@@ -0,0 +1,15 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..0506c6afb39b49ac5a15c77dc10ab60f54de9ee6
--- /dev/null
+++ b/regression/valid/Assign1.scala
@@ -0,0 +1,12 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..2ae7201dd933e345fa71a6218b48599a61110f44
--- /dev/null
+++ b/regression/valid/Epsilon1.scala
@@ -0,0 +1,9 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..36e5268e2b1ccdbc710dc8d6410ce6968231c7d1
--- /dev/null
+++ b/regression/valid/Epsilon2.scala
@@ -0,0 +1,13 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..f652016d28976d0b7e110b009a0802a7aac10c99
--- /dev/null
+++ b/regression/valid/Epsilon3.scala
@@ -0,0 +1,9 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..174042863a690067fae5a2fd4aaf55f95bf29129
--- /dev/null
+++ b/regression/valid/Epsilon4.scala
@@ -0,0 +1,32 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..0427cf086ba1050226ae8a3e28d6177a9904b460
--- /dev/null
+++ b/regression/valid/Epsilon5.scala
@@ -0,0 +1,9 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..116557ab7b883d01a10168aeaf529d5300ee5f19
--- /dev/null
+++ b/regression/valid/Field1.scala
@@ -0,0 +1,11 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..9a96610235a68754b84e58f73f5e435ce642ebc9
--- /dev/null
+++ b/regression/valid/Field2.scala
@@ -0,0 +1,11 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..82db13d5285bc3c779010fd3e62b6e9e68e84e84
--- /dev/null
+++ b/regression/valid/IfExpr1.scala
@@ -0,0 +1,13 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..7a681bc7276d07e41884147342dc0874d0bbf93d
--- /dev/null
+++ b/regression/valid/IfExpr2.scala
@@ -0,0 +1,14 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..86d4e494a7ce8fd22024020bb9580b393af8377a
--- /dev/null
+++ b/regression/valid/IfExpr3.scala
@@ -0,0 +1,19 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..94b99fde39e6f7e10b1c898548d60592023ffbd6
--- /dev/null
+++ b/regression/valid/IfExpr4.scala
@@ -0,0 +1,18 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..1c52338bbda859f82ef7ea619af088b9c1a1812d
--- /dev/null
+++ b/regression/valid/InstanceOf1.scala
@@ -0,0 +1,18 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..48383898e203c723751a7a53869ac6c8c69ae3b5
--- /dev/null
+++ b/regression/valid/MyTuple1.scala
@@ -0,0 +1,11 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..9fd21eb20b14350d86d06071800ec3b86acc1a84
--- /dev/null
+++ b/regression/valid/MyTuple2.scala
@@ -0,0 +1,14 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..2e14c067b78d86d4d915eb72178169d641e9755a
--- /dev/null
+++ b/regression/valid/MyTuple3.scala
@@ -0,0 +1,8 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..6fcfed661beca0487da4b02db71677e2dbaac60e
--- /dev/null
+++ b/regression/valid/MyTuple4.scala
@@ -0,0 +1,14 @@
+
+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
new file mode 100644
index 0000000000000000000000000000000000000000..6a55bc8c9cdbc4f70be7a6b79c8d11137ecb0d71
--- /dev/null
+++ b/regression/valid/MyTuple5.scala
@@ -0,0 +1,16 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..a54710fbbe54d9532a5ab4d2ba9906a48ad37acc
--- /dev/null
+++ b/regression/valid/MyTuple6.scala
@@ -0,0 +1,8 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..7745f794f369cf59b529133fa6c73383466acec8
--- /dev/null
+++ b/regression/valid/Nested1.scala
@@ -0,0 +1,15 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..b3c4f865367ca84a52091e89b655ac6438dc65a2
--- /dev/null
+++ b/regression/valid/Nested10.scala
@@ -0,0 +1,14 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..0316fc5f2ba3497691bc48b1d573933ba2cea027
--- /dev/null
+++ b/regression/valid/Nested11.scala
@@ -0,0 +1,14 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..05ac1569f630f1fc905a84f0550cbbaa42047906
--- /dev/null
+++ b/regression/valid/Nested12.scala
@@ -0,0 +1,17 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..ccb742494564433dffe096210fac07b37a663dfe
--- /dev/null
+++ b/regression/valid/Nested13.scala
@@ -0,0 +1,21 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..9a79a4f6e4e7c28aa860d0636487a60a06e9e2ba
--- /dev/null
+++ b/regression/valid/Nested14.scala
@@ -0,0 +1,11 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..cc7220b02109c394e71c127e4cd3f53d6714ed7f
--- /dev/null
+++ b/regression/valid/Nested2.scala
@@ -0,0 +1,13 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..be6e6d04a335d12d079a9e3dc1a4b14ec0164014
--- /dev/null
+++ b/regression/valid/Nested3.scala
@@ -0,0 +1,15 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..ea1e6066c6f4b7aaf6df23065e3011b86471b7f4
--- /dev/null
+++ b/regression/valid/Nested4.scala
@@ -0,0 +1,19 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..6ba128f415ecc3c61ebcccb42b65100d15373982
--- /dev/null
+++ b/regression/valid/Nested5.scala
@@ -0,0 +1,12 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..1c0220c0447dba10ccd710d60e5f19b1c1ec6e18
--- /dev/null
+++ b/regression/valid/Nested6.scala
@@ -0,0 +1,14 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..62f5a567f49be174873a24711e630f69e8469a22
--- /dev/null
+++ b/regression/valid/Nested7.scala
@@ -0,0 +1,19 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..e8a05e40e6cd1b2428e03bcf1a9f96c67797c698
--- /dev/null
+++ b/regression/valid/Nested8.scala
@@ -0,0 +1,43 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..3344a2c7973bed9da2c42208742c34c184b458ac
--- /dev/null
+++ b/regression/valid/Nested9.scala
@@ -0,0 +1,23 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..a26b7312b2f5f85509c6e55cc706fb29845202b1
--- /dev/null
+++ b/regression/valid/NestedVar.scala
@@ -0,0 +1,17 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..a7b890d762648cba480c817506c7eee22259860d
--- /dev/null
+++ b/regression/valid/Unit1.scala
@@ -0,0 +1,7 @@
+object Unit1 {
+
+ def foo(): Unit = ({
+ ()
+ }) ensuring(_ == ())
+
+}
diff --git a/regression/valid/Unit2.scala b/regression/valid/Unit2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ac659589af503a8a79f261f9eb05be095e2e0943
--- /dev/null
+++ b/regression/valid/Unit2.scala
@@ -0,0 +1,7 @@
+object Unit2 {
+
+ def foo(u: Unit): Unit = {
+ u
+ } ensuring(_ == ())
+
+}
diff --git a/regression/valid/While1.scala b/regression/valid/While1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0d868b399330c91342bd4ed26f7166f6b40dae5f
--- /dev/null
+++ b/regression/valid/While1.scala
@@ -0,0 +1,13 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..e841ed40ebf045e5545b584b5c16e80bfc11396a
--- /dev/null
+++ b/regression/valid/While2.scala
@@ -0,0 +1,13 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..da85d5dfab90410eb4d2ee23cea90627d1d40c93
--- /dev/null
+++ b/regression/valid/While3.scala
@@ -0,0 +1,13 @@
+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
index 1a5be572416c6f6794a4f7d1ce108423aebfdc35..7a36168c1eb87dea5b72074eaf7277a2cbcbc5e6 100755
--- a/run-tests.sh
+++ b/run-tests.sh
@@ -1,36 +1,37 @@
#!/bin/bash
-nbtests=$(ls -l testcases/regression/{valid,invalid,error}/*.scala | wc -l)
+base=./regression
+nbtests=$(ls -l $base/{valid,invalid,error}/*.scala | wc -l)
nbsuccess=0
failedtests=""
-for f in testcases/regression/valid/*.scala; do
+for f in $base/valid/*.scala; do
echo -n "Running $f, expecting VALID, got: "
res=`./leon --noLuckyTests --timeout=10 --oneline "$f"`
echo $res | tr [a-z] [A-Z]
- if [ "$res" = valid ]; then
+ if [ $res = valid ]; then
nbsuccess=$((nbsuccess + 1))
else
failedtests="$failedtests $f"
fi
done
-for f in testcases/regression/invalid/*.scala; do
+for f in $base/invalid/*.scala; do
echo -n "Running $f, expecting INVALID, got: "
res=`./leon --noLuckyTests --timeout=10 --oneline "$f"`
echo $res | tr [a-z] [A-Z]
- if [ "$res" = invalid ]; then
+ if [ $res = invalid ]; then
nbsuccess=$((nbsuccess + 1))
else
failedtests="$failedtests $f"
fi
done
-for f in testcases/regression/error/*.scala; do
+for f in $base/error/*.scala; do
echo -n "Running $f, expecting ERROR, got: "
res=`./leon --noLuckyTests --timeout=10 --oneline "$f"`
echo $res | tr [a-z] [A-Z]
- if [ "$res" = error ]; then
+ if [ $res = error ]; then
nbsuccess=$((nbsuccess + 1))
else
failedtests="$failedtests $f"