From 46b4a94376a054728ee72aa8782e38ab83f51590 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 28 Apr 2015 09:44:12 +0200
Subject: [PATCH] Get rid of invalid benchmark
---
.../newsolvers/valid/Choose1.scala | 42 -------------------
1 file changed, 42 deletions(-)
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Choose1.scala
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 da4b4e775..000000000
--- 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 )
-}
--
GitLab