diff --git a/testcases/Abs.scala b/testcases/Abs.scala
deleted file mode 100644
index 52baf710140b76bf5edeeda52ef9e0da5385734f..0000000000000000000000000000000000000000
--- a/testcases/Abs.scala
+++ /dev/null
@@ -1,5 +0,0 @@
-object Abs {
-
-  def abs(x: Int): Int = (if(x < 0) -x else x) ensuring(_ >= 0)
-
-}
diff --git a/testcases/Account2.scala b/testcases/Account2.scala
deleted file mode 100644
index e6fb25ce8d840d45490db6c0eef55551f472609f..0000000000000000000000000000000000000000
--- a/testcases/Account2.scala
+++ /dev/null
@@ -1,22 +0,0 @@
-object Account2 {
-  sealed abstract class AccLike 
-  case class Acc(checking : Int, savings : Int) extends AccLike
-
-  def sameTotal(a1 : Acc, a2 : Acc) : Boolean = {
-    a1.checking + a1.savings == a2.checking + a2.savings
-  }
-  def notRed(a : Acc) : Boolean = {
-    a.checking >= 0 && a.savings >= 0
-  }
-
-  def toSavingsOk(x : Int, a : Acc) : Acc = {
-    require (notRed(a) && x >= 0 && a.checking >= x)
-    Acc(a.checking - x, a.savings + x)
-  } ensuring (res => (notRed(res) && sameTotal(a, res)))
-
-  def toSavingsBroken(x : Int, a : Acc) : Acc = {
-    require (notRed(a) && a.checking >= x)
-    Acc(a.checking - x, a.savings + x)
-  } ensuring (res => (notRed(res) && sameTotal(a, res)))
-
-}
diff --git a/testcases/etaps2011-testcases/FromReport.scala b/testcases/graveyard/etaps2011-testcases/FromReport.scala
similarity index 100%
rename from testcases/etaps2011-testcases/FromReport.scala
rename to testcases/graveyard/etaps2011-testcases/FromReport.scala
diff --git a/testcases/etaps2011-testcases/HeapSort.scala b/testcases/graveyard/etaps2011-testcases/HeapSort.scala
similarity index 100%
rename from testcases/etaps2011-testcases/HeapSort.scala
rename to testcases/graveyard/etaps2011-testcases/HeapSort.scala
diff --git a/testcases/etaps2011-testcases/LeftistHeap.scala b/testcases/graveyard/etaps2011-testcases/LeftistHeap.scala
similarity index 100%
rename from testcases/etaps2011-testcases/LeftistHeap.scala
rename to testcases/graveyard/etaps2011-testcases/LeftistHeap.scala
diff --git a/testcases/etaps2011-testcases/VCs.scala b/testcases/graveyard/etaps2011-testcases/VCs.scala
similarity index 100%
rename from testcases/etaps2011-testcases/VCs.scala
rename to testcases/graveyard/etaps2011-testcases/VCs.scala
diff --git a/testcases/etaps2011-testcases/VCsHARD.scala b/testcases/graveyard/etaps2011-testcases/VCsHARD.scala
similarity index 100%
rename from testcases/etaps2011-testcases/VCsHARD.scala
rename to testcases/graveyard/etaps2011-testcases/VCsHARD.scala
diff --git a/testcases/etaps2011-testcases/manual b/testcases/graveyard/etaps2011-testcases/manual
similarity index 100%
rename from testcases/etaps2011-testcases/manual
rename to testcases/graveyard/etaps2011-testcases/manual
diff --git a/testcases/testgen/Abs.scala b/testcases/graveyard/testgen/Abs.scala
similarity index 100%
rename from testcases/testgen/Abs.scala
rename to testcases/graveyard/testgen/Abs.scala
diff --git a/testcases/testgen/Abs2.scala b/testcases/graveyard/testgen/Abs2.scala
similarity index 100%
rename from testcases/testgen/Abs2.scala
rename to testcases/graveyard/testgen/Abs2.scala
diff --git a/testcases/testgen/Diamond.scala b/testcases/graveyard/testgen/Diamond.scala
similarity index 100%
rename from testcases/testgen/Diamond.scala
rename to testcases/graveyard/testgen/Diamond.scala
diff --git a/testcases/testgen/Imp.scala b/testcases/graveyard/testgen/Imp.scala
similarity index 100%
rename from testcases/testgen/Imp.scala
rename to testcases/graveyard/testgen/Imp.scala
diff --git a/testcases/testgen/ImpWaypoint.scala b/testcases/graveyard/testgen/ImpWaypoint.scala
similarity index 100%
rename from testcases/testgen/ImpWaypoint.scala
rename to testcases/graveyard/testgen/ImpWaypoint.scala
diff --git a/testcases/testgen/List.scala b/testcases/graveyard/testgen/List.scala
similarity index 100%
rename from testcases/testgen/List.scala
rename to testcases/graveyard/testgen/List.scala
diff --git a/testcases/testgen/MultiCall.scala b/testcases/graveyard/testgen/MultiCall.scala
similarity index 100%
rename from testcases/testgen/MultiCall.scala
rename to testcases/graveyard/testgen/MultiCall.scala
diff --git a/testcases/testgen/Sum.scala b/testcases/graveyard/testgen/Sum.scala
similarity index 100%
rename from testcases/testgen/Sum.scala
rename to testcases/graveyard/testgen/Sum.scala
diff --git a/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala b/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala
similarity index 100%
rename from testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala
rename to testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala
diff --git a/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala b/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala
similarity index 100%
rename from testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala
rename to testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala
diff --git a/testcases/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala b/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala
similarity index 100%
rename from testcases/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala
rename to testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueue.scala b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
similarity index 100%
rename from testcases/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
rename to testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueCheckf.scala b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueCheckf.scala
similarity index 100%
rename from testcases/condabd/benchmarks/BatchedQueue/BatchedQueueCheckf.scala
rename to testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueCheckf.scala
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala
similarity index 100%
rename from testcases/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala
rename to testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnoc.scala b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueSnoc.scala
similarity index 100%
rename from testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnoc.scala
rename to testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueSnoc.scala
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnocWeird.scala b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueSnocWeird.scala
similarity index 100%
rename from testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnocWeird.scala
rename to testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueSnocWeird.scala
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueTail.scala b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueTail.scala
similarity index 100%
rename from testcases/condabd/benchmarks/BatchedQueue/BatchedQueueTail.scala
rename to testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueTail.scala
diff --git a/testcases/condabd/benchmarks/BinarySearch.scala b/testcases/synthesis/condabd/benchmarks/BinarySearch.scala
similarity index 100%
rename from testcases/condabd/benchmarks/BinarySearch.scala
rename to testcases/synthesis/condabd/benchmarks/BinarySearch.scala
diff --git a/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala b/testcases/synthesis/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala
similarity index 100%
rename from testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala
rename to testcases/synthesis/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala
diff --git a/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeMember.scala b/testcases/synthesis/condabd/benchmarks/BinarySearchTree/BinarySearchTreeMember.scala
similarity index 100%
rename from testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeMember.scala
rename to testcases/synthesis/condabd/benchmarks/BinarySearchTree/BinarySearchTreeMember.scala
diff --git a/testcases/condabd/benchmarks/InsertionSort/InsertionSortInsert.scala b/testcases/synthesis/condabd/benchmarks/InsertionSort/InsertionSortInsert.scala
similarity index 100%
rename from testcases/condabd/benchmarks/InsertionSort/InsertionSortInsert.scala
rename to testcases/synthesis/condabd/benchmarks/InsertionSort/InsertionSortInsert.scala
diff --git a/testcases/condabd/benchmarks/InsertionSort/InsertionSortSort.scala b/testcases/synthesis/condabd/benchmarks/InsertionSort/InsertionSortSort.scala
similarity index 100%
rename from testcases/condabd/benchmarks/InsertionSort/InsertionSortSort.scala
rename to testcases/synthesis/condabd/benchmarks/InsertionSort/InsertionSortSort.scala
diff --git a/testcases/condabd/benchmarks/List/ListConcat.scala b/testcases/synthesis/condabd/benchmarks/List/ListConcat.scala
similarity index 100%
rename from testcases/condabd/benchmarks/List/ListConcat.scala
rename to testcases/synthesis/condabd/benchmarks/List/ListConcat.scala
diff --git a/testcases/condabd/benchmarks/List/ListSearch.scala b/testcases/synthesis/condabd/benchmarks/List/ListSearch.scala
similarity index 100%
rename from testcases/condabd/benchmarks/List/ListSearch.scala
rename to testcases/synthesis/condabd/benchmarks/List/ListSearch.scala
diff --git a/testcases/condabd/benchmarks/MergeSort/MergeSortMerge.scala b/testcases/synthesis/condabd/benchmarks/MergeSort/MergeSortMerge.scala
similarity index 100%
rename from testcases/condabd/benchmarks/MergeSort/MergeSortMerge.scala
rename to testcases/synthesis/condabd/benchmarks/MergeSort/MergeSortMerge.scala
diff --git a/testcases/condabd/benchmarks/MergeSort/MergeSortSort.scala b/testcases/synthesis/condabd/benchmarks/MergeSort/MergeSortSort.scala
similarity index 100%
rename from testcases/condabd/benchmarks/MergeSort/MergeSortSort.scala
rename to testcases/synthesis/condabd/benchmarks/MergeSort/MergeSortSort.scala
diff --git a/testcases/condabd/benchmarks/MergeSort/MergeSortSortWithVal.scala b/testcases/synthesis/condabd/benchmarks/MergeSort/MergeSortSortWithVal.scala
similarity index 100%
rename from testcases/condabd/benchmarks/MergeSort/MergeSortSortWithVal.scala
rename to testcases/synthesis/condabd/benchmarks/MergeSort/MergeSortSortWithVal.scala
diff --git a/testcases/condabd/benchmarks/RedBlackTree/RedBlackTree.scala b/testcases/synthesis/condabd/benchmarks/RedBlackTree/RedBlackTree.scala
similarity index 100%
rename from testcases/condabd/benchmarks/RedBlackTree/RedBlackTree.scala
rename to testcases/synthesis/condabd/benchmarks/RedBlackTree/RedBlackTree.scala
diff --git a/testcases/condabd/benchmarks/RedBlackTree/RedBlackTreeInsert.scala b/testcases/synthesis/condabd/benchmarks/RedBlackTree/RedBlackTreeInsert.scala
similarity index 100%
rename from testcases/condabd/benchmarks/RedBlackTree/RedBlackTreeInsert.scala
rename to testcases/synthesis/condabd/benchmarks/RedBlackTree/RedBlackTreeInsert.scala
diff --git a/testcases/condabd/test/insynth/Addresses.scala b/testcases/synthesis/condabd/test/insynth/Addresses.scala
similarity index 100%
rename from testcases/condabd/test/insynth/Addresses.scala
rename to testcases/synthesis/condabd/test/insynth/Addresses.scala
diff --git a/testcases/condabd/test/insynth/AddressesWithAddition.scala b/testcases/synthesis/condabd/test/insynth/AddressesWithAddition.scala
similarity index 100%
rename from testcases/condabd/test/insynth/AddressesWithAddition.scala
rename to testcases/synthesis/condabd/test/insynth/AddressesWithAddition.scala
diff --git a/testcases/condabd/test/insynth/ListConcat.scala b/testcases/synthesis/condabd/test/insynth/ListConcat.scala
similarity index 100%
rename from testcases/condabd/test/insynth/ListConcat.scala
rename to testcases/synthesis/condabd/test/insynth/ListConcat.scala
diff --git a/testcases/condabd/test/lesynth/Addresses.scala b/testcases/synthesis/condabd/test/lesynth/Addresses.scala
similarity index 100%
rename from testcases/condabd/test/lesynth/Addresses.scala
rename to testcases/synthesis/condabd/test/lesynth/Addresses.scala
diff --git a/testcases/condabd/test/lesynth/AddressesMergeAddressBooks.scala b/testcases/synthesis/condabd/test/lesynth/AddressesMergeAddressBooks.scala
similarity index 100%
rename from testcases/condabd/test/lesynth/AddressesMergeAddressBooks.scala
rename to testcases/synthesis/condabd/test/lesynth/AddressesMergeAddressBooks.scala
diff --git a/testcases/condabd/test/lesynth/BinarySearchTree.scala b/testcases/synthesis/condabd/test/lesynth/BinarySearchTree.scala
similarity index 100%
rename from testcases/condabd/test/lesynth/BinarySearchTree.scala
rename to testcases/synthesis/condabd/test/lesynth/BinarySearchTree.scala
diff --git a/testcases/condabd/test/lesynth/InsertionSortInsert.scala b/testcases/synthesis/condabd/test/lesynth/InsertionSortInsert.scala
similarity index 100%
rename from testcases/condabd/test/lesynth/InsertionSortInsert.scala
rename to testcases/synthesis/condabd/test/lesynth/InsertionSortInsert.scala
diff --git a/testcases/condabd/test/lesynth/ListConcat.scala b/testcases/synthesis/condabd/test/lesynth/ListConcat.scala
similarity index 100%
rename from testcases/condabd/test/lesynth/ListConcat.scala
rename to testcases/synthesis/condabd/test/lesynth/ListConcat.scala
diff --git a/testcases/condabd/test/lesynth/ListConcatVerifierTest.scala b/testcases/synthesis/condabd/test/lesynth/ListConcatVerifierTest.scala
similarity index 100%
rename from testcases/condabd/test/lesynth/ListConcatVerifierTest.scala
rename to testcases/synthesis/condabd/test/lesynth/ListConcatVerifierTest.scala
diff --git a/testcases/condabd/test/lesynth/ListConcatWithEmpty.scala b/testcases/synthesis/condabd/test/lesynth/ListConcatWithEmpty.scala
similarity index 100%
rename from testcases/condabd/test/lesynth/ListConcatWithEmpty.scala
rename to testcases/synthesis/condabd/test/lesynth/ListConcatWithEmpty.scala
diff --git a/testcases/condabd/test/lesynth/MergeSortSort.scala b/testcases/synthesis/condabd/test/lesynth/MergeSortSort.scala
similarity index 100%
rename from testcases/condabd/test/lesynth/MergeSortSort.scala
rename to testcases/synthesis/condabd/test/lesynth/MergeSortSort.scala
diff --git a/testcases/condabd/test/lesynth/RedBlackTreeInsert.scala b/testcases/synthesis/condabd/test/lesynth/RedBlackTreeInsert.scala
similarity index 100%
rename from testcases/condabd/test/lesynth/RedBlackTreeInsert.scala
rename to testcases/synthesis/condabd/test/lesynth/RedBlackTreeInsert.scala
diff --git a/testcases/insynth-leon-tests/Arguments.scala b/testcases/synthesis/insynth-leon-tests/Arguments.scala
similarity index 100%
rename from testcases/insynth-leon-tests/Arguments.scala
rename to testcases/synthesis/insynth-leon-tests/Arguments.scala
diff --git a/testcases/insynth-leon-tests/BubbleSortBug.scala b/testcases/synthesis/insynth-leon-tests/BubbleSortBug.scala
similarity index 100%
rename from testcases/insynth-leon-tests/BubbleSortBug.scala
rename to testcases/synthesis/insynth-leon-tests/BubbleSortBug.scala
diff --git a/testcases/insynth-leon-tests/CaseClassSelectExample.scala b/testcases/synthesis/insynth-leon-tests/CaseClassSelectExample.scala
similarity index 100%
rename from testcases/insynth-leon-tests/CaseClassSelectExample.scala
rename to testcases/synthesis/insynth-leon-tests/CaseClassSelectExample.scala
diff --git a/testcases/insynth-leon-tests/Hole.scala b/testcases/synthesis/insynth-leon-tests/Hole.scala
similarity index 100%
rename from testcases/insynth-leon-tests/Hole.scala
rename to testcases/synthesis/insynth-leon-tests/Hole.scala
diff --git a/testcases/insynth-leon-tests/ListOperationsHole.scala b/testcases/synthesis/insynth-leon-tests/ListOperationsHole.scala
similarity index 100%
rename from testcases/insynth-leon-tests/ListOperationsHole.scala
rename to testcases/synthesis/insynth-leon-tests/ListOperationsHole.scala
diff --git a/testcases/insynth-leon-tests/RedBlackTreeFull.scala b/testcases/synthesis/insynth-leon-tests/RedBlackTreeFull.scala
similarity index 100%
rename from testcases/insynth-leon-tests/RedBlackTreeFull.scala
rename to testcases/synthesis/insynth-leon-tests/RedBlackTreeFull.scala
diff --git a/testcases/insynth-synthesis-tests/Hole.scala b/testcases/synthesis/insynth-synthesis-tests/Hole.scala
similarity index 100%
rename from testcases/insynth-synthesis-tests/Hole.scala
rename to testcases/synthesis/insynth-synthesis-tests/Hole.scala
diff --git a/testcases/insynth-synthesis-tests/LocalScope.scala b/testcases/synthesis/insynth-synthesis-tests/LocalScope.scala
similarity index 100%
rename from testcases/insynth-synthesis-tests/LocalScope.scala
rename to testcases/synthesis/insynth-synthesis-tests/LocalScope.scala
diff --git a/testcases/lesynth-results/RedBlackTreeSynthResult.scala b/testcases/synthesis/lesynth-results/RedBlackTreeSynthResult.scala
similarity index 100%
rename from testcases/lesynth-results/RedBlackTreeSynthResult.scala
rename to testcases/synthesis/lesynth-results/RedBlackTreeSynthResult.scala
diff --git a/testcases/lesynth-results/RedBlackTreeSynthResultBad.scala b/testcases/synthesis/lesynth-results/RedBlackTreeSynthResultBad.scala
similarity index 100%
rename from testcases/lesynth-results/RedBlackTreeSynthResultBad.scala
rename to testcases/synthesis/lesynth-results/RedBlackTreeSynthResultBad.scala
diff --git a/testcases/Addresses.scala b/testcases/verification/Addresses.scala
similarity index 99%
rename from testcases/Addresses.scala
rename to testcases/verification/Addresses.scala
index 3e5d730e5ff12a1887987894287c5b93acd81762..cd089c44cfce8f966e6f6ff98d3511c9dae796d2 100644
--- a/testcases/Addresses.scala
+++ b/testcases/verification/Addresses.scala
@@ -31,7 +31,7 @@ object Addresses {
   }) ensuring (res => res==theseAunique1(as,l))
 
   def disjoint(x:Set[Int],y:Set[Int]):Boolean = {
-    x ** y == Set.empty[Int]
+    (x & y) == Set.empty[Int]
   }
 
   def uniqueAbsentAs(unique:Set[Int],absent:Set[Int],l:List) : Boolean = (l match {
diff --git a/testcases/Errors.scala b/testcases/verification/Errors.scala
similarity index 100%
rename from testcases/Errors.scala
rename to testcases/verification/Errors.scala
diff --git a/testcases/Fibonacci.scala b/testcases/verification/Fibonacci.scala
similarity index 100%
rename from testcases/Fibonacci.scala
rename to testcases/verification/Fibonacci.scala
diff --git a/testcases/FiniteSort.scala b/testcases/verification/FiniteSort.scala
similarity index 100%
rename from testcases/FiniteSort.scala
rename to testcases/verification/FiniteSort.scala
diff --git a/testcases/Interpret.scala b/testcases/verification/Interpreter.scala
similarity index 100%
rename from testcases/Interpret.scala
rename to testcases/verification/Interpreter.scala
diff --git a/testcases/MutuallyRecursive.scala b/testcases/verification/MutuallyRecursive.scala
similarity index 100%
rename from testcases/MutuallyRecursive.scala
rename to testcases/verification/MutuallyRecursive.scala
diff --git a/testcases/Naturals.scala b/testcases/verification/Naturals.scala
similarity index 100%
rename from testcases/Naturals.scala
rename to testcases/verification/Naturals.scala
diff --git a/testcases/Parser.scala b/testcases/verification/Parser.scala
similarity index 100%
rename from testcases/Parser.scala
rename to testcases/verification/Parser.scala
diff --git a/testcases/Prime.scala b/testcases/verification/Prime.scala
similarity index 100%
rename from testcases/Prime.scala
rename to testcases/verification/Prime.scala
diff --git a/testcases/PropositionalLogic.scala b/testcases/verification/PropositionalLogic.scala
similarity index 100%
rename from testcases/PropositionalLogic.scala
rename to testcases/verification/PropositionalLogic.scala
diff --git a/testcases/SecondsToTime.scala b/testcases/verification/SecondsToTime.scala
similarity index 100%
rename from testcases/SecondsToTime.scala
rename to testcases/verification/SecondsToTime.scala
diff --git a/testcases/SimpInterpret.scala b/testcases/verification/SimpInterpret.scala
similarity index 100%
rename from testcases/SimpInterpret.scala
rename to testcases/verification/SimpInterpret.scala
diff --git a/testcases/TwoSizeFunctions.scala b/testcases/verification/TwoSizeFunctions.scala
similarity index 100%
rename from testcases/TwoSizeFunctions.scala
rename to testcases/verification/TwoSizeFunctions.scala
diff --git a/testcases/case-studies/Compiler.scala b/testcases/verification/case-studies/Compiler.scala
similarity index 100%
rename from testcases/case-studies/Compiler.scala
rename to testcases/verification/case-studies/Compiler.scala
diff --git a/testcases/case-studies/Lambda.scala b/testcases/verification/case-studies/Lambda.scala
similarity index 100%
rename from testcases/case-studies/Lambda.scala
rename to testcases/verification/case-studies/Lambda.scala
diff --git a/testcases/case-studies/Sync.scala b/testcases/verification/case-studies/Sync.scala
similarity index 100%
rename from testcases/case-studies/Sync.scala
rename to testcases/verification/case-studies/Sync.scala
diff --git a/testcases/datastructures/AVLTree.scala b/testcases/verification/datastructures/AVLTree.scala
similarity index 100%
rename from testcases/datastructures/AVLTree.scala
rename to testcases/verification/datastructures/AVLTree.scala
diff --git a/testcases/datastructures/AmortizedQueue.scala b/testcases/verification/datastructures/AmortizedQueue.scala
similarity index 100%
rename from testcases/datastructures/AmortizedQueue.scala
rename to testcases/verification/datastructures/AmortizedQueue.scala
diff --git a/testcases/datastructures/BinarySearchTree.scala b/testcases/verification/datastructures/BinarySearchTree.scala
similarity index 100%
rename from testcases/datastructures/BinarySearchTree.scala
rename to testcases/verification/datastructures/BinarySearchTree.scala
diff --git a/testcases/datastructures/BinarySearchTreeSorted.scala b/testcases/verification/datastructures/BinarySearchTreeSorted.scala
similarity index 100%
rename from testcases/datastructures/BinarySearchTreeSorted.scala
rename to testcases/verification/datastructures/BinarySearchTreeSorted.scala
diff --git a/testcases/datastructures/BinaryTrie.scala b/testcases/verification/datastructures/BinaryTrie.scala
similarity index 100%
rename from testcases/datastructures/BinaryTrie.scala
rename to testcases/verification/datastructures/BinaryTrie.scala
diff --git a/testcases/datastructures/HeapSort.scala b/testcases/verification/datastructures/HeapSort.scala
similarity index 100%
rename from testcases/datastructures/HeapSort.scala
rename to testcases/verification/datastructures/HeapSort.scala
diff --git a/testcases/datastructures/InsertionSort.scala b/testcases/verification/datastructures/InsertionSort.scala
similarity index 100%
rename from testcases/datastructures/InsertionSort.scala
rename to testcases/verification/datastructures/InsertionSort.scala
diff --git a/testcases/datastructures/LeftistHeap.scala b/testcases/verification/datastructures/LeftistHeap.scala
similarity index 100%
rename from testcases/datastructures/LeftistHeap.scala
rename to testcases/verification/datastructures/LeftistHeap.scala
diff --git a/testcases/datastructures/ListWithSize.scala b/testcases/verification/datastructures/ListWithSize.scala
similarity index 100%
rename from testcases/datastructures/ListWithSize.scala
rename to testcases/verification/datastructures/ListWithSize.scala
diff --git a/testcases/datastructures/MergeSort.scala b/testcases/verification/datastructures/MergeSort.scala
similarity index 100%
rename from testcases/datastructures/MergeSort.scala
rename to testcases/verification/datastructures/MergeSort.scala
diff --git a/testcases/datastructures/QuickSort.scala b/testcases/verification/datastructures/QuickSort.scala
similarity index 100%
rename from testcases/datastructures/QuickSort.scala
rename to testcases/verification/datastructures/QuickSort.scala
diff --git a/testcases/datastructures/RedBlackTree.scala b/testcases/verification/datastructures/RedBlackTree.scala
similarity index 100%
rename from testcases/datastructures/RedBlackTree.scala
rename to testcases/verification/datastructures/RedBlackTree.scala
diff --git a/testcases/datastructures/SortedList.scala b/testcases/verification/datastructures/SortedList.scala
similarity index 100%
rename from testcases/datastructures/SortedList.scala
rename to testcases/verification/datastructures/SortedList.scala
diff --git a/testcases/datastructures/TreeListSetNoDup.scala b/testcases/verification/datastructures/TreeListSetNoDup.scala
similarity index 100%
rename from testcases/datastructures/TreeListSetNoDup.scala
rename to testcases/verification/datastructures/TreeListSetNoDup.scala
diff --git a/testcases/graph/MST/MSTMap.scala b/testcases/verification/graph/MST/MSTMap.scala
similarity index 100%
rename from testcases/graph/MST/MSTMap.scala
rename to testcases/verification/graph/MST/MSTMap.scala
diff --git a/testcases/graph/MST/SpanningTree.scala b/testcases/verification/graph/MST/SpanningTree.scala
similarity index 100%
rename from testcases/graph/MST/SpanningTree.scala
rename to testcases/verification/graph/MST/SpanningTree.scala
diff --git a/testcases/graph/SetIteration.scala b/testcases/verification/graph/SetIteration.scala
similarity index 100%
rename from testcases/graph/SetIteration.scala
rename to testcases/verification/graph/SetIteration.scala
diff --git a/testcases/graph/SimpleInduction.scala b/testcases/verification/graph/SimpleInduction.scala
similarity index 100%
rename from testcases/graph/SimpleInduction.scala
rename to testcases/verification/graph/SimpleInduction.scala
diff --git a/testcases/graph/SortedNDList.scala b/testcases/verification/graph/SortedNDList.scala
similarity index 100%
rename from testcases/graph/SortedNDList.scala
rename to testcases/verification/graph/SortedNDList.scala
diff --git a/testcases/graph/Subgraph.scala b/testcases/verification/graph/Subgraph.scala
similarity index 100%
rename from testcases/graph/Subgraph.scala
rename to testcases/verification/graph/Subgraph.scala
diff --git a/testcases/graph/SubgraphMap.scala b/testcases/verification/graph/SubgraphMap.scala
similarity index 100%
rename from testcases/graph/SubgraphMap.scala
rename to testcases/verification/graph/SubgraphMap.scala
diff --git a/testcases/graph/TreeEquivalence.scala b/testcases/verification/graph/TreeEquivalence.scala
similarity index 100%
rename from testcases/graph/TreeEquivalence.scala
rename to testcases/verification/graph/TreeEquivalence.scala
diff --git a/testcases/graph/TreeEquivalenceMap.scala b/testcases/verification/graph/TreeEquivalenceMap.scala
similarity index 100%
rename from testcases/graph/TreeEquivalenceMap.scala
rename to testcases/verification/graph/TreeEquivalenceMap.scala
diff --git a/testcases/graph/dijkstras/DijkstrasSet.scala b/testcases/verification/graph/dijkstras/DijkstrasSet.scala
similarity index 100%
rename from testcases/graph/dijkstras/DijkstrasSet.scala
rename to testcases/verification/graph/dijkstras/DijkstrasSet.scala
diff --git a/testcases/graph/dijkstras/DijkstrasSetToVisit.scala b/testcases/verification/graph/dijkstras/DijkstrasSetToVisit.scala
similarity index 100%
rename from testcases/graph/dijkstras/DijkstrasSetToVisit.scala
rename to testcases/verification/graph/dijkstras/DijkstrasSetToVisit.scala
diff --git a/testcases/graph/dijkstras/DijkstrasSortedList.scala b/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala
similarity index 100%
rename from testcases/graph/dijkstras/DijkstrasSortedList.scala
rename to testcases/verification/graph/dijkstras/DijkstrasSortedList.scala
diff --git a/testcases/pldi2011-testcases/AssociativeList.scala b/testcases/verification/pldi2011-testcases/AssociativeList.scala
similarity index 100%
rename from testcases/pldi2011-testcases/AssociativeList.scala
rename to testcases/verification/pldi2011-testcases/AssociativeList.scala
diff --git a/testcases/pldi2011-testcases/ForElimination.scala b/testcases/verification/pldi2011-testcases/ForElimination.scala
similarity index 100%
rename from testcases/pldi2011-testcases/ForElimination.scala
rename to testcases/verification/pldi2011-testcases/ForElimination.scala
diff --git a/testcases/pldi2011-testcases/InsertionSort.scala b/testcases/verification/pldi2011-testcases/InsertionSort.scala
similarity index 100%
rename from testcases/pldi2011-testcases/InsertionSort.scala
rename to testcases/verification/pldi2011-testcases/InsertionSort.scala
diff --git a/testcases/pldi2011-testcases/LambdaEval.scala b/testcases/verification/pldi2011-testcases/LambdaEval.scala
similarity index 100%
rename from testcases/pldi2011-testcases/LambdaEval.scala
rename to testcases/verification/pldi2011-testcases/LambdaEval.scala
diff --git a/testcases/pldi2011-testcases/ListTree.scala b/testcases/verification/pldi2011-testcases/ListTree.scala
similarity index 100%
rename from testcases/pldi2011-testcases/ListTree.scala
rename to testcases/verification/pldi2011-testcases/ListTree.scala
diff --git a/testcases/pldi2011-testcases/MergeSort.scala b/testcases/verification/pldi2011-testcases/MergeSort.scala
similarity index 100%
rename from testcases/pldi2011-testcases/MergeSort.scala
rename to testcases/verification/pldi2011-testcases/MergeSort.scala
diff --git a/testcases/pldi2011-testcases/PropositionalLogic.scala b/testcases/verification/pldi2011-testcases/PropositionalLogic.scala
similarity index 100%
rename from testcases/pldi2011-testcases/PropositionalLogic.scala
rename to testcases/verification/pldi2011-testcases/PropositionalLogic.scala
diff --git a/testcases/pldi2011-testcases/QuickSort.scala b/testcases/verification/pldi2011-testcases/QuickSort.scala
similarity index 100%
rename from testcases/pldi2011-testcases/QuickSort.scala
rename to testcases/verification/pldi2011-testcases/QuickSort.scala
diff --git a/testcases/pldi2011-testcases/RedBlackTree.scala b/testcases/verification/pldi2011-testcases/RedBlackTree.scala
similarity index 100%
rename from testcases/pldi2011-testcases/RedBlackTree.scala
rename to testcases/verification/pldi2011-testcases/RedBlackTree.scala
diff --git a/testcases/pldi2011-testcases/RedBlackTreeDeletion.scala b/testcases/verification/pldi2011-testcases/RedBlackTreeDeletion.scala
similarity index 100%
rename from testcases/pldi2011-testcases/RedBlackTreeDeletion.scala
rename to testcases/verification/pldi2011-testcases/RedBlackTreeDeletion.scala
diff --git a/testcases/pldi2011-testcases/SemanticsPreservation.scala b/testcases/verification/pldi2011-testcases/SemanticsPreservation.scala
similarity index 100%
rename from testcases/pldi2011-testcases/SemanticsPreservation.scala
rename to testcases/verification/pldi2011-testcases/SemanticsPreservation.scala
diff --git a/testcases/pldi2011-testcases/TreeMap.scala b/testcases/verification/pldi2011-testcases/TreeMap.scala
similarity index 100%
rename from testcases/pldi2011-testcases/TreeMap.scala
rename to testcases/verification/pldi2011-testcases/TreeMap.scala
diff --git a/testcases/sas2011-testcases/AmortizedQueue.scala b/testcases/verification/sas2011-testcases/AmortizedQueue.scala
similarity index 100%
rename from testcases/sas2011-testcases/AmortizedQueue.scala
rename to testcases/verification/sas2011-testcases/AmortizedQueue.scala
diff --git a/testcases/sas2011-testcases/AssociativeList.scala b/testcases/verification/sas2011-testcases/AssociativeList.scala
similarity index 100%
rename from testcases/sas2011-testcases/AssociativeList.scala
rename to testcases/verification/sas2011-testcases/AssociativeList.scala
diff --git a/testcases/sas2011-testcases/InsertionSort.scala b/testcases/verification/sas2011-testcases/InsertionSort.scala
similarity index 100%
rename from testcases/sas2011-testcases/InsertionSort.scala
rename to testcases/verification/sas2011-testcases/InsertionSort.scala
diff --git a/testcases/sas2011-testcases/ListOperations.scala b/testcases/verification/sas2011-testcases/ListOperations.scala
similarity index 100%
rename from testcases/sas2011-testcases/ListOperations.scala
rename to testcases/verification/sas2011-testcases/ListOperations.scala
diff --git a/testcases/sas2011-testcases/PropositionalLogic.scala b/testcases/verification/sas2011-testcases/PropositionalLogic.scala
similarity index 100%
rename from testcases/sas2011-testcases/PropositionalLogic.scala
rename to testcases/verification/sas2011-testcases/PropositionalLogic.scala
diff --git a/testcases/sas2011-testcases/RedBlackTree.scala b/testcases/verification/sas2011-testcases/RedBlackTree.scala
similarity index 100%
rename from testcases/sas2011-testcases/RedBlackTree.scala
rename to testcases/verification/sas2011-testcases/RedBlackTree.scala
diff --git a/testcases/sas2011-testcases/SearchLinkedList.scala b/testcases/verification/sas2011-testcases/SearchLinkedList.scala
similarity index 100%
rename from testcases/sas2011-testcases/SearchLinkedList.scala
rename to testcases/verification/sas2011-testcases/SearchLinkedList.scala
diff --git a/testcases/sas2011-testcases/SumAndMax.scala b/testcases/verification/sas2011-testcases/SumAndMax.scala
similarity index 100%
rename from testcases/sas2011-testcases/SumAndMax.scala
rename to testcases/verification/sas2011-testcases/SumAndMax.scala
diff --git a/testcases/sas2011-testcases/camera-ready-eval-summaries/AmortizedQueue-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/AmortizedQueue-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/camera-ready-eval-summaries/AmortizedQueue-evaluation.txt
rename to testcases/verification/sas2011-testcases/camera-ready-eval-summaries/AmortizedQueue-evaluation.txt
diff --git a/testcases/sas2011-testcases/camera-ready-eval-summaries/AssociativeList-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/AssociativeList-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/camera-ready-eval-summaries/AssociativeList-evaluation.txt
rename to testcases/verification/sas2011-testcases/camera-ready-eval-summaries/AssociativeList-evaluation.txt
diff --git a/testcases/sas2011-testcases/camera-ready-eval-summaries/InsertionSort-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/InsertionSort-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/camera-ready-eval-summaries/InsertionSort-evaluation.txt
rename to testcases/verification/sas2011-testcases/camera-ready-eval-summaries/InsertionSort-evaluation.txt
diff --git a/testcases/sas2011-testcases/camera-ready-eval-summaries/ListOperations-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/ListOperations-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/camera-ready-eval-summaries/ListOperations-evaluation.txt
rename to testcases/verification/sas2011-testcases/camera-ready-eval-summaries/ListOperations-evaluation.txt
diff --git a/testcases/sas2011-testcases/camera-ready-eval-summaries/PropositionalLogic-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/PropositionalLogic-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/camera-ready-eval-summaries/PropositionalLogic-evaluation.txt
rename to testcases/verification/sas2011-testcases/camera-ready-eval-summaries/PropositionalLogic-evaluation.txt
diff --git a/testcases/sas2011-testcases/camera-ready-eval-summaries/RedBlackTree-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/RedBlackTree-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/camera-ready-eval-summaries/RedBlackTree-evaluation.txt
rename to testcases/verification/sas2011-testcases/camera-ready-eval-summaries/RedBlackTree-evaluation.txt
diff --git a/testcases/sas2011-testcases/camera-ready-eval-summaries/SearchLinkedList-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/SearchLinkedList-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/camera-ready-eval-summaries/SearchLinkedList-evaluation.txt
rename to testcases/verification/sas2011-testcases/camera-ready-eval-summaries/SearchLinkedList-evaluation.txt
diff --git a/testcases/sas2011-testcases/camera-ready-eval-summaries/SumAndMax-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/SumAndMax-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/camera-ready-eval-summaries/SumAndMax-evaluation.txt
rename to testcases/verification/sas2011-testcases/camera-ready-eval-summaries/SumAndMax-evaluation.txt
diff --git a/testcases/sas2011-testcases/eval-summary/AmortizedQueue-evaluation.txt b/testcases/verification/sas2011-testcases/eval-summary/AmortizedQueue-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/eval-summary/AmortizedQueue-evaluation.txt
rename to testcases/verification/sas2011-testcases/eval-summary/AmortizedQueue-evaluation.txt
diff --git a/testcases/sas2011-testcases/eval-summary/AssociativeList-evaluation.txt b/testcases/verification/sas2011-testcases/eval-summary/AssociativeList-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/eval-summary/AssociativeList-evaluation.txt
rename to testcases/verification/sas2011-testcases/eval-summary/AssociativeList-evaluation.txt
diff --git a/testcases/sas2011-testcases/eval-summary/InsertionSort-evaluation.txt b/testcases/verification/sas2011-testcases/eval-summary/InsertionSort-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/eval-summary/InsertionSort-evaluation.txt
rename to testcases/verification/sas2011-testcases/eval-summary/InsertionSort-evaluation.txt
diff --git a/testcases/sas2011-testcases/eval-summary/ListOperations-evaluation.txt b/testcases/verification/sas2011-testcases/eval-summary/ListOperations-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/eval-summary/ListOperations-evaluation.txt
rename to testcases/verification/sas2011-testcases/eval-summary/ListOperations-evaluation.txt
diff --git a/testcases/sas2011-testcases/eval-summary/PropositionalLogic-evaluation-PLDI-100.txt b/testcases/verification/sas2011-testcases/eval-summary/PropositionalLogic-evaluation-PLDI-100.txt
similarity index 100%
rename from testcases/sas2011-testcases/eval-summary/PropositionalLogic-evaluation-PLDI-100.txt
rename to testcases/verification/sas2011-testcases/eval-summary/PropositionalLogic-evaluation-PLDI-100.txt
diff --git a/testcases/sas2011-testcases/eval-summary/PropositionalLogic-evaluation.txt b/testcases/verification/sas2011-testcases/eval-summary/PropositionalLogic-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/eval-summary/PropositionalLogic-evaluation.txt
rename to testcases/verification/sas2011-testcases/eval-summary/PropositionalLogic-evaluation.txt
diff --git a/testcases/sas2011-testcases/eval-summary/RedBlackTree-evaluation.txt b/testcases/verification/sas2011-testcases/eval-summary/RedBlackTree-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/eval-summary/RedBlackTree-evaluation.txt
rename to testcases/verification/sas2011-testcases/eval-summary/RedBlackTree-evaluation.txt
diff --git a/testcases/sas2011-testcases/eval-summary/SearchLinkedList-evaluation.txt b/testcases/verification/sas2011-testcases/eval-summary/SearchLinkedList-evaluation.txt
similarity index 100%
rename from testcases/sas2011-testcases/eval-summary/SearchLinkedList-evaluation.txt
rename to testcases/verification/sas2011-testcases/eval-summary/SearchLinkedList-evaluation.txt
diff --git a/testcases/sas2011-testcases/eval-summary/SumAndMax-evaluation-pldi-100.txt b/testcases/verification/sas2011-testcases/eval-summary/SumAndMax-evaluation-pldi-100.txt
similarity index 100%
rename from testcases/sas2011-testcases/eval-summary/SumAndMax-evaluation-pldi-100.txt
rename to testcases/verification/sas2011-testcases/eval-summary/SumAndMax-evaluation-pldi-100.txt
diff --git a/testcases/scala-workshop/AmortizedQueue.scala b/testcases/verification/scala2013/AmortizedQueue.scala
similarity index 100%
rename from testcases/scala-workshop/AmortizedQueue.scala
rename to testcases/verification/scala2013/AmortizedQueue.scala
diff --git a/testcases/scala-workshop/AmortizedQueueImp.scala b/testcases/verification/scala2013/AmortizedQueueImp.scala
similarity index 100%
rename from testcases/scala-workshop/AmortizedQueueImp.scala
rename to testcases/verification/scala2013/AmortizedQueueImp.scala
diff --git a/testcases/scala-workshop/Arithmetic.scala b/testcases/verification/scala2013/Arithmetic.scala
similarity index 100%
rename from testcases/scala-workshop/Arithmetic.scala
rename to testcases/verification/scala2013/Arithmetic.scala
diff --git a/testcases/scala-workshop/AssociativeList.scala b/testcases/verification/scala2013/AssociativeList.scala
similarity index 100%
rename from testcases/scala-workshop/AssociativeList.scala
rename to testcases/verification/scala2013/AssociativeList.scala
diff --git a/testcases/scala-workshop/AssociativeListImp.scala b/testcases/verification/scala2013/AssociativeListImp.scala
similarity index 100%
rename from testcases/scala-workshop/AssociativeListImp.scala
rename to testcases/verification/scala2013/AssociativeListImp.scala
diff --git a/testcases/scala-workshop/ListOperations.scala b/testcases/verification/scala2013/ListOperations.scala
similarity index 100%
rename from testcases/scala-workshop/ListOperations.scala
rename to testcases/verification/scala2013/ListOperations.scala
diff --git a/testcases/scala-workshop/ListOperationsImp.scala b/testcases/verification/scala2013/ListOperationsImp.scala
similarity index 100%
rename from testcases/scala-workshop/ListOperationsImp.scala
rename to testcases/verification/scala2013/ListOperationsImp.scala
diff --git a/testcases/scala-workshop/PropositionalLogic.scala b/testcases/verification/scala2013/PropositionalLogic.scala
similarity index 100%
rename from testcases/scala-workshop/PropositionalLogic.scala
rename to testcases/verification/scala2013/PropositionalLogic.scala
diff --git a/testcases/scala-workshop/RedBlackTree.scala b/testcases/verification/scala2013/RedBlackTree.scala
similarity index 100%
rename from testcases/scala-workshop/RedBlackTree.scala
rename to testcases/verification/scala2013/RedBlackTree.scala
diff --git a/testcases/scala-workshop/SearchLinkedList.scala b/testcases/verification/scala2013/SearchLinkedList.scala
similarity index 100%
rename from testcases/scala-workshop/SearchLinkedList.scala
rename to testcases/verification/scala2013/SearchLinkedList.scala
diff --git a/testcases/scala-workshop/Sorting.scala b/testcases/verification/scala2013/Sorting.scala
similarity index 100%
rename from testcases/scala-workshop/Sorting.scala
rename to testcases/verification/scala2013/Sorting.scala
diff --git a/testcases/scala-workshop/SumAndMax.scala b/testcases/verification/scala2013/SumAndMax.scala
similarity index 100%
rename from testcases/scala-workshop/SumAndMax.scala
rename to testcases/verification/scala2013/SumAndMax.scala
diff --git a/testcases/scala-workshop/SumAndMaxImp.scala b/testcases/verification/scala2013/SumAndMaxImp.scala
similarity index 100%
rename from testcases/scala-workshop/SumAndMaxImp.scala
rename to testcases/verification/scala2013/SumAndMaxImp.scala
diff --git a/testcases/vmcai2011-testcases/CADE07.scala b/testcases/verification/vmcai2011-testcases/CADE07.scala
similarity index 100%
rename from testcases/vmcai2011-testcases/CADE07.scala
rename to testcases/verification/vmcai2011-testcases/CADE07.scala
diff --git a/testcases/vmcai2011-testcases/CADE07Hard.scala b/testcases/verification/vmcai2011-testcases/CADE07Hard.scala
similarity index 100%
rename from testcases/vmcai2011-testcases/CADE07Hard.scala
rename to testcases/verification/vmcai2011-testcases/CADE07Hard.scala
diff --git a/testcases/vmcai2011-testcases/Giuliano.scala b/testcases/verification/vmcai2011-testcases/Giuliano.scala
similarity index 100%
rename from testcases/vmcai2011-testcases/Giuliano.scala
rename to testcases/verification/vmcai2011-testcases/Giuliano.scala
diff --git a/testcases/vmcai2011-testcases/JustFormulas.scala b/testcases/verification/vmcai2011-testcases/JustFormulas.scala
similarity index 100%
rename from testcases/vmcai2011-testcases/JustFormulas.scala
rename to testcases/verification/vmcai2011-testcases/JustFormulas.scala
diff --git a/testcases/vmcai2011-testcases/ListProperties.scala b/testcases/verification/vmcai2011-testcases/ListProperties.scala
similarity index 100%
rename from testcases/vmcai2011-testcases/ListProperties.scala
rename to testcases/verification/vmcai2011-testcases/ListProperties.scala
diff --git a/testcases/vmcai2011-testcases/PaperExamples.scala b/testcases/verification/vmcai2011-testcases/PaperExamples.scala
similarity index 100%
rename from testcases/vmcai2011-testcases/PaperExamples.scala
rename to testcases/verification/vmcai2011-testcases/PaperExamples.scala
diff --git a/testcases/vmcai2011-testcases/SanityChecks.scala b/testcases/verification/vmcai2011-testcases/SanityChecks.scala
similarity index 100%
rename from testcases/vmcai2011-testcases/SanityChecks.scala
rename to testcases/verification/vmcai2011-testcases/SanityChecks.scala
diff --git a/testcases/vstte10competition/AmortizedQueue.scala b/testcases/verification/vstte10competition/AmortizedQueue.scala
similarity index 100%
rename from testcases/vstte10competition/AmortizedQueue.scala
rename to testcases/verification/vstte10competition/AmortizedQueue.scala
diff --git a/testcases/vstte10competition/Injection.scala b/testcases/verification/vstte10competition/Injection.scala
similarity index 100%
rename from testcases/vstte10competition/Injection.scala
rename to testcases/verification/vstte10competition/Injection.scala
diff --git a/testcases/vstte10competition/SearchLinkedList.scala b/testcases/verification/vstte10competition/SearchLinkedList.scala
similarity index 100%
rename from testcases/vstte10competition/SearchLinkedList.scala
rename to testcases/verification/vstte10competition/SearchLinkedList.scala
diff --git a/testcases/vstte10competition/SumAndMax.scala b/testcases/verification/vstte10competition/SumAndMax.scala
similarity index 100%
rename from testcases/vstte10competition/SumAndMax.scala
rename to testcases/verification/vstte10competition/SumAndMax.scala
diff --git a/testcases/xlang/AbsArray.scala b/testcases/verification/xlang/AbsArray.scala
similarity index 100%
rename from testcases/xlang/AbsArray.scala
rename to testcases/verification/xlang/AbsArray.scala
diff --git a/testcases/xlang/AbsFun.scala b/testcases/verification/xlang/AbsFun.scala
similarity index 100%
rename from testcases/xlang/AbsFun.scala
rename to testcases/verification/xlang/AbsFun.scala
diff --git a/testcases/xlang/Add.scala b/testcases/verification/xlang/Add.scala
similarity index 100%
rename from testcases/xlang/Add.scala
rename to testcases/verification/xlang/Add.scala
diff --git a/testcases/xlang/ArrayBinarySearch.scala b/testcases/verification/xlang/ArrayBinarySearch.scala
similarity index 100%
rename from testcases/xlang/ArrayBinarySearch.scala
rename to testcases/verification/xlang/ArrayBinarySearch.scala
diff --git a/testcases/xlang/ArrayBinarySearchProcedural.scala b/testcases/verification/xlang/ArrayBinarySearchProcedural.scala
similarity index 100%
rename from testcases/xlang/ArrayBinarySearchProcedural.scala
rename to testcases/verification/xlang/ArrayBinarySearchProcedural.scala
diff --git a/testcases/xlang/BinaryTreeImp.scala b/testcases/verification/xlang/BinaryTreeImp.scala
similarity index 100%
rename from testcases/xlang/BinaryTreeImp.scala
rename to testcases/verification/xlang/BinaryTreeImp.scala
diff --git a/testcases/xlang/BubbleFun.scala b/testcases/verification/xlang/BubbleFun.scala
similarity index 100%
rename from testcases/xlang/BubbleFun.scala
rename to testcases/verification/xlang/BubbleFun.scala
diff --git a/testcases/xlang/BubbleSort.scala b/testcases/verification/xlang/BubbleSort.scala
similarity index 100%
rename from testcases/xlang/BubbleSort.scala
rename to testcases/verification/xlang/BubbleSort.scala
diff --git a/testcases/xlang/BubbleWeakInvariant.scala b/testcases/verification/xlang/BubbleWeakInvariant.scala
similarity index 100%
rename from testcases/xlang/BubbleWeakInvariant.scala
rename to testcases/verification/xlang/BubbleWeakInvariant.scala
diff --git a/testcases/xlang/InsertionSortImp.scala b/testcases/verification/xlang/InsertionSortImp.scala
similarity index 100%
rename from testcases/xlang/InsertionSortImp.scala
rename to testcases/verification/xlang/InsertionSortImp.scala
diff --git a/testcases/xlang/IntOperations.scala b/testcases/verification/xlang/IntOperations.scala
similarity index 100%
rename from testcases/xlang/IntOperations.scala
rename to testcases/verification/xlang/IntOperations.scala
diff --git a/testcases/xlang/LinearSearch.scala b/testcases/verification/xlang/LinearSearch.scala
similarity index 100%
rename from testcases/xlang/LinearSearch.scala
rename to testcases/verification/xlang/LinearSearch.scala
diff --git a/testcases/xlang/ListImp.scala b/testcases/verification/xlang/ListImp.scala
similarity index 100%
rename from testcases/xlang/ListImp.scala
rename to testcases/verification/xlang/ListImp.scala
diff --git a/testcases/xlang/MaxSum.scala b/testcases/verification/xlang/MaxSum.scala
similarity index 100%
rename from testcases/xlang/MaxSum.scala
rename to testcases/verification/xlang/MaxSum.scala
diff --git a/testcases/xlang/Mult.scala b/testcases/verification/xlang/Mult.scala
similarity index 100%
rename from testcases/xlang/Mult.scala
rename to testcases/verification/xlang/Mult.scala
diff --git a/testcases/xlang/NonDeterministicList.scala b/testcases/verification/xlang/NonDeterministicList.scala
similarity index 100%
rename from testcases/xlang/NonDeterministicList.scala
rename to testcases/verification/xlang/NonDeterministicList.scala
diff --git a/testcases/xlang/QuickSortImp.scala b/testcases/verification/xlang/QuickSortImp.scala
similarity index 100%
rename from testcases/xlang/QuickSortImp.scala
rename to testcases/verification/xlang/QuickSortImp.scala
diff --git a/testcases/xlang/buggyEpsilon.scala b/testcases/verification/xlang/buggyEpsilon.scala
similarity index 100%
rename from testcases/xlang/buggyEpsilon.scala
rename to testcases/verification/xlang/buggyEpsilon.scala
diff --git a/testcases/xlang/master-thesis-regis/Arithmetic.scala b/testcases/verification/xlang/master-thesis-regis/Arithmetic.scala
similarity index 100%
rename from testcases/xlang/master-thesis-regis/Arithmetic.scala
rename to testcases/verification/xlang/master-thesis-regis/Arithmetic.scala
diff --git a/testcases/xlang/master-thesis-regis/ArrayBubbleSort.scala b/testcases/verification/xlang/master-thesis-regis/ArrayBubbleSort.scala
similarity index 100%
rename from testcases/xlang/master-thesis-regis/ArrayBubbleSort.scala
rename to testcases/verification/xlang/master-thesis-regis/ArrayBubbleSort.scala
diff --git a/testcases/xlang/master-thesis-regis/ArrayOperations.scala b/testcases/verification/xlang/master-thesis-regis/ArrayOperations.scala
similarity index 100%
rename from testcases/xlang/master-thesis-regis/ArrayOperations.scala
rename to testcases/verification/xlang/master-thesis-regis/ArrayOperations.scala
diff --git a/testcases/xlang/master-thesis-regis/Constraints.scala b/testcases/verification/xlang/master-thesis-regis/Constraints.scala
similarity index 100%
rename from testcases/xlang/master-thesis-regis/Constraints.scala
rename to testcases/verification/xlang/master-thesis-regis/Constraints.scala
diff --git a/testcases/xlang/master-thesis-regis/ListOperations.scala b/testcases/verification/xlang/master-thesis-regis/ListOperations.scala
similarity index 100%
rename from testcases/xlang/master-thesis-regis/ListOperations.scala
rename to testcases/verification/xlang/master-thesis-regis/ListOperations.scala
diff --git a/testcases/xlang/xplusone.scala b/testcases/verification/xlang/xplusone.scala
similarity index 100%
rename from testcases/xlang/xplusone.scala
rename to testcases/verification/xlang/xplusone.scala