From 21422e5d62ac2e3a5548407931a2cb5ab5e64cae Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 21 Apr 2015 18:57:15 +0200
Subject: [PATCH] Make sure that all non-graveyard testcases at least compile,
test it
---
src/test/resources/regression/testcases | 1 +
src/test/scala/leon/test/LeonTestSuite.scala | 14 ++-
src/test/scala/leon/test/LeonTests.scala | 5 +-
.../test/testcases/TestCasesCompile.scala | 53 +++++++++++
.../insynth-leon-tests/BubbleSortBug.scala | 0
.../CaseClassSelectExample.scala | 0
.../insynth-leon-tests/Hole.scala | 0
.../ListOperationsHole.scala | 0
.../insynth-leon-tests/RedBlackTreeFull.scala | 0
.../insynth-synthesis-tests/Hole.scala | 0
.../insynth-synthesis-tests/LocalScope.scala | 0
.../verification/graph/MST/SpanningTree.scala | 2 -
.../verification/graph/SetIteration.scala | 2 -
.../graph/dijkstras/DijkstrasSet.scala | 2 -
.../graph/dijkstras/DijkstrasSetToVisit.scala | 2 -
.../vmcai2011-testcases/CADE07.scala | 2 +-
.../vmcai2011-testcases/CADE07Hard.scala | 2 +-
.../vmcai2011-testcases/Giuliano.scala | 2 +-
.../vmcai2011-testcases/JustFormulas.scala | 2 +-
.../vmcai2011-testcases/ListProperties.scala | 2 +-
.../vmcai2011-testcases/PaperExamples.scala | 2 +-
.../vmcai2011-testcases/SanityChecks.scala | 2 +-
.../verification/xlang/BubbleSort.scala | 0
.../xlang/NonDeterministicList.scala | 0
.../verification/xlang/QuickSortImp.scala | 0
.../verification/xlang/buggyEpsilon.scala | 0
.../master-thesis-regis/ArrayBubbleSort.scala | 0
.../master-thesis-regis/ArrayOperations.scala | 0
.../master-thesis-regis/Constraints.scala | 0
.../verification/xlang/xplusone.scala | 0
testcases/repair/Heap/Heap.scala | 2 +-
testcases/repair/Heap/Heap1.scala | 2 +-
testcases/repair/Heap/Heap10.scala | 2 +-
testcases/repair/Heap/Heap2.scala | 2 +-
testcases/repair/Heap/Heap3.scala | 2 +-
testcases/repair/Heap/Heap4.scala | 2 +-
testcases/repair/Heap/Heap5.scala | 2 +-
testcases/repair/Heap/Heap6.scala | 2 +-
testcases/repair/Heap/Heap7.scala | 2 +-
testcases/repair/Heap/Heap8.scala | 2 +-
testcases/repair/Heap/Heap9.scala | 2 +-
testcases/repair/List/List.scala | 1 +
testcases/repair/List/List1.scala | 1 +
testcases/repair/List/List10.scala | 1 +
testcases/repair/List/List11.scala | 1 +
testcases/repair/List/List12.scala | 1 +
testcases/repair/List/List13.scala | 1 +
testcases/repair/List/List2.scala | 1 +
testcases/repair/List/List3.scala | 1 +
testcases/repair/List/List4.scala | 1 +
testcases/repair/List/List5.scala | 1 +
testcases/repair/List/List6.scala | 1 +
testcases/repair/List/List7.scala | 1 +
testcases/repair/List/List8.scala | 1 +
testcases/repair/List/List9.scala | 1 +
testcases/repair/MergeSort/MergeSort1.scala | 2 +
.../repair/RedBlackTree/RedBlackTree.scala | 4 +-
.../repair/RedBlackTree/RedBlackTree1.scala | 4 +-
.../repair/RedBlackTree/RedBlackTree2.scala | 4 +-
.../repair/RedBlackTree/RedBlackTree3.scala | 4 +-
.../repair/RedBlackTree/RedBlackTree6.scala | 4 +-
testcases/repair/inria/FirstIndexOf.scala | 4 +-
testcases/repair/inria/HeapSort.scala | 2 +-
testcases/synthesis/NewYearsSong.scala | 28 ------
.../BatchedQueue/BatchedQueue.scala | 3 +-
.../BatchedQueue/BatchedQueueFull.scala | 3 +-
.../BinarySearchTreeFull.scala | 1 -
.../condabd/benchmarks/List/ListSearch.scala | 50 ----------
.../benchmarks/MergeSort/MergeSortMerge.scala | 2 +-
.../insynth-leon-tests/Arguments.scala | 13 ---
testcases/synthesis/io-examples/List.scala | 10 +-
testcases/synthesis/io-examples/Lists.scala | 20 ++--
testcases/synthesis/io-examples/Math.scala | 28 ++----
.../BatchedQueue/BatchedQueueFull.scala | 91 -------------------
.../oopsla2013/InsertionSort/Complete.scala | 48 ----------
.../oopsla2013/MergeSort/Complete.scala | 2 -
.../oopsla2013/SortedList/Batch.scala | 4 +-
.../oopsla2013/SparseVector/Complete.scala | 2 +-
testcases/verification/Addresses.scala | 1 -
.../datastructures/BinarySearchTree.scala | 3 +
.../BinarySearchTreeSorted.scala | 2 +-
.../datastructures/InsertionSort.scala | 1 -
.../datastructures/ListWithSize.scala | 1 -
.../datastructures/MergeSort.scala | 2 +-
.../datastructures/QuickSort.scala | 2 +-
.../datastructures/RedBlackTree.scala | 3 +-
.../datastructures/SortedList.scala | 1 -
.../datastructures/TreeListSetNoDup.scala | 1 -
testcases/verification/graph/MST/MSTMap.scala | 2 -
.../verification/graph/SortedNDList.scala | 2 -
testcases/verification/graph/Subgraph.scala | 2 -
.../verification/graph/SubgraphMap.scala | 2 -
.../verification/graph/TreeEquivalence.scala | 2 -
.../graph/TreeEquivalenceMap.scala | 2 -
.../graph/dijkstras/DijkstrasSortedList.scala | 2 -
.../higher-order/invalid/Continuations1.scala | 1 +
.../higher-order/invalid/HOInvocations.scala | 1 +
.../higher-order/invalid/Lists1.scala | 1 +
.../higher-order/invalid/Lists2.scala | 2 -
.../higher-order/invalid/ParBalance.scala | 2 +-
.../higher-order/invalid/PositiveMap.scala | 1 +
.../higher-order/invalid/Sets1.scala | 1 +
.../higher-order/invalid/Transformation.scala | 2 +-
.../pldi2011-testcases/AssociativeList.scala | 1 -
.../pldi2011-testcases/ForElimination.scala | 1 -
.../pldi2011-testcases/InsertionSort.scala | 1 -
.../pldi2011-testcases/LambdaEval.scala | 1 -
.../pldi2011-testcases/ListTree.scala | 2 +-
.../pldi2011-testcases/MergeSort.scala | 2 +-
.../PropositionalLogic.scala | 1 -
.../pldi2011-testcases/QuickSort.scala | 1 -
.../pldi2011-testcases/RedBlackTree.scala | 1 -
.../RedBlackTreeDeletion.scala | 4 +-
.../SemanticsPreservation.scala | 1 -
.../pldi2011-testcases/TreeMap.scala | 1 -
.../sas2011-testcases/AmortizedQueue.scala | 1 -
.../sas2011-testcases/AssociativeList.scala | 1 -
.../sas2011-testcases/InsertionSort.scala | 1 -
.../sas2011-testcases/ListOperations.scala | 1 -
.../PropositionalLogic.scala | 1 -
.../sas2011-testcases/RedBlackTree.scala | 1 -
.../sas2011-testcases/SearchLinkedList.scala | 1 -
.../scala2013/AmortizedQueue.scala | 1 -
.../scala2013/AmortizedQueueImp.scala | 1 -
.../scala2013/AssociativeList.scala | 1 -
.../scala2013/AssociativeListImp.scala | 1 -
.../scala2013/ListOperations.scala | 1 -
.../scala2013/PropositionalLogic.scala | 1 -
.../verification/scala2013/RedBlackTree.scala | 1 -
.../scala2013/SearchLinkedList.scala | 1 -
.../vstte10competition/AmortizedQueue.scala | 1 -
.../vstte10competition/Injection.scala | 78 ----------------
.../vstte10competition/SearchLinkedList.scala | 1 -
.../verification/xlang/BinaryTreeImp.scala | 1 -
testcases/verification/xlang/BubbleFun.scala | 2 +
.../verification/xlang/InsertionSortImp.scala | 1 -
.../verification/xlang/IntOperations.scala | 2 +
137 files changed, 171 insertions(+), 453 deletions(-)
create mode 120000 src/test/resources/regression/testcases
create mode 100644 src/test/scala/leon/test/testcases/TestCasesCompile.scala
rename testcases/{synthesis => graveyard}/insynth-leon-tests/BubbleSortBug.scala (100%)
rename testcases/{synthesis => graveyard}/insynth-leon-tests/CaseClassSelectExample.scala (100%)
rename testcases/{synthesis => graveyard}/insynth-leon-tests/Hole.scala (100%)
rename testcases/{synthesis => graveyard}/insynth-leon-tests/ListOperationsHole.scala (100%)
rename testcases/{synthesis => graveyard}/insynth-leon-tests/RedBlackTreeFull.scala (100%)
rename testcases/{synthesis => graveyard}/insynth-synthesis-tests/Hole.scala (100%)
rename testcases/{synthesis => graveyard}/insynth-synthesis-tests/LocalScope.scala (100%)
rename testcases/{ => graveyard}/verification/graph/MST/SpanningTree.scala (99%)
rename testcases/{ => graveyard}/verification/graph/SetIteration.scala (98%)
rename testcases/{ => graveyard}/verification/graph/dijkstras/DijkstrasSet.scala (99%)
rename testcases/{ => graveyard}/verification/graph/dijkstras/DijkstrasSetToVisit.scala (99%)
rename testcases/{ => graveyard}/verification/vmcai2011-testcases/CADE07.scala (99%)
rename testcases/{ => graveyard}/verification/vmcai2011-testcases/CADE07Hard.scala (99%)
rename testcases/{ => graveyard}/verification/vmcai2011-testcases/Giuliano.scala (95%)
rename testcases/{ => graveyard}/verification/vmcai2011-testcases/JustFormulas.scala (98%)
rename testcases/{ => graveyard}/verification/vmcai2011-testcases/ListProperties.scala (98%)
rename testcases/{ => graveyard}/verification/vmcai2011-testcases/PaperExamples.scala (96%)
rename testcases/{ => graveyard}/verification/vmcai2011-testcases/SanityChecks.scala (98%)
rename testcases/{ => graveyard}/verification/xlang/BubbleSort.scala (100%)
rename testcases/{ => graveyard}/verification/xlang/NonDeterministicList.scala (100%)
rename testcases/{ => graveyard}/verification/xlang/QuickSortImp.scala (100%)
rename testcases/{ => graveyard}/verification/xlang/buggyEpsilon.scala (100%)
rename testcases/{ => graveyard}/verification/xlang/master-thesis-regis/ArrayBubbleSort.scala (100%)
rename testcases/{ => graveyard}/verification/xlang/master-thesis-regis/ArrayOperations.scala (100%)
rename testcases/{ => graveyard}/verification/xlang/master-thesis-regis/Constraints.scala (100%)
rename testcases/{ => graveyard}/verification/xlang/xplusone.scala (100%)
delete mode 100644 testcases/synthesis/NewYearsSong.scala
delete mode 100644 testcases/synthesis/condabd/benchmarks/List/ListSearch.scala
delete mode 100644 testcases/synthesis/insynth-leon-tests/Arguments.scala
delete mode 100644 testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala
delete mode 100644 testcases/synthesis/oopsla2013/InsertionSort/Complete.scala
delete mode 100644 testcases/verification/vstte10competition/Injection.scala
diff --git a/src/test/resources/regression/testcases b/src/test/resources/regression/testcases
new file mode 120000
index 000000000..a8cc08a50
--- /dev/null
+++ b/src/test/resources/regression/testcases
@@ -0,0 +1 @@
+../../../../testcases/
\ No newline at end of file
diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala
index c43e597a6..c5e3c7f40 100644
--- a/src/test/scala/leon/test/LeonTestSuite.scala
+++ b/src/test/scala/leon/test/LeonTestSuite.scala
@@ -152,7 +152,17 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
- def filesInResourceDir(dir : String, filter : String=>Boolean = all) : Iterable[File] = {
+ def scanFilesIn(f: File, filter: String=>Boolean = all, recursive: Boolean = false): Iterable[File] = {
+ f.listFiles().flatMap{f =>
+ if (f.isDirectory && recursive) {
+ scanFilesIn(f, filter, recursive)
+ } else {
+ List(f)
+ }
+ }.filter(f => filter(f.getPath))
+ }
+
+ def filesInResourceDir(dir : String, filter : String=>Boolean = all, recursive: Boolean = false) : Iterable[File] = {
val d = this.getClass.getClassLoader.getResource(dir)
@@ -161,6 +171,6 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
new File(resourceDirHard + dir)
} else new File(d.toURI)
- asFile.listFiles().filter(f => filter(f.getPath))
+ scanFilesIn(asFile, filter, recursive)
}
}
diff --git a/src/test/scala/leon/test/LeonTests.scala b/src/test/scala/leon/test/LeonTests.scala
index d7db5f39e..5650ab907 100644
--- a/src/test/scala/leon/test/LeonTests.scala
+++ b/src/test/scala/leon/test/LeonTests.scala
@@ -30,9 +30,12 @@ class LeonFunTests extends Suites(
new SynthesisSuite,
new SynthesisRegressionSuite,
+
new LibraryVerificationRegression,
new PureScalaVerificationRegression,
- new XLangVerificationRegression
+ new XLangVerificationRegression,
+
+ new TestCasesCompile
)
class LeonUnitTests extends Suites(
diff --git a/src/test/scala/leon/test/testcases/TestCasesCompile.scala b/src/test/scala/leon/test/testcases/TestCasesCompile.scala
new file mode 100644
index 000000000..c6aad47db
--- /dev/null
+++ b/src/test/scala/leon/test/testcases/TestCasesCompile.scala
@@ -0,0 +1,53 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.test.frontends
+
+import leon._
+import test.LeonTestSuite
+import purescala.Definitions.Program
+import java.io.File
+
+class TestCasesCompile extends LeonTestSuite {
+ // Hard-code output directory, for Eclipse purposes
+
+ val pipeline = frontends.scalac.ExtractionPhase andThen utils.PreprocessingPhase
+
+ def testFrontend(f: File, strip: Int) = {
+ val name = f.getAbsolutePath.split("/").toList.drop(strip).mkString("/")
+
+ test("Compiling testcase " + name) {
+ val ctx = createLeonContext()
+ try {
+ pipeline.run(ctx)(List(f.getAbsolutePath))
+ } catch {
+ case _: LeonFatalError =>
+ fail("Failed to compile.")
+ }
+ }
+ }
+
+ private def forEachFileIn(path : String)(block : File => Unit) {
+ val fs = filesInResourceDir(path, _.endsWith(".scala"), recursive=true)
+
+ for(f <- fs.toSeq.sortBy(_.getAbsolutePath)) {
+ block(f)
+ }
+ }
+
+ val baseDir = "regression/testcases/"
+
+ val slashes = resourceDir(baseDir).getAbsolutePath.split("/").toList.size
+
+ forEachFileIn(baseDir+"repair/") { f =>
+ testFrontend(f, slashes)
+ }
+ forEachFileIn(baseDir+"runtime/") { f =>
+ testFrontend(f, slashes)
+ }
+ forEachFileIn(baseDir+"synthesis/") { f =>
+ testFrontend(f, slashes)
+ }
+ forEachFileIn(baseDir+"verification/") { f =>
+ testFrontend(f, slashes)
+ }
+}
diff --git a/testcases/synthesis/insynth-leon-tests/BubbleSortBug.scala b/testcases/graveyard/insynth-leon-tests/BubbleSortBug.scala
similarity index 100%
rename from testcases/synthesis/insynth-leon-tests/BubbleSortBug.scala
rename to testcases/graveyard/insynth-leon-tests/BubbleSortBug.scala
diff --git a/testcases/synthesis/insynth-leon-tests/CaseClassSelectExample.scala b/testcases/graveyard/insynth-leon-tests/CaseClassSelectExample.scala
similarity index 100%
rename from testcases/synthesis/insynth-leon-tests/CaseClassSelectExample.scala
rename to testcases/graveyard/insynth-leon-tests/CaseClassSelectExample.scala
diff --git a/testcases/synthesis/insynth-leon-tests/Hole.scala b/testcases/graveyard/insynth-leon-tests/Hole.scala
similarity index 100%
rename from testcases/synthesis/insynth-leon-tests/Hole.scala
rename to testcases/graveyard/insynth-leon-tests/Hole.scala
diff --git a/testcases/synthesis/insynth-leon-tests/ListOperationsHole.scala b/testcases/graveyard/insynth-leon-tests/ListOperationsHole.scala
similarity index 100%
rename from testcases/synthesis/insynth-leon-tests/ListOperationsHole.scala
rename to testcases/graveyard/insynth-leon-tests/ListOperationsHole.scala
diff --git a/testcases/synthesis/insynth-leon-tests/RedBlackTreeFull.scala b/testcases/graveyard/insynth-leon-tests/RedBlackTreeFull.scala
similarity index 100%
rename from testcases/synthesis/insynth-leon-tests/RedBlackTreeFull.scala
rename to testcases/graveyard/insynth-leon-tests/RedBlackTreeFull.scala
diff --git a/testcases/synthesis/insynth-synthesis-tests/Hole.scala b/testcases/graveyard/insynth-synthesis-tests/Hole.scala
similarity index 100%
rename from testcases/synthesis/insynth-synthesis-tests/Hole.scala
rename to testcases/graveyard/insynth-synthesis-tests/Hole.scala
diff --git a/testcases/synthesis/insynth-synthesis-tests/LocalScope.scala b/testcases/graveyard/insynth-synthesis-tests/LocalScope.scala
similarity index 100%
rename from testcases/synthesis/insynth-synthesis-tests/LocalScope.scala
rename to testcases/graveyard/insynth-synthesis-tests/LocalScope.scala
diff --git a/testcases/verification/graph/MST/SpanningTree.scala b/testcases/graveyard/verification/graph/MST/SpanningTree.scala
similarity index 99%
rename from testcases/verification/graph/MST/SpanningTree.scala
rename to testcases/graveyard/verification/graph/MST/SpanningTree.scala
index 0b564b62d..3d421f6dc 100644
--- a/testcases/verification/graph/MST/SpanningTree.scala
+++ b/testcases/graveyard/verification/graph/MST/SpanningTree.scala
@@ -1,5 +1,3 @@
-import scala.collection.immutable._
-
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/graph/SetIteration.scala b/testcases/graveyard/verification/graph/SetIteration.scala
similarity index 98%
rename from testcases/verification/graph/SetIteration.scala
rename to testcases/graveyard/verification/graph/SetIteration.scala
index f272a48a4..47eb20aa7 100644
--- a/testcases/verification/graph/SetIteration.scala
+++ b/testcases/graveyard/verification/graph/SetIteration.scala
@@ -1,5 +1,3 @@
-import scala.collection.immutable._
-
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/graph/dijkstras/DijkstrasSet.scala b/testcases/graveyard/verification/graph/dijkstras/DijkstrasSet.scala
similarity index 99%
rename from testcases/verification/graph/dijkstras/DijkstrasSet.scala
rename to testcases/graveyard/verification/graph/dijkstras/DijkstrasSet.scala
index 711eff745..96571c95f 100644
--- a/testcases/verification/graph/dijkstras/DijkstrasSet.scala
+++ b/testcases/graveyard/verification/graph/dijkstras/DijkstrasSet.scala
@@ -1,5 +1,3 @@
-import scala.collection.immutable._
-
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/graph/dijkstras/DijkstrasSetToVisit.scala b/testcases/graveyard/verification/graph/dijkstras/DijkstrasSetToVisit.scala
similarity index 99%
rename from testcases/verification/graph/dijkstras/DijkstrasSetToVisit.scala
rename to testcases/graveyard/verification/graph/dijkstras/DijkstrasSetToVisit.scala
index eb954e7ca..3664d99da 100644
--- a/testcases/verification/graph/dijkstras/DijkstrasSetToVisit.scala
+++ b/testcases/graveyard/verification/graph/dijkstras/DijkstrasSetToVisit.scala
@@ -1,5 +1,3 @@
-import scala.collection.immutable._
-
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/vmcai2011-testcases/CADE07.scala b/testcases/graveyard/verification/vmcai2011-testcases/CADE07.scala
similarity index 99%
rename from testcases/verification/vmcai2011-testcases/CADE07.scala
rename to testcases/graveyard/verification/vmcai2011-testcases/CADE07.scala
index e1e697140..0af2fdd49 100644
--- a/testcases/verification/vmcai2011-testcases/CADE07.scala
+++ b/testcases/graveyard/verification/vmcai2011-testcases/CADE07.scala
@@ -1,4 +1,4 @@
-import scala.collection.immutable.Set
+import leon.lang._
object CADE07 {
def vc1(listContent: Set[Int]) : Boolean = {
diff --git a/testcases/verification/vmcai2011-testcases/CADE07Hard.scala b/testcases/graveyard/verification/vmcai2011-testcases/CADE07Hard.scala
similarity index 99%
rename from testcases/verification/vmcai2011-testcases/CADE07Hard.scala
rename to testcases/graveyard/verification/vmcai2011-testcases/CADE07Hard.scala
index 9b4206bdc..e6e9aa062 100644
--- a/testcases/verification/vmcai2011-testcases/CADE07Hard.scala
+++ b/testcases/graveyard/verification/vmcai2011-testcases/CADE07Hard.scala
@@ -1,4 +1,4 @@
-import scala.collection.immutable.Set
+import leon.lang._
object CADE07Hard {
def vc6a(l1 : Int, nul : Int, ths : Int, tmp357 : Int, list : Set[Int], objct : Set[Int], objAlloc : Set[Int], objAlloc16 : Set[Int], objAlloc30 : Set[Int], objAlloc45 : Set[Int], objAlloc60 : Set[Int], objAlloc74 : Set[Int], listContent : Set[Int], listContent59 : Set[Int], listContent73 : Set[Int], s241 : Set[Int], s142 : Set[Int], tmp171 : Boolean) : Set[Int] = {
diff --git a/testcases/verification/vmcai2011-testcases/Giuliano.scala b/testcases/graveyard/verification/vmcai2011-testcases/Giuliano.scala
similarity index 95%
rename from testcases/verification/vmcai2011-testcases/Giuliano.scala
rename to testcases/graveyard/verification/vmcai2011-testcases/Giuliano.scala
index 51ed40b0a..b69f09485 100644
--- a/testcases/verification/vmcai2011-testcases/Giuliano.scala
+++ b/testcases/graveyard/verification/vmcai2011-testcases/Giuliano.scala
@@ -1,4 +1,4 @@
-import scala.collection.immutable.Set
+import leon.lang._
object Giuliano {
sealed abstract class List
diff --git a/testcases/verification/vmcai2011-testcases/JustFormulas.scala b/testcases/graveyard/verification/vmcai2011-testcases/JustFormulas.scala
similarity index 98%
rename from testcases/verification/vmcai2011-testcases/JustFormulas.scala
rename to testcases/graveyard/verification/vmcai2011-testcases/JustFormulas.scala
index bb902f0d5..f8c9b84a0 100644
--- a/testcases/verification/vmcai2011-testcases/JustFormulas.scala
+++ b/testcases/graveyard/verification/vmcai2011-testcases/JustFormulas.scala
@@ -1,4 +1,4 @@
-import scala.collection.immutable.Set
+import leon.lang._
object JustFormulas {
// These are just to provide some "uninterpreted function symbols"
diff --git a/testcases/verification/vmcai2011-testcases/ListProperties.scala b/testcases/graveyard/verification/vmcai2011-testcases/ListProperties.scala
similarity index 98%
rename from testcases/verification/vmcai2011-testcases/ListProperties.scala
rename to testcases/graveyard/verification/vmcai2011-testcases/ListProperties.scala
index 45b2ad1e1..aaa830d37 100644
--- a/testcases/verification/vmcai2011-testcases/ListProperties.scala
+++ b/testcases/graveyard/verification/vmcai2011-testcases/ListProperties.scala
@@ -1,4 +1,4 @@
-import scala.collection.immutable.Set
+import leon.lang._
object IntListProperties {
sealed abstract class IntList
diff --git a/testcases/verification/vmcai2011-testcases/PaperExamples.scala b/testcases/graveyard/verification/vmcai2011-testcases/PaperExamples.scala
similarity index 96%
rename from testcases/verification/vmcai2011-testcases/PaperExamples.scala
rename to testcases/graveyard/verification/vmcai2011-testcases/PaperExamples.scala
index 5f5329fb8..9ee07e0b4 100644
--- a/testcases/verification/vmcai2011-testcases/PaperExamples.scala
+++ b/testcases/graveyard/verification/vmcai2011-testcases/PaperExamples.scala
@@ -1,4 +1,4 @@
-import scala.collection.immutable.Set
+import leon.lang._
object PaperExamples {
sealed abstract class List
diff --git a/testcases/verification/vmcai2011-testcases/SanityChecks.scala b/testcases/graveyard/verification/vmcai2011-testcases/SanityChecks.scala
similarity index 98%
rename from testcases/verification/vmcai2011-testcases/SanityChecks.scala
rename to testcases/graveyard/verification/vmcai2011-testcases/SanityChecks.scala
index 5ee5f3d96..df1f6582c 100644
--- a/testcases/verification/vmcai2011-testcases/SanityChecks.scala
+++ b/testcases/graveyard/verification/vmcai2011-testcases/SanityChecks.scala
@@ -1,4 +1,4 @@
-import scala.collection.immutable.Set
+import leon.lang._
object SanityChecks {
// These are just to provide some "uninterpreted function symbols"
diff --git a/testcases/verification/xlang/BubbleSort.scala b/testcases/graveyard/verification/xlang/BubbleSort.scala
similarity index 100%
rename from testcases/verification/xlang/BubbleSort.scala
rename to testcases/graveyard/verification/xlang/BubbleSort.scala
diff --git a/testcases/verification/xlang/NonDeterministicList.scala b/testcases/graveyard/verification/xlang/NonDeterministicList.scala
similarity index 100%
rename from testcases/verification/xlang/NonDeterministicList.scala
rename to testcases/graveyard/verification/xlang/NonDeterministicList.scala
diff --git a/testcases/verification/xlang/QuickSortImp.scala b/testcases/graveyard/verification/xlang/QuickSortImp.scala
similarity index 100%
rename from testcases/verification/xlang/QuickSortImp.scala
rename to testcases/graveyard/verification/xlang/QuickSortImp.scala
diff --git a/testcases/verification/xlang/buggyEpsilon.scala b/testcases/graveyard/verification/xlang/buggyEpsilon.scala
similarity index 100%
rename from testcases/verification/xlang/buggyEpsilon.scala
rename to testcases/graveyard/verification/xlang/buggyEpsilon.scala
diff --git a/testcases/verification/xlang/master-thesis-regis/ArrayBubbleSort.scala b/testcases/graveyard/verification/xlang/master-thesis-regis/ArrayBubbleSort.scala
similarity index 100%
rename from testcases/verification/xlang/master-thesis-regis/ArrayBubbleSort.scala
rename to testcases/graveyard/verification/xlang/master-thesis-regis/ArrayBubbleSort.scala
diff --git a/testcases/verification/xlang/master-thesis-regis/ArrayOperations.scala b/testcases/graveyard/verification/xlang/master-thesis-regis/ArrayOperations.scala
similarity index 100%
rename from testcases/verification/xlang/master-thesis-regis/ArrayOperations.scala
rename to testcases/graveyard/verification/xlang/master-thesis-regis/ArrayOperations.scala
diff --git a/testcases/verification/xlang/master-thesis-regis/Constraints.scala b/testcases/graveyard/verification/xlang/master-thesis-regis/Constraints.scala
similarity index 100%
rename from testcases/verification/xlang/master-thesis-regis/Constraints.scala
rename to testcases/graveyard/verification/xlang/master-thesis-regis/Constraints.scala
diff --git a/testcases/verification/xlang/xplusone.scala b/testcases/graveyard/verification/xlang/xplusone.scala
similarity index 100%
rename from testcases/verification/xlang/xplusone.scala
rename to testcases/graveyard/verification/xlang/xplusone.scala
diff --git a/testcases/repair/Heap/Heap.scala b/testcases/repair/Heap/Heap.scala
index 5ceed2228..46be0f31a 100644
--- a/testcases/repair/Heap/Heap.scala
+++ b/testcases/repair/Heap/Heap.scala
@@ -4,8 +4,8 @@
* Date: 20.11.2013
**/
+import leon.lang._
import leon.collection._
-import leon._
object HeapSort {
diff --git a/testcases/repair/Heap/Heap1.scala b/testcases/repair/Heap/Heap1.scala
index b5d5b22d0..61ec4ac0f 100644
--- a/testcases/repair/Heap/Heap1.scala
+++ b/testcases/repair/Heap/Heap1.scala
@@ -4,8 +4,8 @@
* Date: 20.11.2013
**/
+import leon.lang._
import leon.collection._
-import leon._
object HeapSort {
diff --git a/testcases/repair/Heap/Heap10.scala b/testcases/repair/Heap/Heap10.scala
index 27a75d344..6847ed8cd 100644
--- a/testcases/repair/Heap/Heap10.scala
+++ b/testcases/repair/Heap/Heap10.scala
@@ -4,8 +4,8 @@
* Date: 20.11.2013
**/
+import leon.lang._
import leon.collection._
-import leon._
object HeapSort {
diff --git a/testcases/repair/Heap/Heap2.scala b/testcases/repair/Heap/Heap2.scala
index df7e82458..914fb0971 100644
--- a/testcases/repair/Heap/Heap2.scala
+++ b/testcases/repair/Heap/Heap2.scala
@@ -4,8 +4,8 @@
* Date: 20.11.2013
**/
+import leon.lang._
import leon.collection._
-import leon._
object HeapSort {
diff --git a/testcases/repair/Heap/Heap3.scala b/testcases/repair/Heap/Heap3.scala
index ebe8c85f2..2adde538b 100644
--- a/testcases/repair/Heap/Heap3.scala
+++ b/testcases/repair/Heap/Heap3.scala
@@ -4,8 +4,8 @@
* Date: 20.11.2013
**/
+import leon.lang._
import leon.collection._
-import leon._
object HeapSort {
diff --git a/testcases/repair/Heap/Heap4.scala b/testcases/repair/Heap/Heap4.scala
index a19ff6c20..ff78b3700 100644
--- a/testcases/repair/Heap/Heap4.scala
+++ b/testcases/repair/Heap/Heap4.scala
@@ -4,8 +4,8 @@
* Date: 20.11.2013
**/
+import leon.lang._
import leon.collection._
-import leon._
object HeapSort {
diff --git a/testcases/repair/Heap/Heap5.scala b/testcases/repair/Heap/Heap5.scala
index 33a3ff5aa..17777f85c 100644
--- a/testcases/repair/Heap/Heap5.scala
+++ b/testcases/repair/Heap/Heap5.scala
@@ -4,8 +4,8 @@
* Date: 20.11.2013
**/
+import leon.lang._
import leon.collection._
-import leon._
object HeapSort {
diff --git a/testcases/repair/Heap/Heap6.scala b/testcases/repair/Heap/Heap6.scala
index c9bf9d61a..a434b70c8 100644
--- a/testcases/repair/Heap/Heap6.scala
+++ b/testcases/repair/Heap/Heap6.scala
@@ -4,8 +4,8 @@
* Date: 20.11.2013
**/
+import leon.lang._
import leon.collection._
-import leon._
object HeapSort {
diff --git a/testcases/repair/Heap/Heap7.scala b/testcases/repair/Heap/Heap7.scala
index d4de52fe4..9de2a20b6 100644
--- a/testcases/repair/Heap/Heap7.scala
+++ b/testcases/repair/Heap/Heap7.scala
@@ -4,8 +4,8 @@
* Date: 20.11.2013
**/
+import leon.lang._
import leon.collection._
-import leon._
object HeapSort {
diff --git a/testcases/repair/Heap/Heap8.scala b/testcases/repair/Heap/Heap8.scala
index 83a75b7ae..6ee493600 100644
--- a/testcases/repair/Heap/Heap8.scala
+++ b/testcases/repair/Heap/Heap8.scala
@@ -4,8 +4,8 @@
* Date: 20.11.2013
**/
+import leon.lang._
import leon.collection._
-import leon._
object HeapSort {
diff --git a/testcases/repair/Heap/Heap9.scala b/testcases/repair/Heap/Heap9.scala
index 6846a9cae..55520379e 100644
--- a/testcases/repair/Heap/Heap9.scala
+++ b/testcases/repair/Heap/Heap9.scala
@@ -4,8 +4,8 @@
* Date: 20.11.2013
**/
+import leon.lang._
import leon.collection._
-import leon._
object HeapSort {
diff --git a/testcases/repair/List/List.scala b/testcases/repair/List/List.scala
index 19cf5ed3f..caa4aa0d3 100644
--- a/testcases/repair/List/List.scala
+++ b/testcases/repair/List/List.scala
@@ -4,6 +4,7 @@ package leon.custom
import leon._
import leon.lang._
+import leon.collection._
import leon.annotation._
sealed abstract class List0[T] {
diff --git a/testcases/repair/List/List1.scala b/testcases/repair/List/List1.scala
index 1e18ca898..9f600f728 100644
--- a/testcases/repair/List/List1.scala
+++ b/testcases/repair/List/List1.scala
@@ -4,6 +4,7 @@ package leon.custom
import leon._
import leon.lang._
+import leon.collection._
import leon.annotation._
sealed abstract class List0[T] {
diff --git a/testcases/repair/List/List10.scala b/testcases/repair/List/List10.scala
index 6ef82201b..1c4b0016a 100644
--- a/testcases/repair/List/List10.scala
+++ b/testcases/repair/List/List10.scala
@@ -4,6 +4,7 @@ package leon.custom
import leon._
import leon.lang._
+import leon.collection._
import leon.annotation._
sealed abstract class List0[T] {
diff --git a/testcases/repair/List/List11.scala b/testcases/repair/List/List11.scala
index ce946496e..7fe816b46 100644
--- a/testcases/repair/List/List11.scala
+++ b/testcases/repair/List/List11.scala
@@ -4,6 +4,7 @@ package leon.custom
import leon._
import leon.lang._
+import leon.collection._
import leon.annotation._
sealed abstract class List0[T] {
diff --git a/testcases/repair/List/List12.scala b/testcases/repair/List/List12.scala
index 63c1da6be..19f2d779e 100644
--- a/testcases/repair/List/List12.scala
+++ b/testcases/repair/List/List12.scala
@@ -4,6 +4,7 @@ package leon.custom
import leon._
import leon.lang._
+import leon.collection._
import leon.annotation._
sealed abstract class List0[T] {
diff --git a/testcases/repair/List/List13.scala b/testcases/repair/List/List13.scala
index 4dc3f2177..b585f3ef1 100644
--- a/testcases/repair/List/List13.scala
+++ b/testcases/repair/List/List13.scala
@@ -4,6 +4,7 @@ package leon.custom
import leon._
import leon.lang._
+import leon.collection._
import leon.annotation._
sealed abstract class List0[T] {
diff --git a/testcases/repair/List/List2.scala b/testcases/repair/List/List2.scala
index 5a000adc8..f83d1d222 100644
--- a/testcases/repair/List/List2.scala
+++ b/testcases/repair/List/List2.scala
@@ -4,6 +4,7 @@ package leon.custom
import leon._
import leon.lang._
+import leon.collection._
import leon.annotation._
sealed abstract class List0[T] {
diff --git a/testcases/repair/List/List3.scala b/testcases/repair/List/List3.scala
index 87a1214c7..1ad7ef0fd 100644
--- a/testcases/repair/List/List3.scala
+++ b/testcases/repair/List/List3.scala
@@ -4,6 +4,7 @@ package leon.custom
import leon._
import leon.lang._
+import leon.collection._
import leon.annotation._
sealed abstract class List0[T] {
diff --git a/testcases/repair/List/List4.scala b/testcases/repair/List/List4.scala
index 6bee40d15..0b641cd80 100644
--- a/testcases/repair/List/List4.scala
+++ b/testcases/repair/List/List4.scala
@@ -4,6 +4,7 @@ package leon.custom
import leon._
import leon.lang._
+import leon.collection._
import leon.annotation._
sealed abstract class List0[T] {
diff --git a/testcases/repair/List/List5.scala b/testcases/repair/List/List5.scala
index 46e6e4d50..34ae1877d 100644
--- a/testcases/repair/List/List5.scala
+++ b/testcases/repair/List/List5.scala
@@ -4,6 +4,7 @@ package leon.custom
import leon._
import leon.lang._
+import leon.collection._
import leon.annotation._
sealed abstract class List0[T] {
diff --git a/testcases/repair/List/List6.scala b/testcases/repair/List/List6.scala
index 028f94109..2e1297cb4 100644
--- a/testcases/repair/List/List6.scala
+++ b/testcases/repair/List/List6.scala
@@ -4,6 +4,7 @@ package leon.custom
import leon._
import leon.lang._
+import leon.collection._
import leon.annotation._
sealed abstract class List0[T] {
diff --git a/testcases/repair/List/List7.scala b/testcases/repair/List/List7.scala
index 3faa418ba..069dd35d2 100644
--- a/testcases/repair/List/List7.scala
+++ b/testcases/repair/List/List7.scala
@@ -4,6 +4,7 @@ package leon.custom
import leon._
import leon.lang._
+import leon.collection._
import leon.annotation._
sealed abstract class List0[T] {
diff --git a/testcases/repair/List/List8.scala b/testcases/repair/List/List8.scala
index f7c431cfe..bf99c2e75 100644
--- a/testcases/repair/List/List8.scala
+++ b/testcases/repair/List/List8.scala
@@ -4,6 +4,7 @@ package leon.custom
import leon._
import leon.lang._
+import leon.collection._
import leon.annotation._
sealed abstract class List0[T] {
diff --git a/testcases/repair/List/List9.scala b/testcases/repair/List/List9.scala
index 6969f2f91..59d05b6c5 100644
--- a/testcases/repair/List/List9.scala
+++ b/testcases/repair/List/List9.scala
@@ -4,6 +4,7 @@ package leon.custom
import leon._
import leon.lang._
+import leon.collection._
import leon.annotation._
sealed abstract class List0[T] {
diff --git a/testcases/repair/MergeSort/MergeSort1.scala b/testcases/repair/MergeSort/MergeSort1.scala
index f8515bade..901d4c6a2 100644
--- a/testcases/repair/MergeSort/MergeSort1.scala
+++ b/testcases/repair/MergeSort/MergeSort1.scala
@@ -1,3 +1,5 @@
+import leon.lang._
+
object MergeSort {
abstract class List {
diff --git a/testcases/repair/RedBlackTree/RedBlackTree.scala b/testcases/repair/RedBlackTree/RedBlackTree.scala
index d80fafc08..8bf916e87 100644
--- a/testcases/repair/RedBlackTree/RedBlackTree.scala
+++ b/testcases/repair/RedBlackTree/RedBlackTree.scala
@@ -1,5 +1,5 @@
-import leon._
-import lang._
+import leon.lang._
+import leon.collection._
import annotation._
object RedBlackTree {
diff --git a/testcases/repair/RedBlackTree/RedBlackTree1.scala b/testcases/repair/RedBlackTree/RedBlackTree1.scala
index d219c0094..c19819441 100644
--- a/testcases/repair/RedBlackTree/RedBlackTree1.scala
+++ b/testcases/repair/RedBlackTree/RedBlackTree1.scala
@@ -1,5 +1,5 @@
-import leon._
-import lang._
+import leon.lang._
+import leon.collection._
import annotation._
object RedBlackTree {
diff --git a/testcases/repair/RedBlackTree/RedBlackTree2.scala b/testcases/repair/RedBlackTree/RedBlackTree2.scala
index 7f0c029c8..a02dcb6f4 100644
--- a/testcases/repair/RedBlackTree/RedBlackTree2.scala
+++ b/testcases/repair/RedBlackTree/RedBlackTree2.scala
@@ -1,5 +1,5 @@
-import leon._
-import lang._
+import leon.lang._
+import leon.collection._
import annotation._
object RedBlackTree {
diff --git a/testcases/repair/RedBlackTree/RedBlackTree3.scala b/testcases/repair/RedBlackTree/RedBlackTree3.scala
index a5d561985..ffacf352e 100644
--- a/testcases/repair/RedBlackTree/RedBlackTree3.scala
+++ b/testcases/repair/RedBlackTree/RedBlackTree3.scala
@@ -1,5 +1,5 @@
-import leon._
-import lang._
+import leon.lang._
+import leon.collection._
import annotation._
object RedBlackTree {
diff --git a/testcases/repair/RedBlackTree/RedBlackTree6.scala b/testcases/repair/RedBlackTree/RedBlackTree6.scala
index 9eed1ac3a..82e0372d5 100644
--- a/testcases/repair/RedBlackTree/RedBlackTree6.scala
+++ b/testcases/repair/RedBlackTree/RedBlackTree6.scala
@@ -1,5 +1,5 @@
-import leon._
-import lang._
+import leon.lang._
+import leon.collection._
import annotation._
object RedBlackTree {
diff --git a/testcases/repair/inria/FirstIndexOf.scala b/testcases/repair/inria/FirstIndexOf.scala
index d59131506..2693d18cd 100644
--- a/testcases/repair/inria/FirstIndexOf.scala
+++ b/testcases/repair/inria/FirstIndexOf.scala
@@ -4,7 +4,7 @@ import leon.lang.synthesis._
object FirstIndexOf {
- def firstIndexOf(l: List[Int], v: Int): Int = {
+ def firstIndexOf(l: List[Int], v: Int): BigInt = {
l match {
case Cons(h, t) if v == h => 0
case Cons(h, t) =>
@@ -17,7 +17,7 @@ object FirstIndexOf {
-1
}
} ensuring {
- (res: Int) => (if (l.content contains v) {
+ (res: BigInt) => (if (l.content contains v) {
l.size > res && l.apply(res) == v
} else {
res == -1
diff --git a/testcases/repair/inria/HeapSort.scala b/testcases/repair/inria/HeapSort.scala
index 5ceed2228..46be0f31a 100644
--- a/testcases/repair/inria/HeapSort.scala
+++ b/testcases/repair/inria/HeapSort.scala
@@ -4,8 +4,8 @@
* Date: 20.11.2013
**/
+import leon.lang._
import leon.collection._
-import leon._
object HeapSort {
diff --git a/testcases/synthesis/NewYearsSong.scala b/testcases/synthesis/NewYearsSong.scala
deleted file mode 100644
index 0bcdf0130..000000000
--- a/testcases/synthesis/NewYearsSong.scala
+++ /dev/null
@@ -1,28 +0,0 @@
-import leon.lang.synthesis._
-import leon.annotation._
-import leon.lang._
-
-object NewYearSong {
-
- def computeLines(eLines: Int,
- iLines: Int,
- iSyls: Int,
- nSyls: Int) : (Int,Int,Int,Int,Int,Int) = {
- choose((line7: Int,
- line8: Int,
- nsLines: Int,
- nLines: Int,
- tLines: Int,
- tLinesFact: Int) => (
- tLines == eLines + nLines
- && nLines == iLines + nsLines
- && nLines == line7 + line8
- && nSyls + iSyls == 7 * line7 + 8 * line8
- && tLines == 4 * tLinesFact // expresses (4 | tLines)
- && line8 >= 0
- && line7 >= 0
- && tLines >= 0
- ))
- }
-
-}
diff --git a/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
index b966885e6..64a8ae73d 100644
--- a/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
+++ b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
@@ -1,4 +1,5 @@
-import scala.collection.immutable.Set
+import leon.lang._
+import leon.collection._
import leon.lang._
diff --git a/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala
index 467fc66df..c0697de3f 100644
--- a/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala
+++ b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.collection._
object BatchedQueue {
sealed abstract class List
diff --git a/testcases/synthesis/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala b/testcases/synthesis/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala
index 2e3f168a3..bcc6d17ab 100644
--- a/testcases/synthesis/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala
+++ b/testcases/synthesis/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/synthesis/condabd/benchmarks/List/ListSearch.scala b/testcases/synthesis/condabd/benchmarks/List/ListSearch.scala
deleted file mode 100644
index 240a5f009..000000000
--- a/testcases/synthesis/condabd/benchmarks/List/ListSearch.scala
+++ /dev/null
@@ -1,50 +0,0 @@
-import leon.lang._
-
-object ListOperations {
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil() extends List
-
- sealed abstract class Option
- case class Some(i: Int) extends Option
- case object None extends Option
-
- def content(l: List) : Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(head, tail) => Set(head) ++ content(tail)
- }
-
- def size(l: List) : Int = l match {
- case Nil() => 0
- case Cons(head, tail) => 1 + size(tail)
- }
-//
-// def isEmpty(l: List) = l match {
-// case Nil() => true
-// case Cons(_, _) => false
-// }
-
-
- def linearSearch(l: List, c: Int): Option = {
- l match {
- case Nil() => None
- case Cons(lHead, lTail) =>
- if (lHead == c) Some(size(l))
- else Some(linearSearch(lTail, c))
- }
- } ensuring(res => if(res > -1) atInd(l, size(l) - res) == c else !content(l).contains(c))
-
- def atInd(l: List, ind: Int): Int = {
- require(ind >= 0 && ind < size(l))
-
- l match {
- case Nil() => -1
- case Cons(lHead, lTail) =>
- if (ind == 0) lHead
- else atInd(lTail, ind - 1)
- }
-
- } ensuring( res =>
- if (size(l) == 0) res == -1 else content(l).contains(res)
- )
-}
diff --git a/testcases/synthesis/condabd/benchmarks/MergeSort/MergeSortMerge.scala b/testcases/synthesis/condabd/benchmarks/MergeSort/MergeSortMerge.scala
index 1fadb1d80..ad20d41b2 100644
--- a/testcases/synthesis/condabd/benchmarks/MergeSort/MergeSortMerge.scala
+++ b/testcases/synthesis/condabd/benchmarks/MergeSort/MergeSortMerge.scala
@@ -30,7 +30,7 @@ object MergeSort {
def merge(aList : List, bList : List) : List = {
require(isSorted(aList) && isSorted(bList))
choose( (res: List) =>
- ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+ contents(res) == contents(aList) ++ contents(bList) && isSorted(res)
)
}
diff --git a/testcases/synthesis/insynth-leon-tests/Arguments.scala b/testcases/synthesis/insynth-leon-tests/Arguments.scala
deleted file mode 100644
index 75b4eceaa..000000000
--- a/testcases/synthesis/insynth-leon-tests/Arguments.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-import leon.annotation._
-import leon.lang._
-
-object Hole {
-
- def method(t: Int, x: Boolean, y: Boolean) : Int = ({
- if (t > 5)
- hole(5)
- else
- t
- }) ensuring ( _ > 0 )
-
-}
diff --git a/testcases/synthesis/io-examples/List.scala b/testcases/synthesis/io-examples/List.scala
index 01214c727..0e2d2b0fd 100644
--- a/testcases/synthesis/io-examples/List.scala
+++ b/testcases/synthesis/io-examples/List.scala
@@ -9,11 +9,11 @@ object Foo {
//Cons[Int](i, l).slice(0, i)
???[List[Int]]
} ensuring { (res: List[Int]) =>
- passes((l, i), res)(Map[(List[Int], Int), List[Int]](
- (Nil[Int](), 2) -> Cons(2, Nil[Int]()),
- (Cons(1, Nil()), 2) -> Cons(2, Cons(1, Nil())),
- (Cons(1, Cons(2, Cons(3, Nil()))), 3) -> Cons(3, Cons(1, Cons(2, Nil())))
- ))
+ ((l, i), res) passes {
+ case (Nil(), 2) => Cons(2, Nil[Int]())
+ case (Cons(1, Nil()), 2) => Cons(2, Cons(1, Nil()))
+ case (Cons(1, Cons(2, Cons(3, Nil()))), 3) => Cons(3, Cons(1, Cons(2, Nil())))
+ }
}
}
diff --git a/testcases/synthesis/io-examples/Lists.scala b/testcases/synthesis/io-examples/Lists.scala
index 62335cc36..7d3d068e0 100644
--- a/testcases/synthesis/io-examples/Lists.scala
+++ b/testcases/synthesis/io-examples/Lists.scala
@@ -5,18 +5,18 @@ import leon.lang.synthesis._
object Lists {
def safetail(l: List[Int]): List[Int] = choose { (res : List[Int]) =>
- passes(l, res)(Map(
- Cons(1, Cons(2, Cons(3, Cons(4, Nil())))) -> Cons(2, Cons(3, Cons(4, Nil()))),
- Cons(2, Cons(3, Cons(4, Nil()))) -> Cons(3, Cons(4, Nil())),
- Nil() -> Nil()
- ))
+ (l, res) passes {
+ case Cons(1, Cons(2, Cons(3, Cons(4, Nil())))) => Cons(2, Cons(3, Cons(4, Nil())))
+ case Cons(2, Cons(3, Cons(4, Nil()))) => Cons(3, Cons(4, Nil()))
+ case Nil() => Nil()
+ }
}
def uniq(l: List[Int]): List[Int] = choose { (res : List[Int]) =>
- passes(l, res)(Map(
- Cons(1, Cons(1, Cons(1, Cons(2, Nil())))) -> Cons(1, Cons(2, Nil())),
- Cons(3, Cons(3, Cons(4, Nil()))) -> Cons(3, Cons(4, Nil())),
- Nil() -> Nil()
- ))
+ (l, res) passes {
+ case Cons(1, Cons(1, Cons(1, Cons(2, Nil())))) => Cons(1, Cons(2, Nil()))
+ case Cons(3, Cons(3, Cons(4, Nil()))) => Cons(3, Cons(4, Nil()))
+ case Nil() => Nil()
+ }
}
}
diff --git a/testcases/synthesis/io-examples/Math.scala b/testcases/synthesis/io-examples/Math.scala
index df68735e3..2e50289d6 100644
--- a/testcases/synthesis/io-examples/Math.scala
+++ b/testcases/synthesis/io-examples/Math.scala
@@ -10,25 +10,17 @@ object Math {
} else {
???[Int]
}
- } ensuring {
- passes(a, _)(Map(
- 0 -> 0,
- 1 -> 1,
- 2 -> 1,
- 3 -> 2,
- 4 -> 3,
- 5 -> 5,
- 18 -> 2584
- ))
- }
-
- def abs(a: Int): Int = {
- if (?(a >= 0, a <= 0, a == 0, a != 0)) {
- a
- } else {
- -a
+ } ensuring { res =>
+ (a, res) passes {
+ case 0 => 0
+ case 1 => 1
+ case 2 => 1
+ case 3 => 2
+ case 4 => 3
+ case 5 => 5
+ case 18 => 2584
}
- } ensuring { _ >= 0 }
+ }
diff --git a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala
deleted file mode 100644
index 7dbb6bfc3..000000000
--- a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala
+++ /dev/null
@@ -1,91 +0,0 @@
-import scala.collection.immutable.Set
-
-import leon.lang._
-
-object BatchedQueue {
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case object Nil extends List
-
- def content(l: List): Set[Int] = l match {
- case Nil => Set.empty
- case Cons(head, tail) => Set(head) ++ content(tail)
- }
-
- def content(p: Queue): Set[Int] =
- content(p.f) ++ content(p.r)
-
- case class Queue(f: List, r: List)
-
- def rev_append(aList: List, bList: List): List = (aList match {
- case Nil => bList
- case Cons(x, xs) => rev_append(xs, Cons(x, bList))
- }) ensuring (
- res =>
- content(res) == content(aList) ++ content(bList) &&
- size(res) == size(aList) + size(bList)
- )
-
- def invariantList(q:Queue, f: List, r: List): Boolean = ({
- rev_append(q.f, q.r) == rev_append(f, r)
- }) ensuring (
- res =>
- true
- )
-
- def reverse(list: List) = rev_append(list, Nil) ensuring (
- res =>
- content(res) == content(list) && size(res) == size(list)
- )
-
- def checkf(f: List, r: List): Queue = (f match {
- case Nil => Queue(reverse(r), Nil)
- case _ => Queue(f, r)
- }) ensuring {
- res => content(res) == content(f) ++ content(r) &&
- size(res) == size(f) + size(r) &&
- invariantList(res, f, r)
- }
-
- def head(p: Queue): Set[Int] = (
- p.f match {
- case Nil => Set[Int]()
- case Cons(x, xs) => Set(x)
- }) ensuring (
- res =>
- if (isEmpty(p)) true
- else content(p) == res ++ content(tail(p)))
-
- def tail(p: Queue): Queue = {
- require(!isEmpty(p))
- p.f match {
- case Nil => p
- case Cons(_, xs) => checkf(xs, p.r)
- }
- } ensuring {
- (res: Queue) => content(res) ++ head(p) == content(p) &&
- (if (isEmpty(p)) true
- else size(res) + 1 == size(p))
- }
- //
- // def last(p: Queue): Int = {
- // require(!isEmpty(p))
- // p.r match {
- // case Nil => reverse(p.f).asInstanceOf[Cons].head
- // case Cons(x, _) => x
- // }
- // }
-
- def snoc(p: Queue, x: Int): Queue =
- checkf(p.f, Cons(x, p.r)) ensuring (
- res =>
- content(res) == content(p) ++ Set(x) &&
- size(res) == size(p) + 1 &&
- (
- if (isEmpty(p)) true
- else (content(tail(res)) ++ Set(x) == content(tail(res)) &&
- size(res.f) == size(p.f))
- )
- )
-
-}
diff --git a/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala b/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala
deleted file mode 100644
index 310b7e7e2..000000000
--- a/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala
+++ /dev/null
@@ -1,48 +0,0 @@
-import scala.collection.immutable.Set
-import leon.annotation._
-import leon.lang._
-
-object InsertionSort {
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil() extends List
-
- def size(l: List): Int = (l match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- }) ensuring (_ >= 0)
-
- def contents(l: List): Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(x, xs) => contents(xs) ++ Set(x)
- }
-
- def isSorted(l: List): Boolean = l match {
- case Nil() => true
- case Cons(x, Nil()) => true
- case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
- }
-
- /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
- * the expected content and size */
- def insert(e: Int, l: List): List = {
- l match {
- case Nil() => Cons(e, Nil())
- case Cons(x, xs) =>
- if (x <= e) Cons(x, sortedIns(e, xs))
- else Cons(e, l)
- }
- } ensuring (res => contents(res) == contents(l) ++ Set(e)
- && isSorted(res)
- && size(res) == size(l) + 1)
-
- /* Insertion sort yields a sorted list of same size and content as the input
- * list */
- def sort(l: List): List = (l match {
- case Nil() => Nil()
- case Cons(x, xs) => sortedIns(x, sort(xs))
- }) ensuring (res => contents(res) == contents(l)
- && isSorted(res)
- && size(res) == size(l))
-
-}
diff --git a/testcases/synthesis/oopsla2013/MergeSort/Complete.scala b/testcases/synthesis/oopsla2013/MergeSort/Complete.scala
index 062578c96..326295aaf 100644
--- a/testcases/synthesis/oopsla2013/MergeSort/Complete.scala
+++ b/testcases/synthesis/oopsla2013/MergeSort/Complete.scala
@@ -1,5 +1,3 @@
-import scala.collection.immutable.Set
-
import leon.lang._
object MergeSort {
diff --git a/testcases/synthesis/oopsla2013/SortedList/Batch.scala b/testcases/synthesis/oopsla2013/SortedList/Batch.scala
index 35e60c8d8..8da614143 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Batch.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Batch.scala
@@ -47,7 +47,7 @@ object SortedList {
choose {
(out : List) =>
- && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ (content(out) == content(in1) ++ content(in2)) && isSorted(out)
}
}
@@ -56,7 +56,7 @@ object SortedList {
choose {
(out : List) =>
- && (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ (content(out) == content(in1) -- content(in2)) && isSorted(out)
}
}
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Complete.scala b/testcases/synthesis/oopsla2013/SparseVector/Complete.scala
index 2cf542ae5..8683e0b5a 100644
--- a/testcases/synthesis/oopsla2013/SparseVector/Complete.scala
+++ b/testcases/synthesis/oopsla2013/SparseVector/Complete.scala
@@ -107,7 +107,7 @@ object SparseVector {
case Nil =>
None
}
- } ensuring { res => ((indices(sv) contains at) == isDefined(res)) && (!isDefined(res) || (values(sv) contains valueOf(res)) }
+ } ensuring { res => ((indices(sv) contains at) == isDefined(res)) && (!isDefined(res) || (values(sv) contains valueOf(res))) }
// def get(sv: SparseVector, at: Int): Option = choose {
// (res: Option) => invariant(sv) && ((indices(sv) contains at) == isDefined(res)) && (!isDefined(res) || (values(sv) contains valueOf(res)))
diff --git a/testcases/verification/Addresses.scala b/testcases/verification/Addresses.scala
index cd089c44c..bc6ad57b8 100644
--- a/testcases/verification/Addresses.scala
+++ b/testcases/verification/Addresses.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/datastructures/BinarySearchTree.scala b/testcases/verification/datastructures/BinarySearchTree.scala
index 471813c13..ef87a00ea 100644
--- a/testcases/verification/datastructures/BinarySearchTree.scala
+++ b/testcases/verification/datastructures/BinarySearchTree.scala
@@ -1,3 +1,6 @@
+import leon.lang._
+import leon.collection._
+
object BSTSimpler {
sealed abstract class Tree
case class Node(left: Tree, value: Int, right: Tree) extends Tree
diff --git a/testcases/verification/datastructures/BinarySearchTreeSorted.scala b/testcases/verification/datastructures/BinarySearchTreeSorted.scala
index 464335f62..577e0e6a0 100644
--- a/testcases/verification/datastructures/BinarySearchTreeSorted.scala
+++ b/testcases/verification/datastructures/BinarySearchTreeSorted.scala
@@ -1,6 +1,6 @@
import leon.lang._
import leon.annotation._
-import leon._
+import leon.collection._
object BinaryTree {
sealed abstract class Tree
diff --git a/testcases/verification/datastructures/InsertionSort.scala b/testcases/verification/datastructures/InsertionSort.scala
index 1781531cb..fcb2b94d5 100644
--- a/testcases/verification/datastructures/InsertionSort.scala
+++ b/testcases/verification/datastructures/InsertionSort.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
object InsertionSort {
diff --git a/testcases/verification/datastructures/ListWithSize.scala b/testcases/verification/datastructures/ListWithSize.scala
index 660f09a43..d826eae58 100644
--- a/testcases/verification/datastructures/ListWithSize.scala
+++ b/testcases/verification/datastructures/ListWithSize.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/datastructures/MergeSort.scala b/testcases/verification/datastructures/MergeSort.scala
index 408830ced..1bbd7f607 100644
--- a/testcases/verification/datastructures/MergeSort.scala
+++ b/testcases/verification/datastructures/MergeSort.scala
@@ -1,4 +1,4 @@
-import scala.collection.immutable.Set
+import leon.lang._
object MergeSort {
sealed abstract class List
diff --git a/testcases/verification/datastructures/QuickSort.scala b/testcases/verification/datastructures/QuickSort.scala
index a5f03f214..cb193d2c8 100644
--- a/testcases/verification/datastructures/QuickSort.scala
+++ b/testcases/verification/datastructures/QuickSort.scala
@@ -1,4 +1,4 @@
-import scala.collection.immutable.Set
+import leon.lang._
object QuickSort {
sealed abstract class List
diff --git a/testcases/verification/datastructures/RedBlackTree.scala b/testcases/verification/datastructures/RedBlackTree.scala
index 98a70c191..eb998becb 100644
--- a/testcases/verification/datastructures/RedBlackTree.scala
+++ b/testcases/verification/datastructures/RedBlackTree.scala
@@ -1,5 +1,4 @@
-import scala.collection.immutable.Set
-//import scala.collection.immutable.Multiset
+import leon.lang._
object RedBlackTree {
sealed abstract class Color
diff --git a/testcases/verification/datastructures/SortedList.scala b/testcases/verification/datastructures/SortedList.scala
index 41451641b..91b3e2af3 100644
--- a/testcases/verification/datastructures/SortedList.scala
+++ b/testcases/verification/datastructures/SortedList.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/datastructures/TreeListSetNoDup.scala b/testcases/verification/datastructures/TreeListSetNoDup.scala
index 44d7fcf0b..ef72d3a68 100644
--- a/testcases/verification/datastructures/TreeListSetNoDup.scala
+++ b/testcases/verification/datastructures/TreeListSetNoDup.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/graph/MST/MSTMap.scala b/testcases/verification/graph/MST/MSTMap.scala
index da2a08fc0..1ef72da32 100644
--- a/testcases/verification/graph/MST/MSTMap.scala
+++ b/testcases/verification/graph/MST/MSTMap.scala
@@ -1,5 +1,3 @@
-import scala.collection.immutable._
-
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/graph/SortedNDList.scala b/testcases/verification/graph/SortedNDList.scala
index 98c06e7c9..42a16cfbd 100644
--- a/testcases/verification/graph/SortedNDList.scala
+++ b/testcases/verification/graph/SortedNDList.scala
@@ -1,5 +1,3 @@
-import scala.collection.immutable._
-
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/graph/Subgraph.scala b/testcases/verification/graph/Subgraph.scala
index 2f60f78f0..5e1781137 100644
--- a/testcases/verification/graph/Subgraph.scala
+++ b/testcases/verification/graph/Subgraph.scala
@@ -1,5 +1,3 @@
-import scala.collection.immutable._
-
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/graph/SubgraphMap.scala b/testcases/verification/graph/SubgraphMap.scala
index 90522ba9c..3714d2eb7 100644
--- a/testcases/verification/graph/SubgraphMap.scala
+++ b/testcases/verification/graph/SubgraphMap.scala
@@ -1,5 +1,3 @@
-import scala.collection.immutable._
-
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/graph/TreeEquivalence.scala b/testcases/verification/graph/TreeEquivalence.scala
index c059473ea..a12c82ed3 100644
--- a/testcases/verification/graph/TreeEquivalence.scala
+++ b/testcases/verification/graph/TreeEquivalence.scala
@@ -1,5 +1,3 @@
-import scala.collection.immutable._
-
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/graph/TreeEquivalenceMap.scala b/testcases/verification/graph/TreeEquivalenceMap.scala
index e0dd4bca5..7c4a1103c 100644
--- a/testcases/verification/graph/TreeEquivalenceMap.scala
+++ b/testcases/verification/graph/TreeEquivalenceMap.scala
@@ -1,5 +1,3 @@
-import scala.collection.immutable._
-
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala b/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala
index d3958a893..20461a256 100644
--- a/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala
+++ b/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala
@@ -1,5 +1,3 @@
-import scala.collection.immutable._
-
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/higher-order/invalid/Continuations1.scala b/testcases/verification/higher-order/invalid/Continuations1.scala
index 82f4bdea4..0d65fc817 100644
--- a/testcases/verification/higher-order/invalid/Continuations1.scala
+++ b/testcases/verification/higher-order/invalid/Continuations1.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.collection._
object Continuations1 {
def add_cps[T](x: BigInt, y: BigInt)(f: BigInt => T): T = {
diff --git a/testcases/verification/higher-order/invalid/HOInvocations.scala b/testcases/verification/higher-order/invalid/HOInvocations.scala
index 3d2e16835..bf1f40a43 100644
--- a/testcases/verification/higher-order/invalid/HOInvocations.scala
+++ b/testcases/verification/higher-order/invalid/HOInvocations.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.collection._
object HOInvocations {
def switch(x: Int, f: (Int) => Int, g: (Int) => Int) = if(x > 0) f else g
diff --git a/testcases/verification/higher-order/invalid/Lists1.scala b/testcases/verification/higher-order/invalid/Lists1.scala
index e7582fad6..7fc938a51 100644
--- a/testcases/verification/higher-order/invalid/Lists1.scala
+++ b/testcases/verification/higher-order/invalid/Lists1.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.collection._
object Lists1 {
abstract class List[T]
diff --git a/testcases/verification/higher-order/invalid/Lists2.scala b/testcases/verification/higher-order/invalid/Lists2.scala
index 777223617..59faa779b 100644
--- a/testcases/verification/higher-order/invalid/Lists2.scala
+++ b/testcases/verification/higher-order/invalid/Lists2.scala
@@ -1,6 +1,4 @@
-import leon._
import leon.lang._
-import leon.annotation._
import leon.collection._
diff --git a/testcases/verification/higher-order/invalid/ParBalance.scala b/testcases/verification/higher-order/invalid/ParBalance.scala
index 4a2a93c23..62eca559d 100644
--- a/testcases/verification/higher-order/invalid/ParBalance.scala
+++ b/testcases/verification/higher-order/invalid/ParBalance.scala
@@ -1,5 +1,5 @@
-import leon._
import leon.lang._
+import leon.collection._
object ParBalance {
diff --git a/testcases/verification/higher-order/invalid/PositiveMap.scala b/testcases/verification/higher-order/invalid/PositiveMap.scala
index fb1452f47..7fb002360 100644
--- a/testcases/verification/higher-order/invalid/PositiveMap.scala
+++ b/testcases/verification/higher-order/invalid/PositiveMap.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.collection._
object PositiveMap {
diff --git a/testcases/verification/higher-order/invalid/Sets1.scala b/testcases/verification/higher-order/invalid/Sets1.scala
index 45545c356..62d1409b0 100644
--- a/testcases/verification/higher-order/invalid/Sets1.scala
+++ b/testcases/verification/higher-order/invalid/Sets1.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.collection._
object Sets1 {
def set(i: Int): Int => Boolean = x => x == i
diff --git a/testcases/verification/higher-order/invalid/Transformation.scala b/testcases/verification/higher-order/invalid/Transformation.scala
index 83c265aee..9c9bf86bc 100644
--- a/testcases/verification/higher-order/invalid/Transformation.scala
+++ b/testcases/verification/higher-order/invalid/Transformation.scala
@@ -1,5 +1,5 @@
-import leon._
import leon.lang._
+import leon.collection._
object Transformation {
diff --git a/testcases/verification/pldi2011-testcases/AssociativeList.scala b/testcases/verification/pldi2011-testcases/AssociativeList.scala
index 2b99141b2..5f5dd8ae1 100644
--- a/testcases/verification/pldi2011-testcases/AssociativeList.scala
+++ b/testcases/verification/pldi2011-testcases/AssociativeList.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/pldi2011-testcases/ForElimination.scala b/testcases/verification/pldi2011-testcases/ForElimination.scala
index fe9650133..0e478762b 100644
--- a/testcases/verification/pldi2011-testcases/ForElimination.scala
+++ b/testcases/verification/pldi2011-testcases/ForElimination.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/pldi2011-testcases/InsertionSort.scala b/testcases/verification/pldi2011-testcases/InsertionSort.scala
index 3e606fe8b..a201e6eb1 100644
--- a/testcases/verification/pldi2011-testcases/InsertionSort.scala
+++ b/testcases/verification/pldi2011-testcases/InsertionSort.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/pldi2011-testcases/LambdaEval.scala b/testcases/verification/pldi2011-testcases/LambdaEval.scala
index 4dde6b2bc..84ecf4737 100644
--- a/testcases/verification/pldi2011-testcases/LambdaEval.scala
+++ b/testcases/verification/pldi2011-testcases/LambdaEval.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/pldi2011-testcases/ListTree.scala b/testcases/verification/pldi2011-testcases/ListTree.scala
index 5057b155b..edcd48650 100644
--- a/testcases/verification/pldi2011-testcases/ListTree.scala
+++ b/testcases/verification/pldi2011-testcases/ListTree.scala
@@ -1,4 +1,4 @@
-import scala.collection.immutable.Set
+import leon.lang._
object ListTree {
/* Trees holding integers and internal lists */
diff --git a/testcases/verification/pldi2011-testcases/MergeSort.scala b/testcases/verification/pldi2011-testcases/MergeSort.scala
index 4e0121ac4..96e81e40e 100644
--- a/testcases/verification/pldi2011-testcases/MergeSort.scala
+++ b/testcases/verification/pldi2011-testcases/MergeSort.scala
@@ -1,4 +1,4 @@
-import scala.collection.immutable.Set
+import leon.lang._
object MergeSort {
sealed abstract class List
diff --git a/testcases/verification/pldi2011-testcases/PropositionalLogic.scala b/testcases/verification/pldi2011-testcases/PropositionalLogic.scala
index 0270bdf87..8356d2cbf 100644
--- a/testcases/verification/pldi2011-testcases/PropositionalLogic.scala
+++ b/testcases/verification/pldi2011-testcases/PropositionalLogic.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/pldi2011-testcases/QuickSort.scala b/testcases/verification/pldi2011-testcases/QuickSort.scala
index a0a151057..30b362143 100644
--- a/testcases/verification/pldi2011-testcases/QuickSort.scala
+++ b/testcases/verification/pldi2011-testcases/QuickSort.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/pldi2011-testcases/RedBlackTree.scala b/testcases/verification/pldi2011-testcases/RedBlackTree.scala
index 3ebfa25e2..c7f380df8 100644
--- a/testcases/verification/pldi2011-testcases/RedBlackTree.scala
+++ b/testcases/verification/pldi2011-testcases/RedBlackTree.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/pldi2011-testcases/RedBlackTreeDeletion.scala b/testcases/verification/pldi2011-testcases/RedBlackTreeDeletion.scala
index 585135d06..fed0247b6 100644
--- a/testcases/verification/pldi2011-testcases/RedBlackTreeDeletion.scala
+++ b/testcases/verification/pldi2011-testcases/RedBlackTreeDeletion.scala
@@ -1,4 +1,4 @@
-import scala.collection.immutable.Set
+import leon.lang._
import leon.annotation._
object RedBlackTree {
@@ -238,7 +238,7 @@ object RedBlackTree {
val maxV = max(l)
val newL = removeMax(l)
bubble(c, newL, maxV, r)
- case _ => throw new Exception("Removing an unexpected tree")
+ case _ => error[Tree]("Removing an unexpected tree")
}
} ensuring(res => hasRedBlackDesc(res))
diff --git a/testcases/verification/pldi2011-testcases/SemanticsPreservation.scala b/testcases/verification/pldi2011-testcases/SemanticsPreservation.scala
index 034ec1222..0a10b118d 100644
--- a/testcases/verification/pldi2011-testcases/SemanticsPreservation.scala
+++ b/testcases/verification/pldi2011-testcases/SemanticsPreservation.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/pldi2011-testcases/TreeMap.scala b/testcases/verification/pldi2011-testcases/TreeMap.scala
index 44b85cff7..ce6fd7f81 100644
--- a/testcases/verification/pldi2011-testcases/TreeMap.scala
+++ b/testcases/verification/pldi2011-testcases/TreeMap.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
object TreeMap {
diff --git a/testcases/verification/sas2011-testcases/AmortizedQueue.scala b/testcases/verification/sas2011-testcases/AmortizedQueue.scala
index a3636e00a..d5caf37ec 100644
--- a/testcases/verification/sas2011-testcases/AmortizedQueue.scala
+++ b/testcases/verification/sas2011-testcases/AmortizedQueue.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/sas2011-testcases/AssociativeList.scala b/testcases/verification/sas2011-testcases/AssociativeList.scala
index 6567c4786..3b4e954a8 100644
--- a/testcases/verification/sas2011-testcases/AssociativeList.scala
+++ b/testcases/verification/sas2011-testcases/AssociativeList.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/sas2011-testcases/InsertionSort.scala b/testcases/verification/sas2011-testcases/InsertionSort.scala
index b01d0ae2f..5c7419ce5 100644
--- a/testcases/verification/sas2011-testcases/InsertionSort.scala
+++ b/testcases/verification/sas2011-testcases/InsertionSort.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/sas2011-testcases/ListOperations.scala b/testcases/verification/sas2011-testcases/ListOperations.scala
index 2cba911ad..991febc57 100644
--- a/testcases/verification/sas2011-testcases/ListOperations.scala
+++ b/testcases/verification/sas2011-testcases/ListOperations.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/sas2011-testcases/PropositionalLogic.scala b/testcases/verification/sas2011-testcases/PropositionalLogic.scala
index ca410a5ae..efc8f8f87 100644
--- a/testcases/verification/sas2011-testcases/PropositionalLogic.scala
+++ b/testcases/verification/sas2011-testcases/PropositionalLogic.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/sas2011-testcases/RedBlackTree.scala b/testcases/verification/sas2011-testcases/RedBlackTree.scala
index e77838fff..0e6603209 100644
--- a/testcases/verification/sas2011-testcases/RedBlackTree.scala
+++ b/testcases/verification/sas2011-testcases/RedBlackTree.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/sas2011-testcases/SearchLinkedList.scala b/testcases/verification/sas2011-testcases/SearchLinkedList.scala
index 40f29050f..14e36d3e4 100644
--- a/testcases/verification/sas2011-testcases/SearchLinkedList.scala
+++ b/testcases/verification/sas2011-testcases/SearchLinkedList.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/scala2013/AmortizedQueue.scala b/testcases/verification/scala2013/AmortizedQueue.scala
index 52e4ed7e2..467a39d48 100644
--- a/testcases/verification/scala2013/AmortizedQueue.scala
+++ b/testcases/verification/scala2013/AmortizedQueue.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/scala2013/AmortizedQueueImp.scala b/testcases/verification/scala2013/AmortizedQueueImp.scala
index afaefbca1..fb3d54970 100644
--- a/testcases/verification/scala2013/AmortizedQueueImp.scala
+++ b/testcases/verification/scala2013/AmortizedQueueImp.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/scala2013/AssociativeList.scala b/testcases/verification/scala2013/AssociativeList.scala
index 6567c4786..3b4e954a8 100644
--- a/testcases/verification/scala2013/AssociativeList.scala
+++ b/testcases/verification/scala2013/AssociativeList.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/scala2013/AssociativeListImp.scala b/testcases/verification/scala2013/AssociativeListImp.scala
index d15101ec7..3810203c0 100644
--- a/testcases/verification/scala2013/AssociativeListImp.scala
+++ b/testcases/verification/scala2013/AssociativeListImp.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/scala2013/ListOperations.scala b/testcases/verification/scala2013/ListOperations.scala
index 86d0f522f..157c6b978 100644
--- a/testcases/verification/scala2013/ListOperations.scala
+++ b/testcases/verification/scala2013/ListOperations.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/scala2013/PropositionalLogic.scala b/testcases/verification/scala2013/PropositionalLogic.scala
index ca410a5ae..efc8f8f87 100644
--- a/testcases/verification/scala2013/PropositionalLogic.scala
+++ b/testcases/verification/scala2013/PropositionalLogic.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/scala2013/RedBlackTree.scala b/testcases/verification/scala2013/RedBlackTree.scala
index 11daef0b0..a65cc1f0f 100644
--- a/testcases/verification/scala2013/RedBlackTree.scala
+++ b/testcases/verification/scala2013/RedBlackTree.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/scala2013/SearchLinkedList.scala b/testcases/verification/scala2013/SearchLinkedList.scala
index 02f265f12..f85d51421 100644
--- a/testcases/verification/scala2013/SearchLinkedList.scala
+++ b/testcases/verification/scala2013/SearchLinkedList.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/vstte10competition/AmortizedQueue.scala b/testcases/verification/vstte10competition/AmortizedQueue.scala
index 696d92c40..4ba21d023 100644
--- a/testcases/verification/vstte10competition/AmortizedQueue.scala
+++ b/testcases/verification/vstte10competition/AmortizedQueue.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/vstte10competition/Injection.scala b/testcases/verification/vstte10competition/Injection.scala
deleted file mode 100644
index 22b9d2d25..000000000
--- a/testcases/verification/vstte10competition/Injection.scala
+++ /dev/null
@@ -1,78 +0,0 @@
-import scala.collection.immutable.Set
-import leon.lang._
-import leon.annotation._
-
-object Injection {
- sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
- case class Nil() extends List
-
- sealed abstract class OptionInt
- case class Some(value : Int) extends OptionInt
- case class None() extends OptionInt
-
- def size(list : List) : Int = (list match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- }) ensuring(_ >= 0)
-
- def content(list : List) : Set[Int] = list match {
- case Nil() => Set.empty[Int]
- case Cons(x, xs) => content(xs) ++ Set(x)
- }
-
- def completeSet(n : Int) : Set[Int] = if(n <= 0) {
- Set.empty[Int]
- } else {
- completeSet(n-1) ++ Set(n-1)
- }
-
- def at(list : List, i : Int) : OptionInt = {
- if(i < 0) None() else list match {
- case Nil() => None()
- case Cons(x, _) if i == 0 => Some(x)
- case Cons(_, xs) => at(xs, i - 1)
- }
- } ensuring(res => (res == None()) == (i < 0 || i >= size(list)))
-
- def reverse(l: List) : List = reverse0(l, Nil())
- def reverse0(l1: List, l2: List) : List = (l1 match {
- case Nil() => l2
- case Cons(x, xs) => reverse0(xs, Cons(x, l2))
- }) ensuring(res =>
- size(res) == size(l1) + size(l2) &&
- content(res) == content(l1) ++ content(l2))
-
- def isPermutation(list : List, n : Int) : Boolean = {
- n < 0 || (size(list) == n && content(list) == completeSet(n))
- }
- def prop0(list : List, n : Int) : Boolean = {
- require(n >= 0 && isPermutation(list, n))
- isPermutation(reverse(list), n)
- } holds
-
- def indexOf(e : Int, list : List) : Int = (list match {
- case Nil() => 0
- case Cons(x, xs) => if (x == e) 0 else 1 + indexOf(e, xs)
- }) ensuring(res => (res == size(list)) == !content(list).contains(e))
-
- // def invert(list : List, n : Int) : List = {
- // require(isPermutation(list, n))
- // list
- // } ensuring(res => isPermutation(res, n))
-
- def f(list : List) = f0(list, size(list)-1, Nil())
- def f0(list : List, c : Int, acc : List) : List = {
- require(isPermutation(list, size(list)) && c <= size(list))
- if(c < 0) {
- acc
- } else {
- f0(list, c-1, Cons(indexOf(c, list), acc))
- }
- } ensuring(res => content(acc) -- completeSet(n) == Set.empty)
-
- def main(args : Array[String]) : Unit = {
- val test = Cons(9, Cons(3, Cons(8, Cons(2, Cons(7, Cons(4, Cons(0, Cons(1, Cons(5, Cons(6, Nil()))))))))))
- println(f(test, size(test)))
- }
-}
diff --git a/testcases/verification/vstte10competition/SearchLinkedList.scala b/testcases/verification/vstte10competition/SearchLinkedList.scala
index 02f265f12..f85d51421 100644
--- a/testcases/verification/vstte10competition/SearchLinkedList.scala
+++ b/testcases/verification/vstte10competition/SearchLinkedList.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/testcases/verification/xlang/BinaryTreeImp.scala b/testcases/verification/xlang/BinaryTreeImp.scala
index 57542971b..b731586da 100644
--- a/testcases/verification/xlang/BinaryTreeImp.scala
+++ b/testcases/verification/xlang/BinaryTreeImp.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/xlang/BubbleFun.scala b/testcases/verification/xlang/BubbleFun.scala
index 4847fc8ac..a7c72648c 100644
--- a/testcases/verification/xlang/BubbleFun.scala
+++ b/testcases/verification/xlang/BubbleFun.scala
@@ -1,3 +1,5 @@
+import leon.lang._
+
object BubbleFun {
// --------------------- sort ----------------------
diff --git a/testcases/verification/xlang/InsertionSortImp.scala b/testcases/verification/xlang/InsertionSortImp.scala
index 67e37a686..0a53cb55f 100644
--- a/testcases/verification/xlang/InsertionSortImp.scala
+++ b/testcases/verification/xlang/InsertionSortImp.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/testcases/verification/xlang/IntOperations.scala b/testcases/verification/xlang/IntOperations.scala
index 98c9f9e5f..91b3b636c 100644
--- a/testcases/verification/xlang/IntOperations.scala
+++ b/testcases/verification/xlang/IntOperations.scala
@@ -1,3 +1,5 @@
+import leon.lang._
+
object IntOperations {
def sum(a: Int, b: Int) : Int = {
require(b >= 0)
--
GitLab