diff --git a/src/test/resources/regression/verification/newsolvers/valid/Choose1.scala b/src/test/resources/regression/verification/newsolvers/valid/Choose1.scala deleted file mode 100644 index da4b4e7752a7a4a6fcbd21c72533e0312c18cb73..0000000000000000000000000000000000000000 --- a/src/test/resources/regression/verification/newsolvers/valid/Choose1.scala +++ /dev/null @@ -1,42 +0,0 @@ -/* Copyright 2009-2014 EPFL, Lausanne */ - -import leon.annotation._ -import leon.lang.synthesis._ -import leon.lang._ - -object Choose1 { - sealed abstract class List - case class Cons(head: Int, tail: List) extends List - case class Nil() extends List - - def size(l: List) : BigInt = (l match { - case Nil() => BigInt(0) - case Cons(_, t) => 1 + size(t) - }) ensuring(res => res >= 0) - - def content(l: List) : Set[Int] = l match { - case Nil() => Set.empty[Int] - case Cons(x, xs) => Set(x) ++ content(xs) - } - - def listOfSize(i: BigInt): List = { - require(i >= 0) - - if (i == BigInt(0)) { - Nil() - } else { - choose { (res: List) => size(res) == i } - } - } ensuring ( size(_) == i ) - - - def listOfSize2(i: BigInt): List = { - require(i >= 0) - - if (i > 0) { - Cons(0, listOfSize(i-1)) - } else { - Nil() - } - } ensuring ( size(_) == i ) -}