diff --git a/build.sbt b/build.sbt
index 908d231bc6bb940904d7a957c2187892f11ac649..9c65cad8612062a40ad17857359b273ae9331676 100644
--- a/build.sbt
+++ b/build.sbt
@@ -4,13 +4,13 @@ version := "2.0"
organization := "ch.epfl.lara"
-scalaVersion := "2.9.0-1"
+scalaVersion := "2.9.1-1"
scalacOptions += "-deprecation"
scalacOptions += "-unchecked"
-libraryDependencies += "org.scala-lang" % "scala-compiler" % "2.9.0-1"
+libraryDependencies += "org.scala-lang" % "scala-compiler" % "2.9.1-1"
unmanagedBase <<= baseDirectory { base => base / "unmanaged" }
diff --git a/testcases/AddressBook.scala b/testcases/AddressBook.scala
index 9e5144cebe14d6639e8eb7b15194c999165d8b80..aaad0040a0ea3eb2ce2601b832ec8dffa8af90d7 100644
--- a/testcases/AddressBook.scala
+++ b/testcases/AddressBook.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
// Ongoing work: take Chapter 2 of Daniel Jackson's book,
// adapt the addressbook example from there.
diff --git a/testcases/ConnectedTest.scala b/testcases/ConnectedTest.scala
index a50e3cd2478d5bec475c14660b53de0d4b567bf5..00125985290e6eefb3ab4627351800af9741acdb 100644
--- a/testcases/ConnectedTest.scala
+++ b/testcases/ConnectedTest.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object VerySimple {
sealed abstract class L0
diff --git a/testcases/Expr2Comp.scala b/testcases/Expr2Comp.scala
index b5aa14adcb9fc7ba84f331cde76de38a1bcea71b..eca1fe6f5b0527034ec6f866fbfe362776c1618d 100644
--- a/testcases/Expr2Comp.scala
+++ b/testcases/Expr2Comp.scala
@@ -1,5 +1,5 @@
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object ExprComp {
// Lists
@@ -111,7 +111,7 @@ object ExprComp {
def main(args : Array[String]) = {
val e1 = Binary(Constant(100), Times(), Binary(Constant(3), Plus(), Constant(5)))
- // thanks to funcheck:
+ // thanks to Leon:
val e = Binary(Binary(Binary(Binary(Constant(75), Plus(), Constant(69)), Times(), Binary(Constant(73), Plus(), Constant(71))), Times(), Binary(Binary(Constant(70), Plus(), Constant(77)), Times(), Binary(Constant(68), Plus(), Constant(66)))), Plus(), Binary(Constant(1), Plus(), Binary(Constant(0), Times(), Binary(Constant(65), Plus(), Constant(72)))))
val acc = EProgram()
val vs = Cons(42,Nil())
diff --git a/testcases/ExprComp.scala b/testcases/ExprComp.scala
index fb36237dc021b545d4c827e7c62ae3b60bc2e871..116f0099bd4741717322355a4c0a1709eb89d4f6 100644
--- a/testcases/ExprComp.scala
+++ b/testcases/ExprComp.scala
@@ -1,5 +1,5 @@
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object ExprComp {
diff --git a/testcases/InsertionSort.scala b/testcases/InsertionSort.scala
index 0db222160cd86558ec159ee13ee78ad75c392376..6b162246f803831a5f789d09895d67f04465db0d 100644
--- a/testcases/InsertionSort.scala
+++ b/testcases/InsertionSort.scala
@@ -1,5 +1,5 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
+import leon.Utils._
object InsertionSort {
sealed abstract class List
diff --git a/testcases/IntOperations.scala b/testcases/IntOperations.scala
index 98a7574342ab4a7cebe3ae2a6741c977dc06fe44..98c9f9e5fdcc580de10a9e51060c5ab95a2eaff9 100644
--- a/testcases/IntOperations.scala
+++ b/testcases/IntOperations.scala
@@ -9,7 +9,7 @@ object IntOperations {
// The body of the following function is not in PureScala
// It will still get extracted, with "unknown body".
- // To disable the warnings, run with -P:funcheck:tolerant
+ // To disable the warnings, run with -P:leon:tolerant
// (if it has a postcondition, you'll still get warnings
// about the impossibility of verifying them)
def factorial(v: Int) : Int = {
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index c74a21761a49811340510b7eb37d4ca168cfe0c9..868cb45561e95552e10b8310c1a17f321515f89b 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object ListWithSize {
sealed abstract class List
diff --git a/testcases/MutuallyRecursive.scala b/testcases/MutuallyRecursive.scala
index 374b571c7b600ed9f9f555c76cd9bc500d37748e..bd5a6bfe42fa41d68f70e9abbb2bd845c1d8d88f 100644
--- a/testcases/MutuallyRecursive.scala
+++ b/testcases/MutuallyRecursive.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object MutuallyRecursive {
def f(n : Int) : Int = {
diff --git a/testcases/Naturals.scala b/testcases/Naturals.scala
index 8f9ea83156cc9ea3d37652b33dacf74ae387fe06..9b621b0a051d16cb040cb37b1760c6a4956ff3db 100644
--- a/testcases/Naturals.scala
+++ b/testcases/Naturals.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object Naturals {
sealed abstract class Nat
diff --git a/testcases/README b/testcases/README
index 020435430314d78ec6d7d0a373bfc6b8b1bc538f..896a958ee912d9d3c5662b6a59aeed51b96536aa 100644
--- a/testcases/README
+++ b/testcases/README
@@ -1,2 +1,2 @@
-Anything that's in this directory needs to be parsable by FunCheck, otherwise
+Anything that's in this directory needs to be parsable by Leon, otherwise
it will make me angry.
diff --git a/testcases/Test.scala b/testcases/Test.scala
index 798ee003722523ee678f4e7f9cdc5c7cdef35240..79f143b3497fbf4bd14ad4e87948872175e066ed 100644
--- a/testcases/Test.scala
+++ b/testcases/Test.scala
@@ -1,5 +1,5 @@
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object Test {
sealed abstract class List
diff --git a/testcases/TwoSizeFunctions.scala b/testcases/TwoSizeFunctions.scala
index 1e99907412ca21ec3f00f69cf667123c5415d563..e88239783b7ddfc14e021408d7f058b1edab4c3d 100644
--- a/testcases/TwoSizeFunctions.scala
+++ b/testcases/TwoSizeFunctions.scala
@@ -1,5 +1,5 @@
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object TwoSizeFunctions {
sealed abstract class List
diff --git a/testcases/UseContradictoryLemma.scala b/testcases/UseContradictoryLemma.scala
index f25cec124868e997d9bf1259e013478d96fff335..5ab165bfcd6ed0d9a72145b1b4b519c4a5642aeb 100644
--- a/testcases/UseContradictoryLemma.scala
+++ b/testcases/UseContradictoryLemma.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object UseContradictoryLemma {
diff --git a/testcases/VerySimple.scala b/testcases/VerySimple.scala
index b2f5977eb2470f0e23560c188ea285dc550863ce..d89391d4287b63cab023b0b15dd13fd6e95d6c8b 100644
--- a/testcases/VerySimple.scala
+++ b/testcases/VerySimple.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object VerySimple {
sealed abstract class List
diff --git a/testcases/Viktor.scala b/testcases/Viktor.scala
index 009953cd811f18a3e980f67aec82b0de49ca2a39..3d86ee0ffbbf5f7f9bfd4053b2e7f44484ae056c 100644
--- a/testcases/Viktor.scala
+++ b/testcases/Viktor.scala
@@ -1,4 +1,4 @@
-import funcheck.Utils._
+import leon.Utils._
object Viktor {
def transitive(x: Boolean, y: Boolean, z: Boolean) : Boolean = {
diff --git a/testcases/pldi2011-testcases/AssociativeList.scala b/testcases/pldi2011-testcases/AssociativeList.scala
index ed18a6bba8619fd38aa3d38d9fcea7808a5eedaf..6b9319afdb7d72519f8e8d316901a12b7e652201 100644
--- a/testcases/pldi2011-testcases/AssociativeList.scala
+++ b/testcases/pldi2011-testcases/AssociativeList.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object AssociativeList {
sealed abstract class KeyValuePairAbs
diff --git a/testcases/pldi2011-testcases/ForElimination.scala b/testcases/pldi2011-testcases/ForElimination.scala
index df39b2bc4bb431399dab94aadd729edad613a10e..ed8e6b8776da928730c899b894d34294750143e5 100644
--- a/testcases/pldi2011-testcases/ForElimination.scala
+++ b/testcases/pldi2011-testcases/ForElimination.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object ForElimination {
diff --git a/testcases/pldi2011-testcases/InsertionSort.scala b/testcases/pldi2011-testcases/InsertionSort.scala
index 7d5e0eb62bdee12ef332efba6498dd6695063ed8..a1215b025cc8d5dd906cce8917509f69edf1bd6e 100644
--- a/testcases/pldi2011-testcases/InsertionSort.scala
+++ b/testcases/pldi2011-testcases/InsertionSort.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object InsertionSort {
sealed abstract class List
diff --git a/testcases/pldi2011-testcases/LambdaEval.scala b/testcases/pldi2011-testcases/LambdaEval.scala
index 889847edb87424e7ef9377415f718d49960b2a49..2a26e46877b75c7407ac2e946e2594286bd2bf79 100644
--- a/testcases/pldi2011-testcases/LambdaEval.scala
+++ b/testcases/pldi2011-testcases/LambdaEval.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object LambdaEval {
sealed abstract class Expr
diff --git a/testcases/pldi2011-testcases/PropositionalLogic.scala b/testcases/pldi2011-testcases/PropositionalLogic.scala
index dbdf6e3eeee1ec244fe446eb44f785e8129a7763..ef7b0d34aa82e02d0f88b7e386ba705250e2825e 100644
--- a/testcases/pldi2011-testcases/PropositionalLogic.scala
+++ b/testcases/pldi2011-testcases/PropositionalLogic.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object PropositionalLogic {
diff --git a/testcases/pldi2011-testcases/QuickSort.scala b/testcases/pldi2011-testcases/QuickSort.scala
index db8645ffe7171533c1d066273a60d708c0e58025..c0456021865c200cf9ea747d473b1d8eecbdc89c 100644
--- a/testcases/pldi2011-testcases/QuickSort.scala
+++ b/testcases/pldi2011-testcases/QuickSort.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object QuickSort {
sealed abstract class List
diff --git a/testcases/pldi2011-testcases/RedBlackTree.scala b/testcases/pldi2011-testcases/RedBlackTree.scala
index 0f443af5924f84665c409e658d260fdd856c40ec..aca029fb2454d29fb6c20486d9572bb14defd5b9 100644
--- a/testcases/pldi2011-testcases/RedBlackTree.scala
+++ b/testcases/pldi2011-testcases/RedBlackTree.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object RedBlackTree {
sealed abstract class Color
diff --git a/testcases/pldi2011-testcases/RedBlackTreeDeletion.scala b/testcases/pldi2011-testcases/RedBlackTreeDeletion.scala
index c3146a831ed9ec276aad248b301ce770ddc18f04..7cc45ca3c65b233d03a0579bbfb51e9010c666a5 100644
--- a/testcases/pldi2011-testcases/RedBlackTreeDeletion.scala
+++ b/testcases/pldi2011-testcases/RedBlackTreeDeletion.scala
@@ -1,5 +1,5 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
+import leon.Annotations._
object RedBlackTree {
sealed abstract class Color
diff --git a/testcases/pldi2011-testcases/SemanticsPreservation.scala b/testcases/pldi2011-testcases/SemanticsPreservation.scala
index a5a2a38f950793b38532b6bccc9d48299417b472..ece2e608eb3bdee558b9e7ca2e00f0a36c6f5a6e 100644
--- a/testcases/pldi2011-testcases/SemanticsPreservation.scala
+++ b/testcases/pldi2011-testcases/SemanticsPreservation.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object SemanticsPreservation {
diff --git a/testcases/pldi2011-testcases/TreeMap.scala b/testcases/pldi2011-testcases/TreeMap.scala
index fd9bbc038677fc5719d0ce1c3436bb0085806e33..77318cdd29cdb3d0c8ecf2b62ac37639fccfc048 100644
--- a/testcases/pldi2011-testcases/TreeMap.scala
+++ b/testcases/pldi2011-testcases/TreeMap.scala
@@ -1,5 +1,5 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
+import leon.Utils._
object TreeMap {
sealed abstract class TreeMap
diff --git a/testcases/sas2011-testcases/AmortizedQueue.scala b/testcases/sas2011-testcases/AmortizedQueue.scala
index db9f1928ec7ee9f13a955185ed423d33034f43f0..dd5a75f89735805a74612665e487aa8fa99ec397 100644
--- a/testcases/sas2011-testcases/AmortizedQueue.scala
+++ b/testcases/sas2011-testcases/AmortizedQueue.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object AmortizedQueue {
sealed abstract class List
diff --git a/testcases/sas2011-testcases/AssociativeList.scala b/testcases/sas2011-testcases/AssociativeList.scala
index dc56e8fd4eb2c28c216e7191990a31084c5ec89a..f5a2fc0415a2cf6023f9ae1f3620e99f9fdc27cb 100644
--- a/testcases/sas2011-testcases/AssociativeList.scala
+++ b/testcases/sas2011-testcases/AssociativeList.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object AssociativeList {
sealed abstract class KeyValuePairAbs
diff --git a/testcases/sas2011-testcases/InsertionSort.scala b/testcases/sas2011-testcases/InsertionSort.scala
index c8d4cc7072ab525182a2ee35ba0c3a324c64b52a..d2ae67b3bb465f13437a1eb70a57a8e7e613347a 100644
--- a/testcases/sas2011-testcases/InsertionSort.scala
+++ b/testcases/sas2011-testcases/InsertionSort.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object InsertionSort {
sealed abstract class List
diff --git a/testcases/sas2011-testcases/PropositionalLogic.scala b/testcases/sas2011-testcases/PropositionalLogic.scala
index d95ed58c4d44030d576a5e5ef0bc8ec37812e308..a35c3ef9be56871900d5e9474b385f0896edccd4 100644
--- a/testcases/sas2011-testcases/PropositionalLogic.scala
+++ b/testcases/sas2011-testcases/PropositionalLogic.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object PropositionalLogic {
diff --git a/testcases/sas2011-testcases/RedBlackTree.scala b/testcases/sas2011-testcases/RedBlackTree.scala
index da5dd22c0c71649e0dd6ec01a7ee30fa7490ef7f..bc2de6ba96ee699736d4558932b752eea9ebba9f 100644
--- a/testcases/sas2011-testcases/RedBlackTree.scala
+++ b/testcases/sas2011-testcases/RedBlackTree.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object RedBlackTree {
sealed abstract class Color
diff --git a/testcases/sas2011-testcases/SearchLinkedList.scala b/testcases/sas2011-testcases/SearchLinkedList.scala
index d14b9fee6c000c5cc703a6e3b97af4ee1eba5562..2c137fd4ad6b9d411f7e14b4ada6b834234c9e9e 100644
--- a/testcases/sas2011-testcases/SearchLinkedList.scala
+++ b/testcases/sas2011-testcases/SearchLinkedList.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object SearchLinkedList {
sealed abstract class List
diff --git a/testcases/sas2011-testcases/SumAndMax.scala b/testcases/sas2011-testcases/SumAndMax.scala
index c4265e25b6e1846a5a0b8e47f1d8f224229131c0..0aa4ce7060a391d34dd047338fcd1f638054843f 100644
--- a/testcases/sas2011-testcases/SumAndMax.scala
+++ b/testcases/sas2011-testcases/SumAndMax.scala
@@ -1,5 +1,5 @@
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object SumAndMax {
sealed abstract class List
diff --git a/testcases/vmcai2011-testcases/JustFormulas.scala b/testcases/vmcai2011-testcases/JustFormulas.scala
index fada0552dda52fa2d73d8424807816f3028ebad7..bb902f0d5734d47a86062f2f56d0f6cc162af59f 100644
--- a/testcases/vmcai2011-testcases/JustFormulas.scala
+++ b/testcases/vmcai2011-testcases/JustFormulas.scala
@@ -2,7 +2,7 @@ import scala.collection.immutable.Set
object JustFormulas {
// These are just to provide some "uninterpreted function symbols"
- // Use the option -P:funcheck:tolerant to avoid warnings about it.
+ // Use the option -P:leon:tolerant to avoid warnings about it.
def f1(x: Int) : Int = { throw new Exception("Not implemented") }
def f2(s: Set[Int]) : Set[Int] = { throw new Exception("Not implemented") }
def f3(x: Int) : Set[Int] = { throw new Exception("Not implemented") }
diff --git a/testcases/vmcai2011-testcases/SanityChecks.scala b/testcases/vmcai2011-testcases/SanityChecks.scala
index 2eb68f673d75138ddd6d3462874c82b7e8f463fb..5ee5f3d962e4629974ee2c94b37bca4002f9f7c8 100644
--- a/testcases/vmcai2011-testcases/SanityChecks.scala
+++ b/testcases/vmcai2011-testcases/SanityChecks.scala
@@ -2,7 +2,7 @@ import scala.collection.immutable.Set
object SanityChecks {
// These are just to provide some "uninterpreted function symbols"
- // Use the option -P:funcheck:tolerant to avoid warnings about it.
+ // Use the option -P:leon:tolerant to avoid warnings about it.
def f1(x: Int) : Int = { throw new Exception("Not implemented") }
def f2(s: Set[Int]) : Set[Int] = { throw new Exception("Not implemented") }
def f3(x: Int) : Set[Int] = { throw new Exception("Not implemented") }
diff --git a/testcases/vstte10competition/AmortizedQueue.scala b/testcases/vstte10competition/AmortizedQueue.scala
index 9c049989dd5a734e213307d14a609bf95bfdc474..fa9d8f02322ff88bc7a7db6cf5be9d30f74b30af 100644
--- a/testcases/vstte10competition/AmortizedQueue.scala
+++ b/testcases/vstte10competition/AmortizedQueue.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object AmortizedQueue {
sealed abstract class List
diff --git a/testcases/vstte10competition/Injection.scala b/testcases/vstte10competition/Injection.scala
index 1bb8b3ee2de4f12523dd565e7dd591449471d32a..e20fdcedde55f429bb3c9718ffb2de52336dbce9 100644
--- a/testcases/vstte10competition/Injection.scala
+++ b/testcases/vstte10competition/Injection.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object Injection {
sealed abstract class List
diff --git a/testcases/vstte10competition/SearchLinkedList.scala b/testcases/vstte10competition/SearchLinkedList.scala
index d14b9fee6c000c5cc703a6e3b97af4ee1eba5562..2c137fd4ad6b9d411f7e14b4ada6b834234c9e9e 100644
--- a/testcases/vstte10competition/SearchLinkedList.scala
+++ b/testcases/vstte10competition/SearchLinkedList.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object SearchLinkedList {
sealed abstract class List
diff --git a/testcases/vstte10competition/SumAndMax.scala b/testcases/vstte10competition/SumAndMax.scala
index c4265e25b6e1846a5a0b8e47f1d8f224229131c0..0aa4ce7060a391d34dd047338fcd1f638054843f 100644
--- a/testcases/vstte10competition/SumAndMax.scala
+++ b/testcases/vstte10competition/SumAndMax.scala
@@ -1,5 +1,5 @@
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object SumAndMax {
sealed abstract class List