regression is now at the top level

testcases/regression/invalid/Epsilon3.scala

-import leon.Utils._
-
-object Epsilon3 {
-
-  def posWrong(): Int = {
-    epsilon((y: Int) => y >= 0)
-  } ensuring(_ > 0)
-
-}

testcases/regression/invalid/Epsilon4.scala

-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
-}

testcases/regression/invalid/Epsilon5.scala

-import leon.Utils._
-
-object Epsilon5 {
-
-  def fooWrong(x: Int, y: Int): Int = {
-    epsilon((z: Int) => z >= x && z <= y)
-  } ensuring(_ > x)
-
-}

testcases/regression/invalid/Epsilon6.scala

-import leon.Utils._
-
-object Epsilon6 {
-
-  def greaterWrong(x: Int): Int = {
-    epsilon((y: Int) => y >= x)
-  } ensuring(_ > x)
-
-}

testcases/regression/invalid/IfExpr1.scala

-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)
-
-}

testcases/regression/invalid/IfExpr2.scala

-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)
-
-}

testcases/regression/invalid/MyTuple1.scala

-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)
-
-}

testcases/regression/invalid/MyTuple2.scala

-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)
-
-}

testcases/regression/invalid/MyTuple3.scala

-object MyTuple3 {
-
-  def foo(t: (Int, Int)): (Int, Int) = {
-    t
-  } ensuring(res => res._1 > 0 && res._2 > 1)
-
-}

testcases/regression/invalid/Unit1.scala

-object Unit1 {
-
-  def foo(u: Unit): Unit = ({
-    u
-  }) ensuring(_ != ())
-
-}

testcases/regression/unifier_valid.scala

-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()
-  )
-  
-}
-

testcases/regression/valid/Array1.scala

-object Array1 {
-
-  def foo(): Int = {
-    val a = Array.fill(5)(0)
-    a(2) = 3
-    a(2)
-  } ensuring(_ == 3)
-
-}

testcases/regression/valid/Array10.scala

-object Array10 {
-
-  def foo(a: Array[Int]): Int = {
-    require(a.length > 0)
-    val b = a.clone
-    b(0)
-  } ensuring(res => res == a(0))
-
-}

testcases/regression/valid/Array2.scala

-object Array2 {
-
-  def foo(): Int = {
-    val a = Array.fill(5)(0)
-    a(2) = 3
-    a.length
-  } ensuring(_ == 5)
-
-}

testcases/regression/valid/Array3.scala

-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)
-
-}

testcases/regression/valid/Array4.scala

-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
-  }
-
-}

testcases/regression/valid/Array5.scala

-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)
-  }
-
-}

testcases/regression/valid/Array6.scala

-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)
-  }
-
-}

testcases/regression/valid/Array7.scala

-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))
-
-
-}

testcases/regression/valid/Array8.scala

-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)
-
-}