diff --git a/Library.scala b/Library.scala
index 551395c69c8bf1294df2b245b660ad763362be64..979bc50ee4932b1ac89f28e7a81d4998522bfbcc 100644
--- a/Library.scala
+++ b/Library.scala
@@ -1,78 +1,17 @@
-package leon
+package leon.library
 
 import leon.Annotations._
 import leon.Utils._
 
-object Library {
+object collections {
   /***
    * Lists
    ***/
 
-  sealed abstract class List[T] {
-    @verified
-    def size: Int = (this match {
-      case Nil() => 0
-      case Cons(h, t) => 1 + t.size
-    }) ensuring (_ >= 0)
-
-    @verified
-    def content: Set[T] = this match {
-      case Nil() => Set()
-      case Cons(h, t) => Set(h) ++ t.content
-    }
-
-    @verified
-    def contains(v: T): Boolean = (this match {
-      case Cons(h, t) if h == v => true
-      case Cons(_, t) => t.contains(v)
-      case Nil() => false
-    }) ensuring { res => res == (content contains v) }
-
-    @verified
-    def append(that: List[T]): List[T] = (this match {
-      case Nil() => that
-      case Cons(x, xs) => Cons(x, xs.append(that))
-    }) ensuring { _.content == this.content ++ that.content }
-
-    @verified
-    def head: T = {
-      require(this != Nil[T]())
-      this match {
-        case Cons(h, t) => h
-      }
-    }
-
-    @verified
-    def tail: List[T] = {
-      require(this != Nil[T]())
-      this match {
-        case Cons(h, t) => t
-      }
-    }
-  }
-
-  case class Cons[T](h: T, t: List[T]) extends List[T]
-  case class Nil[T]() extends List[T]
-
   /***
    * Options
    ***/
 
-  sealed abstract class Option[T] {
-    @verified
-    def getOrElse(default: T) = this match {
-      case Some(v) => v
-      case None()  => default
-    }
-
-    @verified
-    def orElse(or: Option[T]) = this match {
-      case Some(v) => this
-      case None() => or
-    }
-  }
-  case class Some[T](v: T) extends Option[T]
-  case class None[T]() extends Option[T]
 
 
 }
diff --git a/lib-bin/32/libz3.so b/lib-bin/32/libz3.so
deleted file mode 100755
index fe0854bcac7044575dc65529c15bbb2c3fb4da48..0000000000000000000000000000000000000000
Binary files a/lib-bin/32/libz3.so and /dev/null differ
diff --git a/library/Option.scala b/library/Option.scala
new file mode 100644
index 0000000000000000000000000000000000000000..06e6882f7bd7ddb243ef57c35851e6f859e46aa9
--- /dev/null
+++ b/library/Option.scala
@@ -0,0 +1,32 @@
+package leon
+
+import leon.annotation._
+
+sealed abstract class Option[T] {
+  @verified
+  def getOrElse(default: T) = this match {
+    case Some(v) => v
+    case None()  => default
+  }
+
+  @verified
+  def orElse(or: Option[T]) = this match {
+    case Some(v) => this
+    case None() => or
+  }
+
+  @verified
+  def isEmpty = this match {
+    case Some(v) => false
+    case None() =>  true
+  }
+
+  @verified
+  def nonEmpty  = !isEmpty
+
+  @verified
+  def isDefined = !isEmpty
+}
+
+case class Some[T](v: T) extends Option[T]
+case class None[T]() extends Option[T]
diff --git a/library/annotation/package.scala b/library/annotation/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..683ca09df9a73d6ea26fcf7d921ee2413c3b8d85
--- /dev/null
+++ b/library/annotation/package.scala
@@ -0,0 +1,14 @@
+package leon
+
+import scala.annotation.StaticAnnotation
+
+@annotation.ignore
+object annotation {
+  class induct     extends StaticAnnotation
+  class axiomatize extends StaticAnnotation
+  class main       extends StaticAnnotation
+  class verified   extends StaticAnnotation
+  class proxy      extends StaticAnnotation
+  class ignore     extends StaticAnnotation
+}
+
diff --git a/library/build.sbt b/library/build.sbt
deleted file mode 100644
index 0c4c88e13c3096c5e4b9976ab021083f8569aa38..0000000000000000000000000000000000000000
--- a/library/build.sbt
+++ /dev/null
@@ -1,15 +0,0 @@
-name := "Leon Library"
-
-version := "2.0"
-
-organization := "ch.epfl.lara"
-
-scalaVersion := "2.10.2"
-
-scalacOptions += "-deprecation"
-
-scalacOptions += "-unchecked"
-
-scalacOptions += "-feature"
-
-libraryDependencies += "org.scala-lang" % "scala-compiler" % "2.10.2"
diff --git a/library/collection/List.scala b/library/collection/List.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c3356cdcaf158a7b93e8cb69f6da20afc68d0a38
--- /dev/null
+++ b/library/collection/List.scala
@@ -0,0 +1,169 @@
+package leon.collection
+
+import leon.lang._
+import leon.annotation._
+
+sealed abstract class List[T] {
+  @verified
+  def size: Int = (this match {
+    case Nil() => 0
+    case Cons(h, t) => 1 + t.size
+  }) ensuring (_ >= 0)
+
+  @verified
+  def content: Set[T] = this match {
+    case Nil() => Set()
+    case Cons(h, t) => Set(h) ++ t.content
+  }
+
+  @verified
+  def contains(v: T): Boolean = (this match {
+    case Cons(h, t) if h == v => true
+    case Cons(_, t) => t.contains(v)
+    case Nil() => false
+  }) ensuring { res => res == (content contains v) }
+
+  @verified
+  def ++(that: List[T]): List[T] = (this match {
+    case Nil() => that
+    case Cons(x, xs) => Cons(x, xs ++ that)
+  }) ensuring { res => (res.content == this.content ++ that.content) && (res.size == this.size + that.size)}
+
+  @verified
+  def head: T = {
+    require(this != Nil[T]())
+    this match {
+      case Cons(h, t) => h
+    }
+  }
+
+  @verified
+  def tail: List[T] = {
+    require(this != Nil[T]())
+    this match {
+      case Cons(h, t) => t
+    }
+  }
+
+  @verified
+  def apply(index: Int): T = {
+    require(0 <= index && index < size)
+    if (index == 0) {
+      head
+    } else {
+       tail(index-1)
+    }
+  }
+
+  @verified
+  def :+(t:T): List[T] = {
+    this match {
+      case Nil() => Cons(t, this)
+      case Cons(x, xs) => Cons(x, xs :+ (t))
+    }
+  } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
+
+  @verified
+  def reverse: List[T] = {
+    this match {
+      case Nil() => this
+      case Cons(x,xs) => xs.reverse :+ x
+    }
+  } ensuring (res => (res.size == size) && (res.content == content))
+}
+
+
+case class Cons[T](h: T, t: List[T]) extends List[T]
+case class Nil[T]() extends List[T]
+
+object ListSpecs {
+  @verified
+  def snocIndex[T](l : List[T], t : T, i : Int) : Boolean = {
+    require(0 <= i && i < l.size + 1)
+    // proof:
+    (l match {
+      case Nil() => true
+      case Cons(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
+    }) &&
+    // claim:
+    ((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
+  }.holds
+
+  @verified
+  def reverseIndex[T](l : List[T], i : Int) : Boolean = {
+    require(0 <= i && i < l.size)
+    (l match {
+      case Nil() => true
+      case Cons(x,xs) => snocIndex(l, x, i) && reverseIndex[T](l,i)
+    }) &&
+    (l.reverse.apply(i) == l.apply(l.size - 1 - i))
+  }.holds
+
+  @verified
+  def appendIndex[T](l1 : List[T], l2 : List[T], i : Int) : Boolean = {
+    require(0 <= i && i < l1.size + l2.size)
+    (l1 match {
+      case Nil() => true
+      case Cons(x,xs) => if (i==0) true else appendIndex[T](xs,l2,i-1)
+    }) &&
+    ((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
+  }.holds
+
+  @verified
+  def appendAssoc[T](l1 : List[T], l2 : List[T], l3 : List[T]) : Boolean = {
+    (l1 match {
+      case Nil() => true
+      case Cons(x,xs) => appendAssoc(xs,l2,l3)
+    }) &&
+    (((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3)))
+  }.holds
+
+  @verified
+  def snocIsAppend[T](l : List[T], t : T) : Boolean = {
+    (l match {
+      case Nil() => true
+      case Cons(x,xs) =>  snocIsAppend(xs,t)
+    }) &&
+    ((l :+ t) == l ++ Cons[T](t, Nil()))
+  }.holds
+
+  @verified
+  def snocAfterAppend[T](l1 : List[T], l2 : List[T], t : T) : Boolean = {
+    (l1 match {
+      case Nil() => true
+      case Cons(x,xs) =>  snocAfterAppend(xs,l2,t)
+    }) &&
+    ((l1 ++ l2) :+ t == (l1 ++ (l2 :+ t)))
+  }.holds
+
+  @verified
+  def snocReverse[T](l : List[T], t : T) : Boolean = {
+    (l match {
+      case Nil() => true
+      case Cons(x,xs) => snocReverse(xs,t)
+    }) &&
+    ((l :+ t).reverse == Cons(t, l.reverse))
+  }.holds
+
+  @verified
+  def reverseReverse[T](l : List[T]) : Boolean = {
+    (l match {
+      case Nil() => true
+      case Cons(x,xs) => reverseReverse[T](xs) && snocReverse[T](xs.reverse, x)
+    }) &&
+    (l.reverse.reverse == l)
+  }.holds
+
+  //// my hand calculation shows this should work, but it does not seem to be found
+  //def reverseAppend[T](l1 : List[T], l2 : List[T]) : Boolean = {
+  //  (l1 match {
+  //    case Nil() => true
+  //    case Cons(x,xs) => {
+  //      reverseAppend(xs,l2) &&
+  //      snocAfterAppend[T](l2.reverse, xs.reverse, x) &&
+  //      l1.reverse == (xs.reverse :+ x)
+  //    }
+  //  }) &&
+  //  ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
+  //}.holds
+}
diff --git a/library/src/main/scala/leon/Utils.scala b/library/lang/package.scala
similarity index 91%
rename from library/src/main/scala/leon/Utils.scala
rename to library/lang/package.scala
index d34bcd0e9c36c572fa9b4948e71a7b7b09185b7e..cc6f5112233e21163fcb3fbe09277316e114f147 100644
--- a/library/src/main/scala/leon/Utils.scala
+++ b/library/lang/package.scala
@@ -1,10 +1,10 @@
-/* Copyright 2009-2013 EPFL, Lausanne */
-
 package leon
 
-import  scala.language.implicitConversions
+import leon.annotation._
+import scala.language.implicitConversions
 
-object Utils {
+@ignore
+object lang {
   sealed class IsValid(val property : Boolean) {
     def holds : Boolean = {
       assert(property)
@@ -19,8 +19,8 @@ object Utils {
   object InvariantFunction {
     def invariant(x: Boolean): Unit = ()
   }
-  implicit def while2Invariant(u: Unit) = InvariantFunction
 
+  implicit def while2Invariant(u: Unit) = InvariantFunction
 
   def waypoint[A](i: Int, expr: A): A = expr
 
diff --git a/library/src/main/scala/leon/Annotations.scala b/library/src/main/scala/leon/Annotations.scala
deleted file mode 100644
index f72dd66d04ce5f5dd0e4db4c36af8b3759c67c2c..0000000000000000000000000000000000000000
--- a/library/src/main/scala/leon/Annotations.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-/* Copyright 2009-2013 EPFL, Lausanne */
-
-package leon
-
-import scala.annotation.StaticAnnotation
-
-object Annotations {
-  class induct extends StaticAnnotation
-  class axiomatize extends StaticAnnotation
-  class main extends StaticAnnotation
-  class verified extends StaticAnnotation
-  class proxy extends StaticAnnotation
-}
diff --git a/project/Build.scala b/project/Build.scala
index b0551d5413ff85b1dd5384edc921f1af0a5a0652..bd6318a3ff4cbfbfbfb40d5a9cbdae18456e94d6 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -43,11 +43,6 @@ object Leon extends Build {
 
     val ldLibPath = if (is64) ldLibraryDir64.absolutePath else ldLibraryDir32.absolutePath
 
-    val leonLibPath = depsPaths.find(_.endsWith("/library/target/scala-2.10/classes")) match {
-      case None => throw new Exception("Couldn't find leon-library in the classpath.")
-      case Some(p) => p
-    }
-
     // One ugly hack... Likely to fail for Windows, but it's a Bash script anyway.
     s.log.info("Will use " + scalaHomeDir + " as SCALA_HOME.")
 
@@ -66,7 +61,10 @@ object Leon extends Build {
       sfw.write("fi"+ nl)
     }
     sfw.write("export LD_LIBRARY_PATH=\""+ldLibPath+"\"" + nl)
-    sfw.write("export LEON_LIBRARY_PATH=\""+leonLibPath+"\"" + nl)
+
+    val libFiles = file("library") ** "*.scala"
+
+    sfw.write("export LEON_LIBFILES=\""+libFiles.getPaths.mkString(" ")+"\"" + nl)
     sfw.write("export SCALA_HOME=\""+scalaHomeDir+"\"" + nl)
     sfw.close
     setupScriptFile.setExecutable(true)
@@ -121,8 +119,5 @@ object Leon extends Build {
     id = "leon",
     base = file("."),
     settings = Project.defaultSettings ++ LeonProject.settings
-  ) aggregate(leonLibrary) dependsOn(leonLibrary) 
-
-  lazy val leonLibrary = Project(id = "leon-library", base = file("./library"))
-
+  )
 }
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 1d5da5f55c89741d04e767405dd1baa6e0931cbb..ef65489357eb41ed109034e2d241fa7c107bdddf 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -30,6 +30,7 @@ object Main {
       LeonFlagOptionDef ("termination", "--termination",        "Check program termination"),
       LeonFlagOptionDef ("synthesis",   "--synthesis",          "Partial synthesis of choose() constructs"),
       LeonFlagOptionDef ("xlang",       "--xlang",              "Support for extra program constructs (imperative,...)"),
+      LeonFlagOptionDef ("library",     "--library",            "Inject Leon standard library"),
       LeonValueOptionDef("debug",       "--debug=<sections..>", "Enables specific messages"),
       LeonFlagOptionDef ("help",        "--help",               "Show help")
     )
@@ -128,8 +129,6 @@ object Main {
         Some(LeonValueOption(vod.name, value))
     }.toSeq
 
-
-
     var settings  = Settings()
 
     // Process options we understand:
@@ -138,6 +137,8 @@ object Main {
         settings = settings.copy(termination = value)
       case LeonFlagOption("synthesis", value) =>
         settings = settings.copy(synthesis = value)
+      case LeonFlagOption("library", value) =>
+        settings = settings.copy(injectLibrary = value)
       case LeonFlagOption("xlang", value) =>
         settings = settings.copy(xlang = value)
       case LeonValueOption("debug", ListValue(sections)) =>
@@ -213,8 +214,17 @@ object Main {
   def main(args : Array[String]) {
     val timer     = new Timer().start
 
+    val argsl = args.toList
+
+    // By default we add --library from Main
+    val realArgs = if (!args.exists(_.contains("--library"))) {
+      "--library" :: argsl
+    } else {
+      argsl
+    }
+
     // Process options
-    val ctx = processOptions(args.toList)
+    val ctx = processOptions(realArgs)
 
     try {
       ctx.interruptManager.registerSignalHandler()
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 63f116d7cc58a22fb1f33b8386d4a519a138320e..a4ef710c311b19bf04ecfc1085f14a502e8fcd8f 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -11,6 +11,7 @@ case class Settings(
   val synthesis: Boolean               = false,
   val xlang: Boolean                   = false,
   val verify: Boolean                  = true,
+  val injectLibrary: Boolean           = false,
   val classPath: List[String]          = Settings.defaultClassPath()
 )
 
@@ -20,13 +21,6 @@ object Settings {
   // one for the leon runtime library.
 
   private def defaultClassPath() = {
-    val leonLib = System.getenv("LEON_LIBRARY_PATH")
-    if (leonLib == "" || leonLib == null) {
-      sys.error("LEON_LIBRARY_PATH env variable is undefined")
-    }
-
-    val leonCPs = leonLib
-
     val scalaHome = System.getenv("SCALA_HOME")
     val scalaCPs = if (scalaHome != "") {
       val f = new java.io.File(scalaHome+"/lib")
@@ -39,6 +33,11 @@ object Settings {
       Nil
     }
 
-    leonCPs :: scalaCPs
+    scalaCPs
   }
+
+  private[leon] def defaultLibFiles() = {
+    Option(System.getenv("LEON_LIBFILES")).map(_.split(" ").toList).getOrElse(Nil)
+  }
+
 }
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index f609b810efa9f7af95edfcedb65a769ff115fb6b..d815a0549fa6b22dd0374f03e3fa20e5e1098e93 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -84,7 +84,7 @@ trait CodeGeneration {
         funDef.params.map(_.id).zipWithIndex.toMap
       }
 
-    val body = funDef.body.getOrElse(throw CompilationException("Can't compile a FunDef without body"))
+    val body = funDef.body.getOrElse(throw CompilationException("Can't compile a FunDef without body: "+funDef.id.name))
 
     val bodyWithPre = if(funDef.hasPrecondition && params.checkContracts) {
       IfExpr(funDef.precondition.get, body, Error("Precondition failed"))
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index a130ee946d0a4b033cb5526b1ce964ebfd54ce8e..3e7021f63e4c5f3d7545efadc995d4fea351f476 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -122,7 +122,7 @@ trait ASTExtractors {
 
     object ExHoldsExpression {
       def unapply(tree: Select) : Option[Tree] = tree match {
-        case Select(Apply(ExSelected("leon", "Utils", "any2IsValid"), realExpr :: Nil), ExNamed("holds")) =>
+        case Select(Apply(ExSelected("leon", "lang", "any2IsValid"), realExpr :: Nil), ExNamed("holds")) =>
             Some(realExpr)
         case _ => None
        }
@@ -233,7 +233,7 @@ trait ASTExtractors {
     object ExEpsilonExpression {
       def unapply(tree: Apply) : Option[(Type, Symbol, Tree)] = tree match {
         case Apply(
-              TypeApply(ExSelected("leon", "Utils", "epsilon"), typeTree :: Nil),
+              TypeApply(ExSelected("leon", "lang", "epsilon"), typeTree :: Nil),
               Function((vd @ ValDef(_, _, _, EmptyTree)) :: Nil, predicateBody) :: Nil) =>
             Some((typeTree.tpe, vd.symbol, predicateBody))
         case _ => None
@@ -242,7 +242,7 @@ trait ASTExtractors {
 
     object ExErrorExpression {
       def unapply(tree: Apply) : Option[(String, Type)] = tree match {
-        case a @ Apply(TypeApply(ExSelected("leon", "Utils", "error"), List(tpe)), List(lit : Literal)) =>
+        case a @ Apply(TypeApply(ExSelected("leon", "lang", "error"), List(tpe)), List(lit : Literal)) =>
           Some((lit.value.stringValue, tpe.tpe))
         case _ =>
           None
@@ -252,7 +252,7 @@ trait ASTExtractors {
     object ExChooseExpression {
       def unapply(tree: Apply) : Option[(List[(Type, Symbol)], Type, Tree, Tree)] = tree match {
         case a @ Apply(
-              TypeApply(s @ ExSelected("leon", "Utils", "choose"), types),
+              TypeApply(s @ ExSelected("leon", "lang", "choose"), types),
               Function(vds, predicateBody) :: Nil) =>
             Some(((types.map(_.tpe) zip vds.map(_.symbol)).toList, a.tpe, predicateBody, s))
         case _ => None
@@ -262,13 +262,22 @@ trait ASTExtractors {
     object ExWaypointExpression {
       def unapply(tree: Apply) : Option[(Type, Tree, Tree)] = tree match {
         case Apply(
-              TypeApply(ExSelected("leon", "Utils", "waypoint"), typeTree :: Nil),
+              TypeApply(ExSelected("leon", "lang", "waypoint"), typeTree :: Nil),
               List(i, expr)) =>
             Some((typeTree.tpe, i, expr))
         case _ => None
       }
     }
 
+    object ExArrayUpdated {
+      def unapply(tree: Apply): Option[(Tree,Tree,Tree)] = tree match {
+        case Apply(
+              Apply(TypeApply(Select(Apply(ExSelected("scala", "Predef", s), Seq(lhs)), n), _), Seq(index, value)),
+              List(Apply(_, _))) if (s.toString contains "Array") && (n.toString == "updated") => Some((lhs, index, value))
+        case _ => None
+      }
+    }
+
 
     object ExValDef {
       /** Extracts val's in the head of blocks. */
@@ -691,23 +700,6 @@ trait ASTExtractors {
       }
     }
 
-    object ExUpdated {
-      def unapply(tree: Apply): Option[(Tree,Tree,Tree)] = tree match {
-        case Apply(TypeApply(Select(lhs, n), typeTreeList), List(from, to)) if (n.toString == "updated") => 
-          Some((lhs, from, to))
-        case Apply(
-              Apply(TypeApply(Select(Apply(_, Seq(lhs)), n), _), Seq(index, value)),
-              List(Apply(_, _))) if (n.toString == "updated") => Some((lhs, index, value))
-        case _ => None
-      }
-    }
-
-    object ExApply {
-      def unapply(tree: Apply): Option[(Tree,List[Tree])] = tree match {
-        case Apply(Select(lhs, n), rhs) if (n.toString == "apply") => Some((lhs, rhs))
-        case _ => None
-      }
-    }
     object ExUpdate {
       def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match {
         case Apply(
@@ -717,28 +709,6 @@ trait ASTExtractors {
       }
     }
 
-    object ExMapIsDefinedAt {
-      def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
-        case Apply(Select(ExHasType(lhs, `mapSym`), n), List(rhs)) if (n.toString == "isDefinedAt") => Some((lhs, rhs))
-        case _ => None
-      }
-    }
-
-    object ExArrayLength {
-      def unapply(tree: Select): Option[Tree] = tree match {
-        case Select(ExHasType(t, `arraySym`), n) if n.toString == "length" => Some(t)
-        case _ => None
-      }
-    }
-
-    object ExArrayClone {
-      def unapply(tree: Apply): Option[Tree] = tree match {
-        case Apply(Select(ExHasType(t, `arraySym`), n), List()) if n.toString == "clone" => Some(t)
-        case _ => None
-      }
-    }
-
-
     object ExArrayFill {
       def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match {
         case Apply(
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 473319e886d8a16ae05889a80589ce2ec17d7782..523a487f3cd5223817fc69cad37e341a196593a4 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -32,6 +32,17 @@ trait CodeExtraction extends ASTExtractors {
   import ExtractorHelpers._
   import scala.collection.immutable.Set
 
+  def annotationsOf(s: Symbol): Set[String] = {
+    (for(a <- s.annotations) yield {
+      val name = a.atp.safeToString
+      if (name startsWith "leon.annotation.") {
+        Some(name.split("\\.", 3)(2))
+      } else {
+        None
+      }
+    }).flatten.toSet
+  }
+
   implicit def scalaPosToLeonPos(p: global.Position): LeonPosition = {
     if (p == NoPosition) {
       leon.utils.NoPosition
@@ -119,13 +130,15 @@ trait CodeExtraction extends ASTExtractors {
     case class DefContext(
         tparams: Map[Symbol, TypeParameter] = Map(),
         vars: Map[Symbol, () => LeonExpr] = Map(),
-        mutableVars: Map[Symbol, () => LeonExpr] = Map()
+        mutableVars: Map[Symbol, () => LeonExpr] = Map(),
+        isProxy: Boolean = false
       ) {
 
       def union(that: DefContext) = {
         copy(this.tparams ++ that.tparams,
              this.vars ++ that.vars,
-             this.mutableVars ++ that.mutableVars)
+             this.mutableVars ++ that.mutableVars,
+             this.isProxy || that.isProxy)
       }
 
       def isVariable(s: Symbol) = (vars contains s) || (mutableVars contains s)
@@ -145,16 +158,40 @@ trait CodeExtraction extends ASTExtractors {
 
     def extractModules: List[LeonModuleDef] = {
       try {
-        val templates = units.reverse.flatMap { u => u.body match {
+        val templates: List[(String, List[Tree])] = units.reverse.flatMap { u => u.body match {
           case PackageDef(name, lst) =>
-            lst.flatMap { _ match {
+            var standaloneDefs = List[Tree]()
+
+            val modules: List[(String, List[Tree])] = lst.flatMap { _ match {
+              case od @ ExObjectDef(_, _) if annotationsOf(od.symbol) contains "ignore" =>
+                None
+
               case ExObjectDef(n, templ) =>
-                Some((n.toString, templ))
+                Some((n.toString, templ.body))
 
-              case other @ _ =>
-                outOfSubsetError(other, "Expected: top-level object.")
+              case d @ ExAbstractClass(_, _, _) =>
+                standaloneDefs ::= d
                 None
-            }}
+
+              case d @ ExCaseClass(_, _, _, _) =>
+                standaloneDefs ::= d
+                None
+
+              case d @ ExCaseClassSyntheticJunk() =>
+                None
+
+              case other =>
+                outOfSubsetError(other, "Expected: top-level object/class.")
+                None
+            }}.toList
+
+            val extraModules: List[(String, List[Tree])] = if (standaloneDefs.isEmpty) {
+              Nil
+            } else {
+              List(("standalone", standaloneDefs.reverse))
+            }
+
+            modules ++ extraModules
         }}
 
         // Phase 1, we detect classes/types
@@ -185,9 +222,9 @@ trait CodeExtraction extends ASTExtractors {
     private var seenClasses = Map[Symbol, (Seq[(String, Tree)], Template)]()
     private var classesToClasses  = Map[Symbol, LeonClassDef]()
 
-    private def collectClassSymbols(tmpl: Template) {
+    private def collectClassSymbols(defs: List[Tree]) {
       // We collect all defined classes
-      for (t <- tmpl.body) t match {
+      for (t <- defs) t match {
         case ExAbstractClass(o2, sym, tmpl) =>
           seenClasses += sym -> ((Nil, tmpl))
 
@@ -198,9 +235,9 @@ trait CodeExtraction extends ASTExtractors {
       }
     }
 
-    private def extractClassDefs(tmpl: Template) {
+    private def extractClassDefs(defs: List[Tree]) {
       // We collect all defined classes
-      for (t <- tmpl.body) t match {
+      for (t <- defs) t match {
         case ExAbstractClass(o2, sym, _) =>
           getClassDef(sym, NoPosition)
 
@@ -335,7 +372,9 @@ trait CodeExtraction extends ASTExtractors {
       // Type params of the function itself
       val tparams = extractTypeParams(sym.typeParams.map(_.tpe))
 
-      val nctx = dctx.copy(tparams = dctx.tparams ++ tparams.toMap)
+      val isProxy = annotationsOf(sym) contains "proxy"
+
+      val nctx = dctx.copy(tparams = dctx.tparams ++ tparams.toMap, isProxy = isProxy)
 
       val newParams = sym.info.paramss.flatten.map{ sym =>
         val ptpe = toPureScalaType(sym.tpe)(nctx)
@@ -354,21 +393,16 @@ trait CodeExtraction extends ASTExtractors {
 
       fd.setPos(sym.pos)
 
-      for(a <- sym.annotations) {
-        val name = a.atp.safeToString
-        if (name startsWith "leon.Annotations.") {
-          fd.addAnnotation(name.split("\\.", 3)(2))
-        }
-      }
+      fd.addAnnotation(annotationsOf(sym).toSeq : _*)
 
       defsToDefs += sym -> fd
 
       fd
     }
 
-    private def collectFunSigs(tmpl: Template) = {
+    private def collectFunSigs(defs: List[Tree]) = {
       // We collect defined function bodies
-      for (d <- tmpl.body) d match {
+      for (d <- defs) d match {
         case ExMainFunctionDef() =>
           // Ignoring...
 
@@ -379,9 +413,9 @@ trait CodeExtraction extends ASTExtractors {
       }
     }
 
-    private def extractMethodDefs(tmpl: Template) = {
+    private def extractMethodDefs(defs: List[Tree]) = {
       // We collect defined function bodies
-      for (d <- tmpl.body) d match {
+      for (d <- defs) d match {
         case ExAbstractClass(_, csym, tmpl) =>
           val cd = classesToClasses(csym)
 
@@ -412,9 +446,9 @@ trait CodeExtraction extends ASTExtractors {
       }
     }
 
-    private def extractFunDefs(tmpl: Template) = {
+    private def extractFunDefs(defs: List[Tree]) = {
       // We collect defined function bodies
-      for (d <- tmpl.body) d match {
+      for (d <- defs) d match {
         case ExMainFunctionDef() =>
           // Ignoring...
 
@@ -439,9 +473,9 @@ trait CodeExtraction extends ASTExtractors {
       }
     }
 
-    private def extractObjectDef(nameStr: String, tmpl: Template): LeonModuleDef = {
+    private def extractObjectDef(nameStr: String, defs: List[Tree]): LeonModuleDef = {
 
-      val defs = tmpl.body.flatMap{ t => t match {
+      val newDefs = defs.flatMap{ t => t match {
         case ExAbstractClass(o2, sym, _) =>
           Some(classesToClasses(sym))
 
@@ -460,18 +494,19 @@ trait CodeExtraction extends ASTExtractors {
       }}
 
       // We check nothing else is polluting the object
-      for (t <- tmpl.body) t match {
+      for (t <- defs) t match {
         case ExCaseClassSyntheticJunk() =>
         case ExAbstractClass(_,_,_) =>
         case ExCaseClass(_,_,_,_) =>
         case ExConstructorDef() =>
         case ExMainFunctionDef() =>
         case ExFunctionDef(_, _, _, _, _) =>
+        case defn if annotationsOf(defn.symbol) contains "ignore" =>
         case tree =>
           outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");
       }
 
-      new LeonModuleDef(FreshIdentifier(nameStr), defs)
+      new LeonModuleDef(FreshIdentifier(nameStr), newDefs)
     }
 
 
@@ -590,7 +625,7 @@ trait CodeExtraction extends ASTExtractors {
       case Ident(nme.WILDCARD) =>
         (WildcardPattern(binder).setPos(p.pos), dctx)
 
-      case s @ Select(This(_), b) if s.tpe.typeSymbol.isCase  =>
+      case s @ Select(_, b) if s.tpe.typeSymbol.isCase  =>
         // case Obj =>
         extractType(s.tpe) match {
           case ct: CaseClassType =>
@@ -621,7 +656,7 @@ trait CodeExtraction extends ASTExtractors {
         }
 
       case _ =>
-        outOfSubsetError(p, "Unsupported pattern: "+p)
+        outOfSubsetError(p, "Unsupported pattern: "+p.getClass)
     }
 
     private def extractMatchCase(cd: CaseDef)(implicit dctx: DefContext): MatchCase = {
@@ -717,12 +752,7 @@ trait CodeExtraction extends ASTExtractors {
 
           val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap
 
-          for(a <- d.symbol.annotations) {
-            val name = a.atp.safeToString
-            if (name startsWith "leon.Annotations.") {
-              fd.addAnnotation(name.split("\\.", 3)(2))
-            }
-          }
+          fd.addAnnotation(annotationsOf(d.symbol).toSeq : _*)
 
           val newDctx = dctx.copy(tparams = dctx.tparams ++ tparamsMap)
 
@@ -961,52 +991,6 @@ trait CodeExtraction extends ASTExtractors {
 
           FiniteMap(singletons).setType(tpe)
 
-        case up @ ExUpdated(m, f, t) =>
-          val rm = extractTree(m)
-          val rf = extractTree(f)
-          val rt = extractTree(t)
-
-          rm.getType match {
-            case t @ MapType(ft, tt) =>
-              MapUnion(rm, FiniteMap(Seq((rf, rt))).setType(t)).setType(t)
-
-            case t @ ArrayType(bt) =>
-              ArrayUpdated(rm, rf, rt).setType(t)
-
-            case _ =>
-              outOfSubsetError(tr, "updated can only be applied to maps.")
-          }
-
-        case ExMapIsDefinedAt(m,k) =>
-          val rm = extractTree(m)
-          val rk = extractTree(k)
-          MapIsDefinedAt(rm, rk)
-
-        case app @ ExApply(lhs,args) =>
-          val rlhs = extractTree(lhs)
-          val rargs = args map extractTree
-
-          rlhs.getType match {
-            case MapType(_,tt) =>
-              assert(rargs.size == 1)
-              MapGet(rlhs, rargs.head).setType(tt)
-
-            case ArrayType(bt) =>
-              assert(rargs.size == 1)
-              ArraySelect(rlhs, rargs.head).setType(bt)
-
-            case _ =>
-              outOfSubsetError(tr, "apply on unexpected type")
-          }
-
-        case ExArrayLength(t) =>
-          val rt = extractTree(t)
-          ArrayLength(rt)
-
-        case ExArrayClone(t) =>
-          val rt = extractTree(t)
-          ArrayClone(rt)
-
         case ExArrayFill(baseType, length, defaultValue) =>
           val underlying = extractType(baseType.tpe)
           val lengthRec = extractTree(length)
@@ -1070,6 +1054,13 @@ trait CodeExtraction extends ASTExtractors {
               outOfSubsetError(t, "Invalid usage of `this`")
           }
 
+        case aup @ ExArrayUpdated(ar, k, v) =>
+          val rar = extractTree(ar)
+          val rk = extractTree(k)
+          val rv = extractTree(v)
+
+          ArrayUpdated(rar, rk, rv)
+
         case c @ ExCall(rec, sym, tps, args) =>
           val rrec = rec match {
             case t if (defsToDefs contains sym) && !isMethod(sym) =>
@@ -1102,41 +1093,71 @@ trait CodeExtraction extends ASTExtractors {
 
               CaseClassSelector(cct, rec, fieldID)
 
-            case (IsTyped(_, SetType(base)), "min", Nil) =>
-              SetMin(rrec).setType(base)
+            // Set methods
+            case (IsTyped(a1, SetType(b1)), "min", Nil) =>
+              SetMin(a1).setType(b1)
 
-            case (IsTyped(_, SetType(base)), "max", Nil) =>
-              SetMax(rrec).setType(base)
-
-            case (IsTyped(_, MultisetType(base)), "toSet", Nil) =>
-              MultisetToSet(rrec).setType(base)
+            case (IsTyped(a1, SetType(b1)), "max", Nil) =>
+              SetMax(a1).setType(b1)
 
             case (IsTyped(a1, SetType(b1)), "++", List(IsTyped(a2, SetType(b2))))  if b1 == b2 =>
               SetUnion(a1, a2).setType(SetType(b1))
 
-            case (IsTyped(a1, MultisetType(b1)), "++", List(IsTyped(a2, MultisetType(b2))))  if b1 == b2 =>
-              MultisetUnion(a1, a2).setType(MultisetType(b1))
-
             case (IsTyped(a1, SetType(b1)), "&", List(IsTyped(a2, SetType(b2)))) if b1 == b2 =>
               SetIntersection(a1, a2).setType(SetType(b1))
 
-            case (IsTyped(a1, MultisetType(b1)), "&", List(IsTyped(a2, MultisetType(b2)))) if b1 == b2 =>
-              MultisetIntersection(a1, a2).setType(MultisetType(b1))
-
             case (IsTyped(a1, SetType(b1)), "subsetOf", List(IsTyped(a2, SetType(b2)))) if b1 == b2 =>
               SubsetOf(a1, a2)
 
             case (IsTyped(a1, SetType(b1)), "--", List(IsTyped(a2, SetType(b2)))) if b1 == b2 =>
               SetDifference(a1, a2).setType(SetType(b1))
 
+            case (IsTyped(a1, SetType(b1)), "contains", List(a2)) =>
+              ElementOfSet(a2, a1)
+
+
+            // Multiset methods
+            case (IsTyped(a1, MultisetType(b1)), "++", List(IsTyped(a2, MultisetType(b2))))  if b1 == b2 =>
+              MultisetUnion(a1, a2).setType(MultisetType(b1))
+
+            case (IsTyped(a1, MultisetType(b1)), "&", List(IsTyped(a2, MultisetType(b2)))) if b1 == b2 =>
+              MultisetIntersection(a1, a2).setType(MultisetType(b1))
+
             case (IsTyped(a1, MultisetType(b1)), "--", List(IsTyped(a2, MultisetType(b2)))) if b1 == b2 =>
               MultisetDifference(a1, a2).setType(MultisetType(b1))
 
             case (IsTyped(a1, MultisetType(b1)), "+++", List(IsTyped(a2, MultisetType(b2)))) if b1 == b2 =>
               MultisetPlus(a1, a2).setType(MultisetType(b1))
 
-            case (IsTyped(a1, SetType(b1)), "contains", List(a2)) =>
-              ElementOfSet(a2, a1)
+            case (IsTyped(_, MultisetType(b1)), "toSet", Nil) =>
+              MultisetToSet(rrec).setType(b1)
+
+            // Array methods
+            case (IsTyped(a1, ArrayType(vt)), "apply", List(a2)) =>
+              ArraySelect(a1, a2).setType(vt)
+
+            case (IsTyped(a1, at: ArrayType), "length", Nil) =>
+              ArrayLength(a1)
+
+            case (IsTyped(a1, at: ArrayType), "clone", Nil) =>
+              ArrayClone(a1).setType(at)
+
+            case (IsTyped(a1, at: ArrayType), "updated", List(k, v)) =>
+              ArrayUpdated(a1, k, v).setType(at)
+
+
+            // Map methods
+            case (IsTyped(a1, MapType(_, vt)), "apply", List(a2)) =>
+              MapGet(a1, a2).setType(vt)
+
+            case (IsTyped(a1, mt: MapType), "isDefinedAt", List(a2)) =>
+              MapIsDefinedAt(a1, a2)
+
+            case (IsTyped(a1, mt: MapType), "contains", List(a2)) =>
+              MapIsDefinedAt(a1, a2)
+
+            case (IsTyped(a1, mt: MapType), "updated", List(k, v)) =>
+              MapUnion(a1, FiniteMap(Seq((k, v))).setType(mt)).setType(mt)
 
             case (_, name, _) =>
               outOfSubsetError(tr, "Unknown call to "+name)
@@ -1204,7 +1225,7 @@ trait CodeExtraction extends ASTExtractors {
             outOfSubsetError(NoPosition, "Unknown type parameter "+sym)
           }
         } else {
-          classDefToClassType(getClassDef(sym, NoPosition), leontps)
+          getClassType(sym, leontps)
         }
 
       case tt: ThisType =>
@@ -1212,12 +1233,30 @@ trait CodeExtraction extends ASTExtractors {
         classDefToClassType(cd, cd.tparams.map(_.tp)) // Typed using own's type parameters
 
       case SingleType(_, sym) =>
-        classDefToClassType(getClassDef(sym.moduleClass, NoPosition), Nil)
+        getClassType(sym.moduleClass, Nil)
 
       case _ =>
         outOfSubsetError(tpt.typeSymbol.pos, "Could not extract type as PureScala: "+tpt+" ("+tpt.getClass+")")
     }
 
+    private var unknownsToTP        = Map[Symbol, TypeParameter]()
+
+    private def getClassType(sym: Symbol, tps: List[LeonType])(implicit dctx: DefContext) = {
+      if (seenClasses contains sym) {
+        classDefToClassType(getClassDef(sym, NoPosition), tps)
+      } else {
+        if (dctx.isProxy) {
+          unknownsToTP.getOrElse(sym, {
+            val tp = TypeParameter(FreshIdentifier(sym.name.toString, true))
+            unknownsToTP += sym -> tp
+            tp
+          })
+        } else {
+          outOfSubsetError(NoPosition, "Unknown class "+sym.name)
+        }
+      }
+    }
+
     private def getReturnedExpr(expr: LeonExpr): Seq[LeonExpr] = expr match {
       case Let(_, _, rest) => getReturnedExpr(rest)
       case LetVar(_, _, rest) => getReturnedExpr(rest)
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index ca7b1d66dd92d103bea011ca4111124e53817d86..a88ac222a9edb37dcb3190261a08b4271ae84e03 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -24,7 +24,15 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
     settings.classpath.value = ctx.settings.classPath.mkString(":")
     settings.skip.value      = List("patmat")
 
-    val compilerOpts = args.filterNot(_.startsWith("--"))
+    val libFiles = Settings.defaultLibFiles()
+
+    val injected = if (ctx.settings.injectLibrary) {
+      libFiles
+    } else {
+      libFiles.filter(f => f.contains("/lang/") || f.contains("/annotation/"))
+    }
+
+    val compilerOpts = injected ::: args.filterNot(_.startsWith("--"))
 
     val command = new CompilerCommand(compilerOpts, settings) {
       override val cmdName = "leon"
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 9c53593cbdc5d94b27def93186291a10c50f99d5..bbab146781b886a1210e1458485f63ff292f9e9f 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -179,7 +179,6 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
         pp(v, p)
         sb.append(")")
 
-      case ArrayMake(v) => sys.error("Not Scala Code")
       case ArraySelect(ar, i) =>
         pp(ar, p)
         sb.append("(")
@@ -256,7 +255,7 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
       case Not(expr) => sb.append("!"); optParentheses { pp(expr, p) }
 
       case e @ Error(desc) => {
-        sb.append("leon.Utils.error[")
+        sb.append("leon.lang.error[")
         pp(e.getType, p)
         sb.append("](\"" + desc + "\")")
       }
diff --git a/src/main/scala/leon/utils/TemporaryInputPhase.scala b/src/main/scala/leon/utils/TemporaryInputPhase.scala
index 216f46dd223937b4feca247a8806eba7267a6b72..9d77ad4152c0f6025e2289f9cc6206090d46c35e 100644
--- a/src/main/scala/leon/utils/TemporaryInputPhase.scala
+++ b/src/main/scala/leon/utils/TemporaryInputPhase.scala
@@ -19,6 +19,7 @@ object TemporaryInputPhase extends LeonPhase[(String, List[String]), List[String
     out.write(content)
     out.close
 
-    file.getAbsolutePath() :: opts
+
+    (file.getAbsolutePath() :: opts)
   }
 }
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 3b46b29d907dcc37ad8d31b7a74173269ac77792..7a093ebadb0925f45699c5d6e3b64f5eb6dabec8 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -93,9 +93,6 @@ object Trees {
 
     def printWith(printer: PrettyPrinter)(implicit lvl: Int) {
       printer match {
-        case _: ScalaPrinter =>
-          sys.error("Not Scala Code")
-
         case _ =>
           printer.append("epsilon(x" + this.getPos.line + "_" + this.getPos.col + ". ")
           printer.pp(pred, Some(this))
@@ -157,9 +154,6 @@ object Trees {
 
     def printWith(printer: PrettyPrinter)(implicit lvl: Int) {
       printer match {
-        case _: ScalaPrinter =>
-          sys.error("Not Scala Code")
-
         case _ =>
           printer.append("waypoint_" + i + "(")
           printer.pp(expr, Some(this))
diff --git a/src/test/resources/regression/synthesis/Church/Add.scala b/src/test/resources/regression/synthesis/Church/Add.scala
index 7b1b6b95fb9e928e031e91ac359e4f64ae1a663d..f9374897c38824193ef6167ebcdda286f35c0690 100644
--- a/src/test/resources/regression/synthesis/Church/Add.scala
+++ b/src/test/resources/regression/synthesis/Church/Add.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 object ChurchNumerals {
   sealed abstract class Num
   case object Z extends Num
diff --git a/src/test/resources/regression/synthesis/Church/Distinct.scala b/src/test/resources/regression/synthesis/Church/Distinct.scala
index a7a0189c20070a28393bb97be7f8066f82939662..9472f04f7922f71d5819bef023b663479b13a5e6 100644
--- a/src/test/resources/regression/synthesis/Church/Distinct.scala
+++ b/src/test/resources/regression/synthesis/Church/Distinct.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 object ChurchNumerals {
   sealed abstract class Num
   case object Z extends Num
diff --git a/src/test/resources/regression/synthesis/Church/Mult.scala b/src/test/resources/regression/synthesis/Church/Mult.scala
index 42519e663c4f59cb118a47854ed98ad2bd6b22df..bb51979eaafdf4ab9a665666f2e11c6ace81cb98 100644
--- a/src/test/resources/regression/synthesis/Church/Mult.scala
+++ b/src/test/resources/regression/synthesis/Church/Mult.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 object ChurchNumerals {
   sealed abstract class Num
   case object Z extends Num
diff --git a/src/test/resources/regression/synthesis/Church/Squared.scala b/src/test/resources/regression/synthesis/Church/Squared.scala
index 096f212a617c433eaf474010dc1e203c86cfce7e..08a71c46288b4b6b0a9eb2d0763e06bc8387a763 100644
--- a/src/test/resources/regression/synthesis/Church/Squared.scala
+++ b/src/test/resources/regression/synthesis/Church/Squared.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 object ChurchNumerals {
   sealed abstract class Num
   case object Z extends Num
diff --git a/src/test/resources/regression/synthesis/List/Delete.scala b/src/test/resources/regression/synthesis/List/Delete.scala
index 9fdef981b563018e52f43a49af6fd468e1395dc5..998249371a3ed370b319990662061237e7c9eb9f 100644
--- a/src/test/resources/regression/synthesis/List/Delete.scala
+++ b/src/test/resources/regression/synthesis/List/Delete.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Delete {
   sealed abstract class List
diff --git a/src/test/resources/regression/synthesis/List/Diff.scala b/src/test/resources/regression/synthesis/List/Diff.scala
index 3e7121eb18b807f746530aa6c1a165960343e1cf..a6c2c181db716f9f546c80df3c720987d2e985c4 100644
--- a/src/test/resources/regression/synthesis/List/Diff.scala
+++ b/src/test/resources/regression/synthesis/List/Diff.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Diff {
   sealed abstract class List
diff --git a/src/test/resources/regression/synthesis/List/Insert.scala b/src/test/resources/regression/synthesis/List/Insert.scala
index e5b21b45d3fcf090c6af8bd3fa7dd40f45ef00f5..91862f1a6440df3d6dff68ab4e9b5560e922392a 100644
--- a/src/test/resources/regression/synthesis/List/Insert.scala
+++ b/src/test/resources/regression/synthesis/List/Insert.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Insert {
   sealed abstract class List
diff --git a/src/test/resources/regression/synthesis/List/Split.scala b/src/test/resources/regression/synthesis/List/Split.scala
index 5aa4a8f1f309475a19eb466d0e871c72cab416fb..649f0b8b1e50aece88c4095baf9a4e4b215950f9 100644
--- a/src/test/resources/regression/synthesis/List/Split.scala
+++ b/src/test/resources/regression/synthesis/List/Split.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/src/test/resources/regression/synthesis/List/Union.scala b/src/test/resources/regression/synthesis/List/Union.scala
index adcc943fdabb9052c50c84f1ec58e80d8432ef99..c92d0c6c0bcba2cd53738e39e6943e4d365f45af 100644
--- a/src/test/resources/regression/synthesis/List/Union.scala
+++ b/src/test/resources/regression/synthesis/List/Union.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Union {
   sealed abstract class List
diff --git a/src/test/resources/regression/termination/looping/Looping1.scala.BAK b/src/test/resources/regression/termination/looping/Looping1.scala.BAK
index b21e705bfbbca9e6a3798552e531b4f74605eec2..04affc48125c5a918c18145c4779acd120c109c6 100644
--- a/src/test/resources/regression/termination/looping/Looping1.scala.BAK
+++ b/src/test/resources/regression/termination/looping/Looping1.scala.BAK
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object ComplexChains {
   
diff --git a/src/test/resources/regression/termination/looping/Looping2.scala.BAK b/src/test/resources/regression/termination/looping/Looping2.scala.BAK
index fc1da261e0a61777fa717b91bdb4d2f46c6b45c2..ac3cf66aeaf4d5309e2749b46ec800699ab64e32 100644
--- a/src/test/resources/regression/termination/looping/Looping2.scala.BAK
+++ b/src/test/resources/regression/termination/looping/Looping2.scala.BAK
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object ComplexChains {
   
diff --git a/src/test/resources/regression/termination/looping/Looping3.scala.BAK b/src/test/resources/regression/termination/looping/Looping3.scala.BAK
index c6d81a758ae100afdf4f2f16e3ce5942d0580fb8..29b3c9f82ab0f5508eb9b6785a3428e17304cdbe 100644
--- a/src/test/resources/regression/termination/looping/Looping3.scala.BAK
+++ b/src/test/resources/regression/termination/looping/Looping3.scala.BAK
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object ComplexChains {
   
diff --git a/src/test/resources/regression/termination/looping/Numeric1.scala b/src/test/resources/regression/termination/looping/Numeric1.scala
index 6949040ed6ce052781d1d0f9c40d277fcfc9de44..e6a95425a9fbfcfd62acfbaf4aa8e1aab48b9e6c 100644
--- a/src/test/resources/regression/termination/looping/Numeric1.scala
+++ b/src/test/resources/regression/termination/looping/Numeric1.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Numeric {
   // division by 0 loops
diff --git a/src/test/resources/regression/termination/looping/Numeric2.scala b/src/test/resources/regression/termination/looping/Numeric2.scala
index 0d5c2c04f76c745a773b2818176feb0bc7688756..e6e9b38d9dc34939ce4c6b27481e8f74f02dd8d4 100644
--- a/src/test/resources/regression/termination/looping/Numeric2.scala
+++ b/src/test/resources/regression/termination/looping/Numeric2.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Numeric {
   def looping1(x: Int): Int = looping2(x - 1)
diff --git a/src/test/resources/regression/termination/looping/Termination_failling1.scala b/src/test/resources/regression/termination/looping/Termination_failling1.scala
index 17b6be8645527074b5f95b0d0012d5b10c4691c7..a43e3cb0411e5838db48062fb572d7f9dec00b26 100644
--- a/src/test/resources/regression/termination/looping/Termination_failling1.scala
+++ b/src/test/resources/regression/termination/looping/Termination_failling1.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Termination {
   abstract class List
diff --git a/src/test/resources/regression/termination/unknown/Numeric3.scala b/src/test/resources/regression/termination/unknown/Numeric3.scala
index fd99e3132107da080723fc126f25c2b402a8c7dd..ccc9f114543253be9e9b96865dc6d05f7fe29ecb 100644
--- a/src/test/resources/regression/termination/unknown/Numeric3.scala
+++ b/src/test/resources/regression/termination/unknown/Numeric3.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Numeric3 {
   def unknown(x: Int) : Int = if (x > 0) unknown(x - 1) else unknown(5)
diff --git a/src/test/resources/regression/termination/valid/BinaryTreeImp.scala b/src/test/resources/regression/termination/valid/BinaryTreeImp.scala
index 3005d199122e373e29cdc3ce19f932be29eb4c3d..77dee8dfbda14920bc2f1ef5431ad52ec4d8ddca 100644
--- a/src/test/resources/regression/termination/valid/BinaryTreeImp.scala
+++ b/src/test/resources/regression/termination/valid/BinaryTreeImp.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinaryTree { 
  
diff --git a/src/test/resources/regression/termination/valid/BubbleSort.scala b/src/test/resources/regression/termination/valid/BubbleSort.scala
index 3551ebf16416f68bd932adc512177edc6f2611d8..4f29a00b0ecefdc4e7a8a9757102e32281738394 100644
--- a/src/test/resources/regression/termination/valid/BubbleSort.scala
+++ b/src/test/resources/regression/termination/valid/BubbleSort.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 /* The calculus of Computation textbook */
 
diff --git a/src/test/resources/regression/termination/valid/ComplexChains.scala b/src/test/resources/regression/termination/valid/ComplexChains.scala
index 68fad00ff27e5db7529c861a59f662af6e43a62f..d6c3ccd47177ed16b2057b6113e48e16e06dd9b2 100644
--- a/src/test/resources/regression/termination/valid/ComplexChains.scala
+++ b/src/test/resources/regression/termination/valid/ComplexChains.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object ComplexChains {
   
diff --git a/src/test/resources/regression/termination/valid/HardChains.scala.BAK b/src/test/resources/regression/termination/valid/HardChains.scala.BAK
index 4ffe63f60b4d651cd9d4d9fd29a1667da4b9c532..9efb8304e7703be1a9f3e166aa6043aa8ec4bd8c 100644
--- a/src/test/resources/regression/termination/valid/HardChains.scala.BAK
+++ b/src/test/resources/regression/termination/valid/HardChains.scala.BAK
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object HardChains {
   
diff --git a/src/test/resources/regression/termination/valid/ListWithSize.scala b/src/test/resources/regression/termination/valid/ListWithSize.scala
index 4e236ae1f7ffac822c932a46168ee31a752b7831..5e52bf74b944f2016cdc7651bafbdec7465b0ee0 100644
--- a/src/test/resources/regression/termination/valid/ListWithSize.scala
+++ b/src/test/resources/regression/termination/valid/ListWithSize.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object ListWithSize {
     sealed abstract class List
diff --git a/src/test/resources/regression/termination/valid/Numeric1.scala b/src/test/resources/regression/termination/valid/Numeric1.scala
index 2c4f65137b42c124a9291c1e11be7b31f66cb02e..c9ad2a12f22e3c5e94f82e672af268acf4abf009 100644
--- a/src/test/resources/regression/termination/valid/Numeric1.scala
+++ b/src/test/resources/regression/termination/valid/Numeric1.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Numeric {
 
diff --git a/src/test/resources/regression/termination/valid/SimpInterpret.scala b/src/test/resources/regression/termination/valid/SimpInterpret.scala
index fd56989f4a4597e2b9e39fb19acdabd0d2cd6d93..52e173af42493fbc6b3bda8312b246685cf9ff6b 100644
--- a/src/test/resources/regression/termination/valid/SimpInterpret.scala
+++ b/src/test/resources/regression/termination/valid/SimpInterpret.scala
@@ -1,6 +1,6 @@
 //import scala.collection.immutable.Set
-//import leon.Annotations._
-import leon.Utils._
+//import leon.annotation._
+import leon.lang._
 
 object Interpret {
   abstract class BoolTree 
diff --git a/src/test/resources/regression/termination/valid/Termination_passing1.scala b/src/test/resources/regression/termination/valid/Termination_passing1.scala
index ea86b67694431ef9efa7eadb30b0a08cac30b4ea..8f0a6f2bd2aee08fb39190cc483420dbf05097db 100644
--- a/src/test/resources/regression/termination/valid/Termination_passing1.scala
+++ b/src/test/resources/regression/termination/valid/Termination_passing1.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Termination {
   abstract class List
diff --git a/src/test/resources/regression/termination/valid/Termination_passing2.scala b/src/test/resources/regression/termination/valid/Termination_passing2.scala
index 8fbbcd83e961a7f5b2cbffcbec3cba470a16a9d5..e8d944bfbd247db77e88fd2ede2a45ca7a100a1d 100644
--- a/src/test/resources/regression/termination/valid/Termination_passing2.scala
+++ b/src/test/resources/regression/termination/valid/Termination_passing2.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Termination {
   def f1(x: Int, b: Boolean) : Int = {
diff --git a/src/test/resources/regression/transformations/Match.scala b/src/test/resources/regression/transformations/Match.scala
index 455517fcc564dedc373771e219af4f430a7b6fad..3af11e05e4af7dc7f316d151f63f3a407eddacfa 100644
--- a/src/test/resources/regression/transformations/Match.scala
+++ b/src/test/resources/regression/transformations/Match.scala
@@ -1,7 +1,7 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Transform {
     sealed abstract class List
diff --git a/src/test/resources/regression/transformations/SimplifyLets.scala b/src/test/resources/regression/transformations/SimplifyLets.scala
index a096199bee82bb676a9bedc5842ee3cb4eb3d66e..24d8509324ce3a01a17248248c3ca27ff0a9f9ee 100644
--- a/src/test/resources/regression/transformations/SimplifyLets.scala
+++ b/src/test/resources/regression/transformations/SimplifyLets.scala
@@ -1,7 +1,7 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Transform {
     sealed abstract class List
diff --git a/src/test/resources/regression/verification/purescala/invalid/Array1.scala b/src/test/resources/regression/verification/purescala/invalid/Array1.scala
index 740f38a96314fb9babbff944fe7a35f0210b50ea..cf4abc13248dd1efd217d30e1e83d374ef69a8f4 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Array1.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Array1.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Array4 {
 
diff --git a/src/test/resources/regression/verification/purescala/invalid/Array2.scala b/src/test/resources/regression/verification/purescala/invalid/Array2.scala
index 4cc49498f6b6510edc7ce23b8511eabad243774d..a01cd23a7ed8444ff29db76f878a4ed4e3443de4 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Array2.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Array2.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Array4 {
 
diff --git a/src/test/resources/regression/verification/purescala/invalid/Array3.scala b/src/test/resources/regression/verification/purescala/invalid/Array3.scala
index 0d744e8078156510486cf12486557cfea6b23d27..997ce966aef72c9202561b180109e741f2b83e77 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Array3.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Array3.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Test {
 
diff --git a/src/test/resources/regression/verification/purescala/invalid/Array4.scala b/src/test/resources/regression/verification/purescala/invalid/Array4.scala
index cb0c2409c26ca61e394bc1a0bf00a382097a013f..280ce5bf103ab4e9aa72e5819bfd58b997f6045d 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Array4.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Array4.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Array4 {
 
diff --git a/src/test/resources/regression/verification/purescala/invalid/Choose1.scala b/src/test/resources/regression/verification/purescala/invalid/Choose1.scala
index 663c15d4e87c729a52311dd064cc939ac976030a..6779cc5f044e5f5ee4c0e2c24f0c24fff7b95e70 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Choose1.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Choose1.scala
@@ -1,7 +1,7 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Choose1 {
     sealed abstract class List
diff --git a/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala b/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala
index f7b0ea17a96c1b4771bfcbf0e7f5428e9d85fc95..1f95b041fbe205f90f3dc7b70f2516cab2ae704d 100644
--- a/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object FiniteSorting {
 
diff --git a/src/test/resources/regression/verification/purescala/invalid/Generics.scala b/src/test/resources/regression/verification/purescala/invalid/Generics.scala
index 0afd38848fe180d3112c1730ac0a2f81baa155d1..258759c21fbf0b098eae5346fef58bc6f2986206 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Generics.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Generics.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Generics1 {
   abstract class List[T]
diff --git a/src/test/resources/regression/verification/purescala/invalid/Generics2.scala b/src/test/resources/regression/verification/purescala/invalid/Generics2.scala
index ae8f9f458858b23687167372a2ef65cabcc5b43f..bc204fb0f6d4019ee4b3177baa9b13ad2382c139 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Generics2.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Generics2.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Generics1 {
   abstract class List[T]
diff --git a/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala b/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
index d8c2d029e818ace24d9be936dd6e64396f938915..e0750c49be2440338b4cc022522d76109ea88fb0 100644
--- a/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
@@ -1,8 +1,8 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object InsertionSort {
   sealed abstract class List
diff --git a/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala b/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
index edf0e170e145458c3d606232be1242e096fa641f..9a35c4a4b84983f7e2e59610de92601cc8ad726e 100644
--- a/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
@@ -1,8 +1,8 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object ListOperations {
     sealed abstract class List
diff --git a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
index ec14ad7bb900e9cfa63212832d4de4b18207c926..994ce5ef31b9ff0c1fdb7be01f5b157c530de20c 100644
--- a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
@@ -1,8 +1,8 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object PropositionalLogic { 
 
diff --git a/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala b/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
index f5478d73479e17f58b0a708420440ae4b03c4b3f..48ab21763a92063f8e0c612014ac9f01a9889354 100644
--- a/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
@@ -1,8 +1,8 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object RedBlackTree { 
   sealed abstract class Color
diff --git a/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala b/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
index 1b264b2e5ac7be4d0fba2b75695b2956665a3ece..054d393e8b3c4f1e8fa32ab542f4e4811d1e3a53 100644
--- a/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
+++ b/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
@@ -1,8 +1,8 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object AmortizedQueue {
   sealed abstract class List
diff --git a/src/test/resources/regression/verification/purescala/valid/ArrayLiterals.scala b/src/test/resources/regression/verification/purescala/valid/ArrayLiterals.scala
index 2ce0669e612100ca51bd542808a5a28517f11054..08c2e5a87f034057a7c1ba60864b9ba7749728fa 100644
--- a/src/test/resources/regression/verification/purescala/valid/ArrayLiterals.scala
+++ b/src/test/resources/regression/verification/purescala/valid/ArrayLiterals.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 object Numerals {
   def foo(): Int = {
     val b : Array[Int] = Array[Int](1,2,3)
diff --git a/src/test/resources/regression/verification/purescala/valid/ArrayUpdated.scala b/src/test/resources/regression/verification/purescala/valid/ArrayUpdated.scala
index 67d4af25d8950ffbd23980308b5d516192582590..78c12a6313d89e8ac5578c9ac8264e06f3cccb83 100644
--- a/src/test/resources/regression/verification/purescala/valid/ArrayUpdated.scala
+++ b/src/test/resources/regression/verification/purescala/valid/ArrayUpdated.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Test {
 
diff --git a/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala b/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
index dd7516b20f9f11435bf047d7d58b4c4f9d0e692e..7f2a3451559363f62ca2fd6a40f5ae0c7d1054eb 100644
--- a/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
+++ b/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
@@ -1,8 +1,8 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object AssociativeList { 
   sealed abstract class KeyValuePairAbs
diff --git a/src/test/resources/regression/verification/purescala/valid/BestRealTypes.scala b/src/test/resources/regression/verification/purescala/valid/BestRealTypes.scala
index 449bba2f192833807566fe54784110aa71548868..1a84e41f18ae9bc771d9e4965d33c00efcd4004b 100644
--- a/src/test/resources/regression/verification/purescala/valid/BestRealTypes.scala
+++ b/src/test/resources/regression/verification/purescala/valid/BestRealTypes.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 /** This benchmarks tests some potential issues with the legacy "bestRealType" function, which was original introduced to work around
  * Scala's well-too-precise-for-Leon type inference. */
diff --git a/src/test/resources/regression/verification/purescala/valid/Choose1.scala b/src/test/resources/regression/verification/purescala/valid/Choose1.scala
index ebcf96f1799a578d3784240d0a9ecdfe6851f9e6..dc16d2314c8c641bca556f1ad2482a54ca4377c6 100644
--- a/src/test/resources/regression/verification/purescala/valid/Choose1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Choose1.scala
@@ -1,7 +1,7 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Choose1 {
     sealed abstract class List
diff --git a/src/test/resources/regression/verification/purescala/valid/FiniteSort.scala b/src/test/resources/regression/verification/purescala/valid/FiniteSort.scala
index 01f2caeeda16345e42173547a42c23f72483ffd7..1f8cddb508be5304ba4056874f3559b2aa834a45 100644
--- a/src/test/resources/regression/verification/purescala/valid/FiniteSort.scala
+++ b/src/test/resources/regression/verification/purescala/valid/FiniteSort.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object FiniteSorting {
 
diff --git a/src/test/resources/regression/verification/purescala/valid/Generics.scala b/src/test/resources/regression/verification/purescala/valid/Generics.scala
index b930b5f2c9932d06347bd40d89004f8ef3f83c7b..75c8d755f9b8c76eae7143740d2d0a20e26792f3 100644
--- a/src/test/resources/regression/verification/purescala/valid/Generics.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Generics.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Generics1 {
   abstract class List[T]
diff --git a/src/test/resources/regression/verification/purescala/valid/Generics2.scala b/src/test/resources/regression/verification/purescala/valid/Generics2.scala
index f1078cca5a0ef04d4fa76ecfaab6f161acaaa92f..fba486c8c98061fe188d8d7f1db6c5f132aed8d2 100644
--- a/src/test/resources/regression/verification/purescala/valid/Generics2.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Generics2.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Generics1 {
   abstract class List[T]
diff --git a/src/test/resources/regression/verification/purescala/valid/Heap.scala b/src/test/resources/regression/verification/purescala/valid/Heap.scala
index 530354f30cf979e0a43525b08de7f2d4242577e0..af01b1cffb821c575e86f38cfca90b9701dd9bf2 100644
--- a/src/test/resources/regression/verification/purescala/valid/Heap.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Heap.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Heaps {
   /*~~~~~~~~~~~~~~~~~~~~~~~*/
diff --git a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
index 630518aa3b01d538394353d7258902f94053ec99..5540fd2d847b0c145b45cd8f243a214c13694d72 100644
--- a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
@@ -1,8 +1,8 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object InsertionSort {
   sealed abstract class List
diff --git a/src/test/resources/regression/verification/purescala/valid/IsolatedAbstract.scala b/src/test/resources/regression/verification/purescala/valid/IsolatedAbstract.scala
index 055e86713307cff14469cb5320166a5104916e77..c1b30838b56823732c27e20f3411d4077d6f6141 100644
--- a/src/test/resources/regression/verification/purescala/valid/IsolatedAbstract.scala
+++ b/src/test/resources/regression/verification/purescala/valid/IsolatedAbstract.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object LoneAbstract {
 
diff --git a/src/test/resources/regression/verification/purescala/valid/ListOperations.scala b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
index 178d9a523d71484b0e667e8c66f4ba06ab1152b2..689aee57d79b577963e07734c128f756b6c22414 100644
--- a/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
+++ b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
@@ -1,8 +1,8 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object ListOperations {
     sealed abstract class List
diff --git a/src/test/resources/regression/verification/purescala/valid/MergeSort.scala b/src/test/resources/regression/verification/purescala/valid/MergeSort.scala
index 32c0c2ddb72faf1e9793d5c430d608eba0736de9..61d4d6433e562856fa08a4c6a488f6a2aff9ccd4 100644
--- a/src/test/resources/regression/verification/purescala/valid/MergeSort.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MergeSort.scala
@@ -1,7 +1,7 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object MergeSort {
   // Data types
diff --git a/src/test/resources/regression/verification/purescala/valid/MyMap.scala b/src/test/resources/regression/verification/purescala/valid/MyMap.scala
index 7b75661126d4452b26387a009ba71236990ec378..652d98c2f46debf754928678724716284ea7fc68 100644
--- a/src/test/resources/regression/verification/purescala/valid/MyMap.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MyMap.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object MyMap {
 
diff --git a/src/test/resources/regression/verification/purescala/valid/MySet.scala b/src/test/resources/regression/verification/purescala/valid/MySet.scala
index 8f1b482ffbf28c0076f5265c016773140e73dbf8..1714ecb8b01287d6d02ae3db68e90eda44cee1a0 100644
--- a/src/test/resources/regression/verification/purescala/valid/MySet.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MySet.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object MySet {
 
diff --git a/src/test/resources/regression/verification/purescala/valid/Nat.scala b/src/test/resources/regression/verification/purescala/valid/Nat.scala
index c78693b66731adfc95a17b4e299d2f7f09c307d1..f09360c572fff09060651318e0405533b52c961f 100644
--- a/src/test/resources/regression/verification/purescala/valid/Nat.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Nat.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Nat {
   sealed abstract class Nat
diff --git a/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
index 25b842f6c7ea194bfe8201d43384ca2690010917..2f1c48e3e69bdf30cfe43197b03b0f2abbfa4029 100644
--- a/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
@@ -1,8 +1,8 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object PropositionalLogic { 
 
diff --git a/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala b/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
index 3cbe4800d94cf092de210c0a0320fd88f2c51dc3..4d052da77b62388fc0e5cb11933356caea022225 100644
--- a/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
+++ b/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
@@ -1,8 +1,8 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object RedBlackTree { 
   sealed abstract class Color
diff --git a/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala b/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
index 44d5550c1a0286c63c0f7a5f38f597f985285166..27e2f4ba8836522cb8f34f4e9b6ffcdb5cbaf680 100644
--- a/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
+++ b/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
@@ -1,8 +1,8 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object SearchLinkedList {
   sealed abstract class List
diff --git a/src/test/resources/regression/verification/purescala/valid/Subtyping2.scala b/src/test/resources/regression/verification/purescala/valid/Subtyping2.scala
index fc7f2e4cae820fe949687cc23448d0aec92edb8a..7b6a8aa16dd2d2543804ad7936917953ebb019dd 100644
--- a/src/test/resources/regression/verification/purescala/valid/Subtyping2.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Subtyping2.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Test {
 
diff --git a/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala b/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala
index 555f80f0a7bf9814a65a3c6ce3f5d1f1433cfaea..90f2efc3299692f22a9c8e529323be9090d23fbf 100644
--- a/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala
+++ b/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala
@@ -1,7 +1,7 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object SumAndMax {
   sealed abstract class List
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array3.scala b/src/test/resources/regression/verification/xlang/invalid/Array3.scala
index deb28f736f33fdfb44e540aae7971aaa5b181566..eaf5470354ef163527ff2754f8c3ee2881347b7c 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array3.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Array3.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Array3 {
 
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array4.scala b/src/test/resources/regression/verification/xlang/invalid/Array4.scala
index 740f38a96314fb9babbff944fe7a35f0210b50ea..cf4abc13248dd1efd217d30e1e83d374ef69a8f4 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array4.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Array4.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Array4 {
 
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array5.scala b/src/test/resources/regression/verification/xlang/invalid/Array5.scala
index 4cc49498f6b6510edc7ce23b8511eabad243774d..a01cd23a7ed8444ff29db76f878a4ed4e3443de4 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array5.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Array5.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Array4 {
 
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array6.scala b/src/test/resources/regression/verification/xlang/invalid/Array6.scala
index 41b35fd03318f89cd7419f08a101ed74ef7f0922..13d8ea191098168158b6739be86ff61f930cf013 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array6.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Array6.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Array4 {
 
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
index 48cc02793a635154563ba1546b2623f14b4f1ed2..9b237296964284fd774e441231e3bc9fcf89f312 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Epsilon1 {
 
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
index f5f0d6be05a34af38f2d558489b34dc8b8b9ab71..b23ab8e670cdde7385b03fd782ce315d59c03804 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Epsilon1 {
 
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala
index d76d9a7f75e91054491dfcb087c4d13424876ed3..095c8c3f23651ee945395c8bb58a80378514f82b 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Epsilon3 {
 
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
index 92cd1d75843217a1c026c0ca191ccf588fcb38ad..fc3fd5938e4c139f7ae438e1f4d8be206697cae3 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Epsilon4 {
 
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala
index cd387c1694c5d1f830f2889a99b4245312955db7..b51def1ee73a9584b7f9f1d3c99f433f488d5c4d 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Epsilon5 {
 
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala
index 0973387862ef0234d9b1800fbe0613dc0ec78bc2..edcc9e2fa501435d9c439e6091f8c839ad5575cc 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Epsilon6 {
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Arithmetic.scala b/src/test/resources/regression/verification/xlang/valid/Arithmetic.scala
index 31a759ad8e8223977dc445539f619ce1ab6aed14..c6be0e96bd18f92b10011803f16edc2982e8cf2f 100644
--- a/src/test/resources/regression/verification/xlang/valid/Arithmetic.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Arithmetic.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Arithmetic {
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Array3.scala b/src/test/resources/regression/verification/xlang/valid/Array3.scala
index cf41ef4f242da814b5df19b3c11828e566c1f7c1..92a13d5907eca6de4e2cfe0deaa773912ee5fa7c 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array3.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array3.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Array3 {
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Array4.scala b/src/test/resources/regression/verification/xlang/valid/Array4.scala
index 9337f21f18847798eca59efe1a90e60b261d88dd..196f7b1dfc5d0ac28bb7d6cc053988807d3ccac9 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array4.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array4.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Array4 {
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Array5.scala b/src/test/resources/regression/verification/xlang/valid/Array5.scala
index a298a74292e293c692dd7b9b9ba8d018f78f8595..9160dbff0fa301d74e8bfe590b97ba1ddcadd8d1 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array5.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array5.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Array5 {
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Array6.scala b/src/test/resources/regression/verification/xlang/valid/Array6.scala
index fb1dc5eee772cfacdd26a8ef4975df9e38f64b79..43551bf7e27fa82071329ebba51ae373ef9214bc 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array6.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array6.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Array6 {
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Array7.scala b/src/test/resources/regression/verification/xlang/valid/Array7.scala
index 806fe5e327464d3295db2b5edcb96c2dd66f6431..c83f7c00c5f79667f80a0429eafe97152f51709c 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array7.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array7.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Array7 {
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Choose1.scala b/src/test/resources/regression/verification/xlang/valid/Choose1.scala
index 1461f0d0cd898722d01d9caf484088f3bccc9329..b44c0856c63602f2a279f253e50bf1c5ce8d1443 100644
--- a/src/test/resources/regression/verification/xlang/valid/Choose1.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Choose1.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Test {
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala
index 1d8402600d5d6d98cbe8503178f371697cd00f9c..32ca5ccf02edb357960a2395ca933fb5069b760f 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Epsilon1 {
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
index 794c4f0708052adef0ffed9e34f1b5f0561dad15..981c463d8db9adc09b4b078bd03acf4c4a08c27c 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Epsilon1 {
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala
index 9d114be164bc1a3c519d212eb856b22852deaf94..d80401c20c7e6b88e3cb295b09ae0b9b3fdc3a9b 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Epsilon3 {
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
index cbe5498b4e89dc90c80bd7e716e0cd32abe621c6..e20b22508fcd2678684948f6c957debb75abdc88 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Epsilon4 {
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala
index a020beee84a436537c592bb0c88818444bea380a..08dd68e0a9fbfb65f44c86690c11514a7e7f1659 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Epsilon5 {
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested8.scala b/src/test/resources/regression/verification/xlang/valid/Nested8.scala
index 6933d1cc2e4df69261205f5a8cabe9603126d6af..2580c215ff2350d1352d9cdb5ac5864484a80399 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested8.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested8.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
-import leon.Utils._
+import leon.lang._
 
 object Nested8 {
 
diff --git a/src/test/scala/leon/test/condabd/EvaluationTest.scala b/src/test/scala/leon/test/condabd/EvaluationTest.scala
index 3ba486435db748621db21da30f630c2d20160f76..b8acc3cb8ea93d28f67736e9b893b7c784a49121 100644
--- a/src/test/scala/leon/test/condabd/EvaluationTest.scala
+++ b/src/test/scala/leon/test/condabd/EvaluationTest.scala
@@ -27,7 +27,7 @@ class EvaluationTest extends FunSuite {
   import Scaffold._
 
   val mergeSortWithTwoExamples = """
-				import leon.Utils._
+				import leon.lang._
 				
 				object MergeSort {
 				  sealed abstract class List
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 44dc2e7898b3914f0e03584cd5e26998ad8c21e8..f6db22df88d4877d615600ad9e0754b3fe1447e1 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -430,7 +430,7 @@ class EvaluatorsTests extends LeonTestSuite {
 
   test("Executing Chooses") {
     val p = """|object Program {
-               |  import leon.Utils._
+               |  import leon.lang._
                |
                |  def c(i : Int) : Int = choose { (j : Int) => j > i && j < i + 2 }
                |}
@@ -448,7 +448,7 @@ class EvaluatorsTests extends LeonTestSuite {
     import codegen._
 
     val p = """|object Program {
-               |  import leon.Utils._
+               |  import leon.lang._
                |
                |  def c(i : Int) : Int = c(i-1)
                |}
@@ -464,7 +464,7 @@ class EvaluatorsTests extends LeonTestSuite {
     import codegen._
 
     val p = """|object Program {
-               |  import leon.Utils._
+               |  import leon.lang._
                |
                |  def c(i : Int) : Int = {
                |    require(i > 0);
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index eaf38ca14dbe12759d4115aafbf3cd8479a4cc03..4ac4e47bf4a2f12fc842a082418c2858e836a98a 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -126,8 +126,8 @@ class SynthesisSuite extends LeonTestSuite {
   forProgram("Cegis 1")(
     """
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Injection {
   sealed abstract class List
@@ -151,8 +151,8 @@ object Injection {
   forProgram("Cegis 2")(
     """
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Injection {
   sealed abstract class List
@@ -188,7 +188,7 @@ object Injection {
 
 
   synthesize("Lists")("""
-import leon.Utils._
+import leon.lang._
 
 object SortedList {
   sealed abstract class List
@@ -253,7 +253,7 @@ object SortedList {
   }
 
   synthesize("Church")("""
-import leon.Utils._
+import leon.lang._
 object ChurchNumerals {
   sealed abstract class Num
   case object Z extends Num
@@ -286,7 +286,7 @@ object ChurchNumerals {
   }
 
   synthesize("Church")("""
-import leon.Utils._
+import leon.lang._
 object ChurchNumerals {
   sealed abstract class Num
   case object Z extends Num
diff --git a/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala b/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a0d91cdf9d105177dab89a70a1a0d6c2e84507a8
--- /dev/null
+++ b/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
@@ -0,0 +1,23 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+package test
+package verification
+
+import java.io.File
+
+class LibraryVerificationRegression extends LeonTestSuite {
+  test("Verify the library") {
+      val pipeline = leon.frontends.scalac.ExtractionPhase andThen
+                     leon.purescala.MethodLifting andThen
+                     leon.utils.SubtypingPhase andThen
+                     leon.purescala.CompleteAbstractDefinitions andThen
+                     leon.verification.AnalysisPhase
+
+      val ctx = Main.processOptions(Seq("--library", "--functions=_")).copy(reporter = new TestSilentReporter())
+
+      val report = pipeline.run(ctx)(Nil)
+
+      assert(report.totalConditions === report.totalValid, "Only "+report.totalValid+" valid out of "+report.totalConditions);
+  }
+}
diff --git a/testcases/Addresses.scala b/testcases/Addresses.scala
index 0eff2a4c1f472ba4dd03a0b2ae3e496ad577616d..3e5d730e5ff12a1887987894287c5b93acd81762 100644
--- a/testcases/Addresses.scala
+++ b/testcases/Addresses.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   // list of integers
diff --git a/testcases/Errors.scala b/testcases/Errors.scala
index b6d7dc74e5ba82ebac0863fd411e4b00ef475bc7..0a975695de7c42fd944ef9c8184e305714b17ca4 100644
--- a/testcases/Errors.scala
+++ b/testcases/Errors.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Errors {
   def a(a: Int): Int = error[Int]("This is an error")
diff --git a/testcases/FiniteSort.scala b/testcases/FiniteSort.scala
index 6f1431ced3c0e90a25d0b5469a17f0b5c1ae348b..97eb2f2fa618a6cf3bcf318c88c78f2f3400ff36 100644
--- a/testcases/FiniteSort.scala
+++ b/testcases/FiniteSort.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object FiniteSorting {
 
diff --git a/testcases/Interpret.scala b/testcases/Interpret.scala
index 795eb4ae31a343e39d5866cbdd829711348311e9..40dcab73cdb00b0b65dd960ca3e2427e4fa503c7 100644
--- a/testcases/Interpret.scala
+++ b/testcases/Interpret.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Interpret {
   abstract class BoolTree 
diff --git a/testcases/MutuallyRecursive.scala b/testcases/MutuallyRecursive.scala
index 186afcffeec667fefdcac9c02d40babca6fa1f86..b394827735a335a6f69e0a5c04127c0c1ee4517f 100644
--- a/testcases/MutuallyRecursive.scala
+++ b/testcases/MutuallyRecursive.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object MutuallyRecursive {
     def f(n : Int) : Int = {
diff --git a/testcases/Naturals.scala b/testcases/Naturals.scala
index be821c963f3d14ddd9c8f21c84088486e7df5de5..1f9131c9cab2d50a2b26f1a055f4c1b4bf28d75d 100644
--- a/testcases/Naturals.scala
+++ b/testcases/Naturals.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Naturals {
     sealed abstract class Nat
diff --git a/testcases/PropositionalLogic.scala b/testcases/PropositionalLogic.scala
index 6d2daeb2e8e3635562d7154d39589a645f278e93..ececf099804ff93410df1753a27963a6aa8bbfa8 100644
--- a/testcases/PropositionalLogic.scala
+++ b/testcases/PropositionalLogic.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object PropositionalLogic {
 
diff --git a/testcases/SimpInterpret.scala b/testcases/SimpInterpret.scala
index a3ef9ee385e43966c35b90fbca73b9fbbfd5a762..fab5035897d86b4b587715cb4d7ef3459c1fed2f 100644
--- a/testcases/SimpInterpret.scala
+++ b/testcases/SimpInterpret.scala
@@ -1,6 +1,6 @@
 //import scala.collection.immutable.Set
-//import leon.Annotations._
-import leon.Utils._
+//import leon.annotation._
+import leon.lang._
 
 object Interpret {
   abstract class BoolTree
diff --git a/testcases/TwoSizeFunctions.scala b/testcases/TwoSizeFunctions.scala
index e88239783b7ddfc14e021408d7f058b1edab4c3d..faafa7d181b21054aa794cda74ca6c0188d9a2a3 100644
--- a/testcases/TwoSizeFunctions.scala
+++ b/testcases/TwoSizeFunctions.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object TwoSizeFunctions {
   sealed abstract class List
diff --git a/testcases/case-studies/Compiler.scala b/testcases/case-studies/Compiler.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6062dff352abc8656fa861a848126b24b13af01a
--- /dev/null
+++ b/testcases/case-studies/Compiler.scala
@@ -0,0 +1,147 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Tokens {
+  abstract class Token
+  case object TPlus extends Token
+  case object TTimes extends Token
+  case object TLT extends Token
+  case object TIf extends Token
+  case object TElse extends Token
+  case object TLeftBrace extends Token
+  case object TRightBrace extends Token
+  case object TLeftPar extends Token
+  case object TRightPar extends Token
+  case class TInt(v: Int) extends Token
+  case class TId(name: Int) extends Token // All variables are : Int
+}
+
+object Trees {
+  abstract class Expr
+  case class Times(lhs: Expr, rhs: Expr) extends Expr
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr
+  case class Var(id: Int) extends Expr
+  case class IntLiteral(v: Int) extends Expr
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+  case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+}
+
+object Types {
+  abstract class Type
+  case object IntType extends Type
+  case object BoolType extends Type
+}
+
+object Parser {
+  import Tokens._
+  import Trees._
+
+  def parsePhrase(ts: List[Token]): Option[Expr] = {
+    parseGoal(ts) match {
+      case Some((res, Nil())) => Some(res)
+      case _ => None()
+    }
+  }
+
+  def parseGoal(ts: List[Token]): Option[(Expr, List[Token])] = {
+    parseLT(ts)
+  }
+
+  def parseLT(ts: List[Token]): Option[(Expr, List[Token])] = {
+    parsePlus(ts) match {
+      case Some((lhs, Cons(TLT, r))) =>
+        parsePlus(r) match {
+          case Some((rhs, ts2)) => Some((LessThan(lhs, rhs), ts2))
+          case None() => None()
+        }
+      case r => r
+    }
+  }
+
+  def parsePlus(ts: List[Token]): Option[(Expr, List[Token])] = {
+    parseTimes(ts) match {
+      case Some((lhs, Cons(TPlus, r))) =>
+        parsePlus(r) match {
+          case Some((rhs, ts2)) => Some((Plus(lhs, rhs), ts2))
+          case None() => None()
+        }
+      case r => r
+    }
+  }
+
+  def parseTimes(ts: List[Token]): Option[(Expr, List[Token])] = {
+    parseLits(ts) match {
+      case Some((lhs, Cons(t, r))) if (t == TTimes) =>
+        parseTimes(r) match {
+          case Some((rhs, ts2)) => Some((Plus(lhs, rhs), ts2))
+          case None() => None()
+        }
+      case r => r
+    }
+  }
+
+  def parseLits(ts: List[Token]): Option[(Expr, List[Token])] = ts match {
+    case Cons(TInt(v), r) => Some((IntLiteral(v), r))
+    case Cons(TId(v), r) => Some((Var(v), r))
+    case Cons(TLeftPar, r) =>
+      parseGoal(r) match {
+        case Some((e, Cons(TRightPar, ts2))) => Some((e, ts2))
+        case _ => None()
+      }
+    case Cons(TIf, Cons(TLeftPar, r)) =>
+      parseGoal(r) match {
+        case Some((c, Cons(TRightPar, Cons(TLeftBrace, ts2)))) =>
+          // Then
+          parseGoal(ts2) match {
+            case Some((th, Cons(TRightBrace, Cons(TElse, Cons(TLeftBrace, ts3))))) =>
+              // Else
+              parseGoal(ts3) match {
+                case Some((el, Cons(TRightBrace, ts4))) =>
+                  Some((Ite(c, th, el), ts4))
+                case _ => None()
+              }
+            case _ => None()
+          }
+        case _ => None()
+      }
+    case _ => None()
+  }
+}
+
+object Compiler {
+  import Tokens._
+  import Trees._
+  import Types._
+  import Parser._
+
+  @proxy
+  def tokenize(s: String): List[Token] = {
+    Cons(TInt(12), Cons(TLT, Cons(TInt(32), Nil())))
+  }
+
+  def parse(ts: List[Token]): Option[Expr] = {
+    parsePhrase(ts)
+  } ensuring { res => res match {
+    case Some(res) => typeChecks(res, BoolType)
+    case None() => true
+  }}
+
+  def typeChecks(e: Expr, t: Type): Boolean = e match {
+    case Times(l, r) => (t == IntType) && typeChecks(l, IntType) && typeChecks(r, IntType)
+    case Plus(l, r) => (t == IntType) && typeChecks(l, IntType) && typeChecks(r, IntType)
+    case LessThan(l, r) => (t == BoolType) && typeChecks(l, IntType) && typeChecks(r, IntType)
+    case Ite(c, th, el) => typeChecks(c, BoolType) && typeChecks(th, t) && typeChecks(el, t)
+    case IntLiteral(_) => t == IntType
+    case Var(_) => t == IntType
+  }
+
+  @proxy
+  def run(s: String) = {
+    val ts = tokenize(s)
+    val e = parse(ts)
+    e
+  }
+
+}
diff --git a/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala b/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala
index 6b9a73a9c1290c626d03f8a8cad3ea8f49bc8598..ccd1d6ad3db6fc7c3dd6e682a32ab97939d39fa9 100644
--- a/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala
+++ b/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   case class Info(
diff --git a/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala b/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala
index c22541f8c9649c1e5485a41d5ebe4ce093d68bf2..f04399105adbdd36e994ccfdabadeb24ffdf3da6 100644
--- a/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala
+++ b/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   
diff --git a/testcases/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala b/testcases/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala
index 0d6d8c0677806c687186184aa929e80032b869a8..a9154bc7694564291a819dfec6bc0bc641bbffdf 100644
--- a/testcases/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala
+++ b/testcases/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   case class Info(
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueue.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
index 941bbadf944b61b78878c2acb0bdb0576f038c26..b966885e6e3505a78bd5501a1cf96f30a8a38b88 100644
--- a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
+++ b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object BatchedQueue {
   sealed abstract class List
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueCheckf.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueCheckf.scala
index 4faa50286c879d90d3e9fe12db58856459ee8993..52e582ffb2c850f60dac404f375da2aa486f637f 100644
--- a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueCheckf.scala
+++ b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueCheckf.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object BatchedQueue {
   sealed abstract class List
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala
index cc5f1f73a99da0f3f64b878e4f569b68ec430e14..467fc66dfb4a8e99d7043f9b3ffeef519d1712df 100644
--- a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala
+++ b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object BatchedQueue {
   sealed abstract class List
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnoc.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnoc.scala
index 6541b33b5dbce7b126d0eeac8b46858d286fa59d..26e70e64995bdf559add3538f4cd23355d1303f6 100644
--- a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnoc.scala
+++ b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnoc.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object BatchedQueue {
   sealed abstract class List
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnocWeird.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnocWeird.scala
index 0b9eccfc3d71060b7b85cf204f3f34b742ce2758..f74b8d8eaffa429632f19f5e66ab01f22092dd4e 100644
--- a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnocWeird.scala
+++ b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnocWeird.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object BatchedQueue {
   sealed abstract class List
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueTail.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueTail.scala
index d35737dab64b76701d1904aae49dd4bfdb188a27..31b67f6a850f0f75e2a79af82ec855605d416337 100644
--- a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueTail.scala
+++ b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueTail.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object BatchedQueue {
   sealed abstract class List
diff --git a/testcases/condabd/benchmarks/BinarySearch.scala b/testcases/condabd/benchmarks/BinarySearch.scala
index d35de5266876b9208d98a8fdb80c9f9976678e8c..b8883a3bbebb6283136dcd777d3c333678c8131c 100644
--- a/testcases/condabd/benchmarks/BinarySearch.scala
+++ b/testcases/condabd/benchmarks/BinarySearch.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object BinarySearch {
 
diff --git a/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala b/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala
index e454407409fa0b47f80914ec16b0770a6f7dcdcb..2e3f168a37939fb67a1203c35a8cc0b4ea3fd4c7 100644
--- a/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala
+++ b/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala
@@ -1,7 +1,7 @@
 import scala.collection.immutable.Set
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinarySearchTree {
   sealed abstract class Tree
diff --git a/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeMember.scala b/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeMember.scala
index 416c6ef577cfb267df1d66c1a8a6f8d0f4ba141a..5ca4fb8c3abe56168ec3dd8ff7fa1da57c90af89 100644
--- a/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeMember.scala
+++ b/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeMember.scala
@@ -1,7 +1,7 @@
 import scala.collection.immutable.Set
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinarySearchTree {
   sealed abstract class Tree
diff --git a/testcases/condabd/benchmarks/InsertionSort/InsertionSortInsert.scala b/testcases/condabd/benchmarks/InsertionSort/InsertionSortInsert.scala
index ac832856ed117c3a7e68eabae2f5ab87b70ef3bb..7afa8f2b8ba2b90d6fc6e3da518f621e145a4425 100644
--- a/testcases/condabd/benchmarks/InsertionSort/InsertionSortInsert.scala
+++ b/testcases/condabd/benchmarks/InsertionSort/InsertionSortInsert.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object InsertionSort {
   sealed abstract class List
diff --git a/testcases/condabd/benchmarks/InsertionSort/InsertionSortSort.scala b/testcases/condabd/benchmarks/InsertionSort/InsertionSortSort.scala
index 7daae970332d41e0b971b32c8cc70b57aa9b69b5..823011be40fa82df76f9da08580aa46455948c25 100644
--- a/testcases/condabd/benchmarks/InsertionSort/InsertionSortSort.scala
+++ b/testcases/condabd/benchmarks/InsertionSort/InsertionSortSort.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object InsertionSort {
   sealed abstract class List
diff --git a/testcases/condabd/benchmarks/List/ListConcat.scala b/testcases/condabd/benchmarks/List/ListConcat.scala
index 96a2d909ac25e11596ee86c63d884df08d5be7e3..271082886e28c46bb98d6aa1d7e77e4036a9f39c 100644
--- a/testcases/condabd/benchmarks/List/ListConcat.scala
+++ b/testcases/condabd/benchmarks/List/ListConcat.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object ListOperations {
     sealed abstract class List
diff --git a/testcases/condabd/benchmarks/List/ListSearch.scala b/testcases/condabd/benchmarks/List/ListSearch.scala
index c70269a41016e45ce3edb968d07730a59aeb7c28..240a5f0091356f4bcdb8c78c972c566f71e60c7c 100644
--- a/testcases/condabd/benchmarks/List/ListSearch.scala
+++ b/testcases/condabd/benchmarks/List/ListSearch.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object ListOperations {
     sealed abstract class List
diff --git a/testcases/condabd/benchmarks/MergeSort/MergeSortMerge.scala b/testcases/condabd/benchmarks/MergeSort/MergeSortMerge.scala
index 8b25821929c319358ea948139245904b6f9e2a3b..c43a3c598f6ab5b44898acd0bdff8cf1d34fdf24 100644
--- a/testcases/condabd/benchmarks/MergeSort/MergeSortMerge.scala
+++ b/testcases/condabd/benchmarks/MergeSort/MergeSortMerge.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object MergeSort {
   sealed abstract class List
diff --git a/testcases/condabd/benchmarks/MergeSort/MergeSortSort.scala b/testcases/condabd/benchmarks/MergeSort/MergeSortSort.scala
index 987c538c4ab36dc9b378f03fc24592210bcbd62b..e96b37543e7636a2870d25cbf967e312e41f5cd5 100644
--- a/testcases/condabd/benchmarks/MergeSort/MergeSortSort.scala
+++ b/testcases/condabd/benchmarks/MergeSort/MergeSortSort.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object MergeSort {
   sealed abstract class List
diff --git a/testcases/condabd/benchmarks/MergeSort/MergeSortSortWithVal.scala b/testcases/condabd/benchmarks/MergeSort/MergeSortSortWithVal.scala
index 2cccf5c98753a362235d4fb423e2621e84de534a..8df35ea8f7c2377cb1d883416bbfcc79627c7409 100644
--- a/testcases/condabd/benchmarks/MergeSort/MergeSortSortWithVal.scala
+++ b/testcases/condabd/benchmarks/MergeSort/MergeSortSortWithVal.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object MergeSort {
   sealed abstract class List
diff --git a/testcases/condabd/benchmarks/RedBlackTree/RedBlackTree.scala b/testcases/condabd/benchmarks/RedBlackTree/RedBlackTree.scala
index f72664258ebb5b329d61d0eb17c82c581b370d01..e9eb12df8170fd6173c752806f1ecb096de6fe29 100644
--- a/testcases/condabd/benchmarks/RedBlackTree/RedBlackTree.scala
+++ b/testcases/condabd/benchmarks/RedBlackTree/RedBlackTree.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object RedBlackTree { 
   sealed abstract class Color
diff --git a/testcases/condabd/benchmarks/RedBlackTree/RedBlackTreeInsert.scala b/testcases/condabd/benchmarks/RedBlackTree/RedBlackTreeInsert.scala
index e6413ffaf8278fdacb43372eb615ced566e60022..b32b6165ac0d8e7debdf74848b4c2c01f3b67ae5 100644
--- a/testcases/condabd/benchmarks/RedBlackTree/RedBlackTreeInsert.scala
+++ b/testcases/condabd/benchmarks/RedBlackTree/RedBlackTreeInsert.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object RedBlackTree {
   sealed abstract class Color
@@ -74,4 +74,4 @@ object RedBlackTree {
     }
   }
 
-}
\ No newline at end of file
+}
diff --git a/testcases/condabd/test/insynth/Addresses.scala b/testcases/condabd/test/insynth/Addresses.scala
index 52260559cecdabef594aa208096cd9a05b93dbe5..8a958cca412c0ea1792187624936e7630e3fc1b3 100644
--- a/testcases/condabd/test/insynth/Addresses.scala
+++ b/testcases/condabd/test/insynth/Addresses.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   
diff --git a/testcases/condabd/test/insynth/AddressesWithAddition.scala b/testcases/condabd/test/insynth/AddressesWithAddition.scala
index 04a73ae087b993d61fc9e43b73c64f7ee2247bc9..c5df950772581d4d7f45007d45490fc398daf0f6 100644
--- a/testcases/condabd/test/insynth/AddressesWithAddition.scala
+++ b/testcases/condabd/test/insynth/AddressesWithAddition.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object AddressesWithAddition {
   
diff --git a/testcases/condabd/test/insynth/ListConcat.scala b/testcases/condabd/test/insynth/ListConcat.scala
index 20972e8af864cc1a618fe5d74278ce4298c01c35..3091e9e472d094dcab1a5482ef14d4bba11144fb 100644
--- a/testcases/condabd/test/insynth/ListConcat.scala
+++ b/testcases/condabd/test/insynth/ListConcat.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object ListOperations {
 
diff --git a/testcases/condabd/test/lesynth/Addresses.scala b/testcases/condabd/test/lesynth/Addresses.scala
index 52260559cecdabef594aa208096cd9a05b93dbe5..8a958cca412c0ea1792187624936e7630e3fc1b3 100644
--- a/testcases/condabd/test/lesynth/Addresses.scala
+++ b/testcases/condabd/test/lesynth/Addresses.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   
diff --git a/testcases/condabd/test/lesynth/AddressesMergeAddressBooks.scala b/testcases/condabd/test/lesynth/AddressesMergeAddressBooks.scala
index 0d6d8c0677806c687186184aa929e80032b869a8..a9154bc7694564291a819dfec6bc0bc641bbffdf 100644
--- a/testcases/condabd/test/lesynth/AddressesMergeAddressBooks.scala
+++ b/testcases/condabd/test/lesynth/AddressesMergeAddressBooks.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   case class Info(
diff --git a/testcases/condabd/test/lesynth/BinarySearchTree.scala b/testcases/condabd/test/lesynth/BinarySearchTree.scala
index 3ddc3fba824da29b9216cbeb60b931eb4e187136..fc49d721c04271af119eae1886282248a78c63ff 100644
--- a/testcases/condabd/test/lesynth/BinarySearchTree.scala
+++ b/testcases/condabd/test/lesynth/BinarySearchTree.scala
@@ -1,7 +1,7 @@
 import scala.collection.immutable.Set
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinarySearchTree {
   sealed abstract class Tree
diff --git a/testcases/condabd/test/lesynth/InsertionSortInsert.scala b/testcases/condabd/test/lesynth/InsertionSortInsert.scala
index ac832856ed117c3a7e68eabae2f5ab87b70ef3bb..7afa8f2b8ba2b90d6fc6e3da518f621e145a4425 100644
--- a/testcases/condabd/test/lesynth/InsertionSortInsert.scala
+++ b/testcases/condabd/test/lesynth/InsertionSortInsert.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object InsertionSort {
   sealed abstract class List
diff --git a/testcases/condabd/test/lesynth/ListConcat.scala b/testcases/condabd/test/lesynth/ListConcat.scala
index 20972e8af864cc1a618fe5d74278ce4298c01c35..3091e9e472d094dcab1a5482ef14d4bba11144fb 100644
--- a/testcases/condabd/test/lesynth/ListConcat.scala
+++ b/testcases/condabd/test/lesynth/ListConcat.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object ListOperations {
 
diff --git a/testcases/condabd/test/lesynth/ListConcatVerifierTest.scala b/testcases/condabd/test/lesynth/ListConcatVerifierTest.scala
index 39b756d8424a66535cf9b4c331fdc7d66cff0bb2..d3e1446ff2640b435998aae6060f82a1cf2c7389 100644
--- a/testcases/condabd/test/lesynth/ListConcatVerifierTest.scala
+++ b/testcases/condabd/test/lesynth/ListConcatVerifierTest.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object ListOperations {
     sealed abstract class List
diff --git a/testcases/condabd/test/lesynth/ListConcatWithEmpty.scala b/testcases/condabd/test/lesynth/ListConcatWithEmpty.scala
index 336fd7e680ca29f30124947d10a1b7a9de8496b0..5b6ae3e46024224597dc4a4af1150c88e7ad3385 100644
--- a/testcases/condabd/test/lesynth/ListConcatWithEmpty.scala
+++ b/testcases/condabd/test/lesynth/ListConcatWithEmpty.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object ListOperations {
     sealed abstract class List
diff --git a/testcases/condabd/test/lesynth/MergeSortSort.scala b/testcases/condabd/test/lesynth/MergeSortSort.scala
index 987c538c4ab36dc9b378f03fc24592210bcbd62b..e96b37543e7636a2870d25cbf967e312e41f5cd5 100644
--- a/testcases/condabd/test/lesynth/MergeSortSort.scala
+++ b/testcases/condabd/test/lesynth/MergeSortSort.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object MergeSort {
   sealed abstract class List
diff --git a/testcases/condabd/test/lesynth/RedBlackTreeInsert.scala b/testcases/condabd/test/lesynth/RedBlackTreeInsert.scala
index e6413ffaf8278fdacb43372eb615ced566e60022..b32b6165ac0d8e7debdf74848b4c2c01f3b67ae5 100644
--- a/testcases/condabd/test/lesynth/RedBlackTreeInsert.scala
+++ b/testcases/condabd/test/lesynth/RedBlackTreeInsert.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object RedBlackTree {
   sealed abstract class Color
@@ -74,4 +74,4 @@ object RedBlackTree {
     }
   }
 
-}
\ No newline at end of file
+}
diff --git a/testcases/datastructures/AVLTree.scala b/testcases/datastructures/AVLTree.scala
index 9c880c0bf81ceb2878c034e002ed3cf6cde2b34f..d94d2da3aa86435867956846a60d9fe1053b3231 100644
--- a/testcases/datastructures/AVLTree.scala
+++ b/testcases/datastructures/AVLTree.scala
@@ -4,7 +4,7 @@
  * Date: 20.11.2013
  **/
 
-import leon.Utils._
+import leon.lang._
 
 object AVLTree  {
   sealed abstract class Tree
diff --git a/testcases/datastructures/AmortizedQueue.scala b/testcases/datastructures/AmortizedQueue.scala
index 6a25184994b42e366122c118ccc6069c10163f05..b7d436bc317c065e5cadb9caa44b72a98c1b9aac 100644
--- a/testcases/datastructures/AmortizedQueue.scala
+++ b/testcases/datastructures/AmortizedQueue.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object AmortizedQueue {
   sealed abstract class List
diff --git a/testcases/datastructures/BinaryTrie.scala b/testcases/datastructures/BinaryTrie.scala
index 83c7bb490e85f42dc09929d06f2ada1a054cf2c1..97871e87113f7393a27f2279a121c9faa4c6ae8d 100644
--- a/testcases/datastructures/BinaryTrie.scala
+++ b/testcases/datastructures/BinaryTrie.scala
@@ -4,7 +4,7 @@
  * Date: 20.11.2013
  **/
 
-import leon.Utils._
+import leon.lang._
 
 object BinaryTrie {
   sealed abstract class Tree
diff --git a/testcases/datastructures/HeapSort.scala b/testcases/datastructures/HeapSort.scala
index 78a72ed2fd19714ad200e42d5fc019db7379e76a..96e11022bed451f4224bad7b01028efd6e703d6f 100644
--- a/testcases/datastructures/HeapSort.scala
+++ b/testcases/datastructures/HeapSort.scala
@@ -4,7 +4,7 @@
  * Date: 20.11.2013
  **/
 
-import leon.Utils._
+import leon.lang._
 
 object HeapSort {
   sealed abstract class List
diff --git a/testcases/datastructures/InsertionSort.scala b/testcases/datastructures/InsertionSort.scala
index e3963ade5ecb0ec434403379044dc274102f9687..1781531cb79175716fa7e8e098594d5c99d35f0a 100644
--- a/testcases/datastructures/InsertionSort.scala
+++ b/testcases/datastructures/InsertionSort.scala
@@ -1,5 +1,5 @@
 import scala.collection.immutable.Set
-import leon.Utils._
+import leon.lang._
 
 object InsertionSort {
   sealed abstract class List
diff --git a/testcases/datastructures/LeftistHeap.scala b/testcases/datastructures/LeftistHeap.scala
index df3bf23c90fbfbbb7847b7b10e6280d796930a8c..629c1013969132416be8e32b598049d9e9f5a69c 100644
--- a/testcases/datastructures/LeftistHeap.scala
+++ b/testcases/datastructures/LeftistHeap.scala
@@ -4,7 +4,7 @@
  * Date: 20.11.2013
  **/
 
-import leon.Utils._
+import leon.lang._
 
 object LeftistHeap {
   sealed abstract class Heap
diff --git a/testcases/datastructures/ListWithSize.scala b/testcases/datastructures/ListWithSize.scala
index 2df0c0cb7d6dc8930bdff155f31485d3e978ea38..660f09a433d571b31daddda5a8124cf0c75bf331 100644
--- a/testcases/datastructures/ListWithSize.scala
+++ b/testcases/datastructures/ListWithSize.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object ListWithSize {
     sealed abstract class List
diff --git a/testcases/datastructures/SortedList.scala b/testcases/datastructures/SortedList.scala
index 6e530b68850d4db4fafdafd213b02d71e5435f57..41451641beaa7917e3fbfa9621d0cdbb53f05893 100644
--- a/testcases/datastructures/SortedList.scala
+++ b/testcases/datastructures/SortedList.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object SortedList {
   sealed abstract class List
diff --git a/testcases/datastructures/TreeListSetNoDup.scala b/testcases/datastructures/TreeListSetNoDup.scala
index b6649c5ca6d28fc6933bc94aec5119958742a8b9..44d7fcf0b10d4a4a6c5dd5dd702ff2c4ccb967f8 100644
--- a/testcases/datastructures/TreeListSetNoDup.scala
+++ b/testcases/datastructures/TreeListSetNoDup.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinaryTree {
   // list of integers
diff --git a/testcases/graph/MST/MSTMap.scala b/testcases/graph/MST/MSTMap.scala
index 71e894754638fc5a3c44162e2be8ba87e17ca510..da2a08fc0052f4cb96c23b72e7a5fcb217dae26b 100644
--- a/testcases/graph/MST/MSTMap.scala
+++ b/testcases/graph/MST/MSTMap.scala
@@ -1,7 +1,7 @@
 import scala.collection.immutable._
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object MSTMap {
 
diff --git a/testcases/graph/MST/SpanningTree.scala b/testcases/graph/MST/SpanningTree.scala
index 862842e08f180736e9f8ffd7f2caa7d62113ae09..0b564b62dc74d41e14d7088f4a80aa3f6e2b0f44 100644
--- a/testcases/graph/MST/SpanningTree.scala
+++ b/testcases/graph/MST/SpanningTree.scala
@@ -1,7 +1,7 @@
 import scala.collection.immutable._
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object SpanningTree {
   case class Graph(nVertices : Int, edges : Set[(Int,Int)])
diff --git a/testcases/graph/SetIteration.scala b/testcases/graph/SetIteration.scala
index 8730d4abcd727a469eb7ec6384c82637127db43e..f272a48a433cd7748ac9fbb551c6d5c81539f2e4 100644
--- a/testcases/graph/SetIteration.scala
+++ b/testcases/graph/SetIteration.scala
@@ -1,7 +1,7 @@
 import scala.collection.immutable._
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 /** Examples of iteration over set elements using 'epsilon'.
  *
diff --git a/testcases/graph/SimpleInduction.scala b/testcases/graph/SimpleInduction.scala
index 50f9109797c1ce3e9c733605f01eb7aa19df4993..f9bf0bf3de9f80f7c53042798a645146f782b162 100644
--- a/testcases/graph/SimpleInduction.scala
+++ b/testcases/graph/SimpleInduction.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 /** A simple example of inductive proofs.
  * 
diff --git a/testcases/graph/SortedNDList.scala b/testcases/graph/SortedNDList.scala
index f7bef6ff38048f6c2d63b4f406c0b0effed39d93..98c06e7c95ac7c6f68a7b61f9a35b54bc85661e4 100644
--- a/testcases/graph/SortedNDList.scala
+++ b/testcases/graph/SortedNDList.scala
@@ -1,7 +1,7 @@
 import scala.collection.immutable._
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 /** Tests for SortedNDList
  */
diff --git a/testcases/graph/Subgraph.scala b/testcases/graph/Subgraph.scala
index d7f245da07cc7683c861f900434bffd1f1c6193d..2f60f78f07cb4f417a6f94381a101b9621d9af13 100644
--- a/testcases/graph/Subgraph.scala
+++ b/testcases/graph/Subgraph.scala
@@ -1,7 +1,7 @@
 import scala.collection.immutable._
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Subgraph {
   /** Graph representation.
diff --git a/testcases/graph/SubgraphMap.scala b/testcases/graph/SubgraphMap.scala
index 15029853287f495c1a175ed71b65610e9a83f990..90522ba9c64eb052180ec288940e0d52b39d5662 100644
--- a/testcases/graph/SubgraphMap.scala
+++ b/testcases/graph/SubgraphMap.scala
@@ -1,7 +1,7 @@
 import scala.collection.immutable._
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object SubgraphSet {
   case class Graph(nVertices : Int, edges : Map[(Int,Int), Int])
diff --git a/testcases/graph/TreeEquivalence.scala b/testcases/graph/TreeEquivalence.scala
index ea1be52ef5581cfa91a7381a844da83f3c4cbe3e..c059473ea82a6643212ccdb9d71712156d18c8e4 100644
--- a/testcases/graph/TreeEquivalence.scala
+++ b/testcases/graph/TreeEquivalence.scala
@@ -1,7 +1,7 @@
 import scala.collection.immutable._
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object TreeEquivalence {
   /** Graph representation.
diff --git a/testcases/graph/TreeEquivalenceMap.scala b/testcases/graph/TreeEquivalenceMap.scala
index 599557f7f11abde533dcb99f0b6ffe8168b4bb71..e0dd4bca5d16ecafcfa8ee847ca4df0faae719a6 100644
--- a/testcases/graph/TreeEquivalenceMap.scala
+++ b/testcases/graph/TreeEquivalenceMap.scala
@@ -1,7 +1,7 @@
 import scala.collection.immutable._
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object TreeEquivalenceSet {
   /*
diff --git a/testcases/graph/dijkstras/DijkstrasSet.scala b/testcases/graph/dijkstras/DijkstrasSet.scala
index f914864627909f182cfe06d5733ddd62af7a7f48..711eff7459e83fcce4e6e86c3ec49a8454b36ce4 100644
--- a/testcases/graph/dijkstras/DijkstrasSet.scala
+++ b/testcases/graph/dijkstras/DijkstrasSet.scala
@@ -1,7 +1,7 @@
 import scala.collection.immutable._
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 /** Implementation of Dijkstra's algorithm. Iterates over vertex IDs, looking
  * distances up in a map, to find the nearest unvisited node.
diff --git a/testcases/graph/dijkstras/DijkstrasSetToVisit.scala b/testcases/graph/dijkstras/DijkstrasSetToVisit.scala
index 6b6cccec647e3d9be4b47e3483021753d48e8b87..eb954e7caaec7356fbf1598abc5704dea1b4932c 100644
--- a/testcases/graph/dijkstras/DijkstrasSetToVisit.scala
+++ b/testcases/graph/dijkstras/DijkstrasSetToVisit.scala
@@ -1,7 +1,7 @@
 import scala.collection.immutable._
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 /** Implementation of Dijkstra's algorithm. Maintains a list of visitable
  * vertices, and iterates over this, looking distances up in a map.
diff --git a/testcases/graph/dijkstras/DijkstrasSortedList.scala b/testcases/graph/dijkstras/DijkstrasSortedList.scala
index 8e586348d6eb1e5d4175a12b5cf27b0d4e3bc040..d3958a893cf86a5550db490c83f06bc387014f4b 100644
--- a/testcases/graph/dijkstras/DijkstrasSortedList.scala
+++ b/testcases/graph/dijkstras/DijkstrasSortedList.scala
@@ -1,7 +1,7 @@
 import scala.collection.immutable._
 
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 /** Implementation of Dijkstra's algorithm.
  *
diff --git a/testcases/graveyard/Choose.scala b/testcases/graveyard/Choose.scala
index 229d07286fcfa8442d60b0e9612efba5193b3282..0584edd430169825d3e1d6e5b2acc20e8d0f4b8b 100644
--- a/testcases/graveyard/Choose.scala
+++ b/testcases/graveyard/Choose.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object ChooseTest {
 
diff --git a/testcases/graveyard/ConnectedTest.scala b/testcases/graveyard/ConnectedTest.scala
index 00125985290e6eefb3ab4627351800af9741acdb..f67ebb8cbff8a6cb4c49037101857a99ac29d3b5 100644
--- a/testcases/graveyard/ConnectedTest.scala
+++ b/testcases/graveyard/ConnectedTest.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object VerySimple {
 		sealed abstract class L0
diff --git a/testcases/graveyard/Expr2Comp.scala b/testcases/graveyard/Expr2Comp.scala
index eca1fe6f5b0527034ec6f866fbfe362776c1618d..1f3afbb930cc205d70f7e3c80e68548a5d74fd07 100644
--- a/testcases/graveyard/Expr2Comp.scala
+++ b/testcases/graveyard/Expr2Comp.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object ExprComp {
   // Lists
diff --git a/testcases/graveyard/ExprComp.scala b/testcases/graveyard/ExprComp.scala
index 116f0099bd4741717322355a4c0a1709eb89d4f6..5309935d66cd08ce8b9d9068fbe6f71f57a81e43 100644
--- a/testcases/graveyard/ExprComp.scala
+++ b/testcases/graveyard/ExprComp.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object ExprComp {
 
diff --git a/testcases/graveyard/Sat.scala b/testcases/graveyard/Sat.scala
index 1c7caaf2205803d665a54e5d62245854596972fe..28dd0057efbf97b5211111f6441e18761bd0847e 100644
--- a/testcases/graveyard/Sat.scala
+++ b/testcases/graveyard/Sat.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Sat {
 
diff --git a/testcases/graveyard/SortedTree.scala b/testcases/graveyard/SortedTree.scala
index 1ccf26880126514e3d5d8b18e32c0eb1065e1d36..fbee8f182a78a74494d7f10bde03759e6d1e1d28 100644
--- a/testcases/graveyard/SortedTree.scala
+++ b/testcases/graveyard/SortedTree.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object SortedTree {
   sealed abstract class Tree
diff --git a/testcases/graveyard/Test.scala b/testcases/graveyard/Test.scala
index 79f143b3497fbf4bd14ad4e87948872175e066ed..d3c5db95b535c4d250150d5527bdbb7c017192bb 100644
--- a/testcases/graveyard/Test.scala
+++ b/testcases/graveyard/Test.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object Test {
     sealed abstract class List
diff --git a/testcases/graveyard/UseContradictoryLemma.scala b/testcases/graveyard/UseContradictoryLemma.scala
index 5ab165bfcd6ed0d9a72145b1b4b519c4a5642aeb..65ba4ea582fb219bc0287dc1a96fe1a17f3de5d6 100644
--- a/testcases/graveyard/UseContradictoryLemma.scala
+++ b/testcases/graveyard/UseContradictoryLemma.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object UseContradictoryLemma {
 
diff --git a/testcases/graveyard/VerySimple.scala b/testcases/graveyard/VerySimple.scala
index d89391d4287b63cab023b0b15dd13fd6e95d6c8b..7dc3c05b67b6d35b4ff003e0624a95dad8549d79 100644
--- a/testcases/graveyard/VerySimple.scala
+++ b/testcases/graveyard/VerySimple.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object VerySimple {
     sealed abstract class List
diff --git a/testcases/graveyard/Viktor.scala b/testcases/graveyard/Viktor.scala
index 3d86ee0ffbbf5f7f9bfd4053b2e7f44484ae056c..11b013dc475ccaefa4da7cec19f536919b828098 100644
--- a/testcases/graveyard/Viktor.scala
+++ b/testcases/graveyard/Viktor.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Viktor {
   def transitive(x: Boolean, y: Boolean, z: Boolean) : Boolean = {
diff --git a/testcases/insynth-leon-tests/Arguments.scala b/testcases/insynth-leon-tests/Arguments.scala
index cae6e5f9e77fb97aa52393ed4a62e40a9a07dae7..75b4eceaaf629f5ed479faebbf6f38bfcd146f07 100644
--- a/testcases/insynth-leon-tests/Arguments.scala
+++ b/testcases/insynth-leon-tests/Arguments.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Hole { 
   
diff --git a/testcases/insynth-leon-tests/BubbleSortBug.scala b/testcases/insynth-leon-tests/BubbleSortBug.scala
index 4377e43994275a92de92a4a49f8f7bc5825675f2..2f76a450d3e4622e111bed74fa7dca56e4c9dfae 100644
--- a/testcases/insynth-leon-tests/BubbleSortBug.scala
+++ b/testcases/insynth-leon-tests/BubbleSortBug.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 /* The calculus of Computation textbook */
 
diff --git a/testcases/insynth-leon-tests/CaseClassSelectExample.scala b/testcases/insynth-leon-tests/CaseClassSelectExample.scala
index 5239efa37de79807bbe50df7a0132cae72e6f7c5..a4c127f0e701cf097b48e6d7cfba7cf3b013300f 100644
--- a/testcases/insynth-leon-tests/CaseClassSelectExample.scala
+++ b/testcases/insynth-leon-tests/CaseClassSelectExample.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object CaseClassSelectExample { 
 
diff --git a/testcases/insynth-leon-tests/Hole.scala b/testcases/insynth-leon-tests/Hole.scala
index f860590f3ae0efcdf69797795deabfab2642289b..5bccc38daba02bdf7e79b561f57c7e7f71cd4015 100644
--- a/testcases/insynth-leon-tests/Hole.scala
+++ b/testcases/insynth-leon-tests/Hole.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Hole { 
   
diff --git a/testcases/insynth-leon-tests/ListOperationsHole.scala b/testcases/insynth-leon-tests/ListOperationsHole.scala
index bd3cb28e6a2a6a9c19822f84562a82c62d0e3737..e0587425d1d581553d3804d19d11fdbc6cdf51d0 100644
--- a/testcases/insynth-leon-tests/ListOperationsHole.scala
+++ b/testcases/insynth-leon-tests/ListOperationsHole.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object ListOperations {
     sealed abstract class List
diff --git a/testcases/insynth-leon-tests/RedBlackTreeFull.scala b/testcases/insynth-leon-tests/RedBlackTreeFull.scala
index bc2de6ba96ee699736d4558932b752eea9ebba9f..11daef0b03ee0e4eae57db7735128456e3844649 100644
--- a/testcases/insynth-leon-tests/RedBlackTreeFull.scala
+++ b/testcases/insynth-leon-tests/RedBlackTreeFull.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object RedBlackTree { 
   sealed abstract class Color
diff --git a/testcases/insynth-synthesis-tests/Hole.scala b/testcases/insynth-synthesis-tests/Hole.scala
index 091afbdb46d9d6c19fab2b627617fe7468c803df..933825e2f3b608cd66dc83e256a30e1257b0591f 100644
--- a/testcases/insynth-synthesis-tests/Hole.scala
+++ b/testcases/insynth-synthesis-tests/Hole.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Hole { 
   
diff --git a/testcases/insynth-synthesis-tests/LocalScope.scala b/testcases/insynth-synthesis-tests/LocalScope.scala
index 4d39693476d3cd55d7c419c5a090e0304cb69842..5b747616213aec2263423fcc80751856e8f2b0cc 100644
--- a/testcases/insynth-synthesis-tests/LocalScope.scala
+++ b/testcases/insynth-synthesis-tests/LocalScope.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object LocalScope {
   sealed abstract class Color
@@ -28,4 +28,4 @@ object LocalScope {
       
     case Empty() => true
   }
-}
\ No newline at end of file
+}
diff --git a/testcases/lesynth-results/RedBlackTreeSynthResult.scala b/testcases/lesynth-results/RedBlackTreeSynthResult.scala
index c1c1c46b3c70af522d42fc083da85299b51d2116..511eb602e5987d2282cbcd3e754050dd71dfbef7 100644
--- a/testcases/lesynth-results/RedBlackTreeSynthResult.scala
+++ b/testcases/lesynth-results/RedBlackTreeSynthResult.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object RedBlackTree { 
   sealed abstract class Color
@@ -85,7 +85,7 @@ object RedBlackTree {
           }
       })
     } else {
-      leon.Utils.error[Tree]("Precondition failed")
+      leon.lang.error[Tree]("Precondition failed")
     }
   } ensuring (res => content(res) == content(t) ++ Set(x) 
                    && size(t) <= size(res) && size(res) <= size(t) + 1
diff --git a/testcases/lesynth-results/RedBlackTreeSynthResultBad.scala b/testcases/lesynth-results/RedBlackTreeSynthResultBad.scala
index 4be3aae0f689d119048297be1f7aac259271db29..5bee9ba90a119c6778067dff279c45022f5797e1 100644
--- a/testcases/lesynth-results/RedBlackTreeSynthResultBad.scala
+++ b/testcases/lesynth-results/RedBlackTreeSynthResultBad.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object RedBlackTree { 
   sealed abstract class Color
@@ -85,7 +85,7 @@ object RedBlackTree {
           }
       })
     } else {
-      leon.Utils.error[Tree]("Precondition failed")
+      leon.lang.error[Tree]("Precondition failed")
     }
   } ensuring (res => content(res) == content(t) ++ Set(x) 
                    && size(t) <= size(res) && size(res) <= size(t) + 1
diff --git a/testcases/pldi2011-testcases/AssociativeList.scala b/testcases/pldi2011-testcases/AssociativeList.scala
index 6b9319afdb7d72519f8e8d316901a12b7e652201..2b99141b2f57708ad03565f8380589adc84c2863 100644
--- a/testcases/pldi2011-testcases/AssociativeList.scala
+++ b/testcases/pldi2011-testcases/AssociativeList.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object AssociativeList { 
   sealed abstract class KeyValuePairAbs
diff --git a/testcases/pldi2011-testcases/ForElimination.scala b/testcases/pldi2011-testcases/ForElimination.scala
index ed8e6b8776da928730c899b894d34294750143e5..fe96501331a6f39ca9c794d75341d98b6fb58eeb 100644
--- a/testcases/pldi2011-testcases/ForElimination.scala
+++ b/testcases/pldi2011-testcases/ForElimination.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object ForElimination { 
 
diff --git a/testcases/pldi2011-testcases/InsertionSort.scala b/testcases/pldi2011-testcases/InsertionSort.scala
index a1215b025cc8d5dd906cce8917509f69edf1bd6e..3e606fe8b41d96c284ebf261ab58af1ee6016172 100644
--- a/testcases/pldi2011-testcases/InsertionSort.scala
+++ b/testcases/pldi2011-testcases/InsertionSort.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object InsertionSort {
   sealed abstract class List
diff --git a/testcases/pldi2011-testcases/LambdaEval.scala b/testcases/pldi2011-testcases/LambdaEval.scala
index 2a26e46877b75c7407ac2e946e2594286bd2bf79..4dde6b2bc88bca4e0fd5295903c7a33b83474d95 100644
--- a/testcases/pldi2011-testcases/LambdaEval.scala
+++ b/testcases/pldi2011-testcases/LambdaEval.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object LambdaEval { 
   sealed abstract class Expr
diff --git a/testcases/pldi2011-testcases/PropositionalLogic.scala b/testcases/pldi2011-testcases/PropositionalLogic.scala
index ef7b0d34aa82e02d0f88b7e386ba705250e2825e..0270bdf87ae8cea34d98afcbfe6f1ca164d7ed57 100644
--- a/testcases/pldi2011-testcases/PropositionalLogic.scala
+++ b/testcases/pldi2011-testcases/PropositionalLogic.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object PropositionalLogic { 
 
diff --git a/testcases/pldi2011-testcases/QuickSort.scala b/testcases/pldi2011-testcases/QuickSort.scala
index c0456021865c200cf9ea747d473b1d8eecbdc89c..a0a151057edd315422d87236b793b1672a64a9ac 100644
--- a/testcases/pldi2011-testcases/QuickSort.scala
+++ b/testcases/pldi2011-testcases/QuickSort.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object QuickSort {
   sealed abstract class List
diff --git a/testcases/pldi2011-testcases/RedBlackTree.scala b/testcases/pldi2011-testcases/RedBlackTree.scala
index aca029fb2454d29fb6c20486d9572bb14defd5b9..3ebfa25e2a4fbfbeaf1fd470848276747c19c87d 100644
--- a/testcases/pldi2011-testcases/RedBlackTree.scala
+++ b/testcases/pldi2011-testcases/RedBlackTree.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object RedBlackTree { 
   sealed abstract class Color
diff --git a/testcases/pldi2011-testcases/RedBlackTreeDeletion.scala b/testcases/pldi2011-testcases/RedBlackTreeDeletion.scala
index 7cc45ca3c65b233d03a0579bbfb51e9010c666a5..585135d06645f4e4fc250d878b3808a797f3f5f9 100644
--- a/testcases/pldi2011-testcases/RedBlackTreeDeletion.scala
+++ b/testcases/pldi2011-testcases/RedBlackTreeDeletion.scala
@@ -1,5 +1,5 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
+import leon.annotation._
 
 object RedBlackTree { 
   sealed abstract class Color
diff --git a/testcases/pldi2011-testcases/SemanticsPreservation.scala b/testcases/pldi2011-testcases/SemanticsPreservation.scala
index ece2e608eb3bdee558b9e7ca2e00f0a36c6f5a6e..034ec122247d26a805518a44ce13c9a0538cb7a9 100644
--- a/testcases/pldi2011-testcases/SemanticsPreservation.scala
+++ b/testcases/pldi2011-testcases/SemanticsPreservation.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object SemanticsPreservation { 
 
diff --git a/testcases/pldi2011-testcases/TreeMap.scala b/testcases/pldi2011-testcases/TreeMap.scala
index 77318cdd29cdb3d0c8ecf2b62ac37639fccfc048..44b85cff7e4b0df9586939bcefd43cd5398ef66c 100644
--- a/testcases/pldi2011-testcases/TreeMap.scala
+++ b/testcases/pldi2011-testcases/TreeMap.scala
@@ -1,5 +1,5 @@
 import scala.collection.immutable.Set
-import leon.Utils._
+import leon.lang._
 
 object TreeMap {
   sealed abstract class TreeMap
diff --git a/testcases/runtime/CachedList.scala b/testcases/runtime/CachedList.scala
index ac34d980abb7bf0c4ac74aaab246930eadc385bf..bf56ed8d1f991613c3068dd4f46c60abf8c84b6f 100644
--- a/testcases/runtime/CachedList.scala
+++ b/testcases/runtime/CachedList.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object SortedList {
   abstract class List
diff --git a/testcases/runtime/SquareRoot.scala b/testcases/runtime/SquareRoot.scala
index dd4eee9222fe19ce29e992a7f6012cfb2087bc2f..9b0ea5c49440f9628a2326ad96a81ff60e2ccd31 100644
--- a/testcases/runtime/SquareRoot.scala
+++ b/testcases/runtime/SquareRoot.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object SquareRoot {
 
@@ -13,7 +13,7 @@ object SquareRoot {
       0
     } else {
       if ((x < 0)) {
-        leon.Utils.error[(Int)]("(((y * y) ≤ x) ∧ (((y + 1) * (y + 1)) ≥ x)) is UNSAT!")
+        leon.lang.error[(Int)]("(((y * y) ≤ x) ∧ (((y + 1) * (y + 1)) ≥ x)) is UNSAT!")
       } else {
         (choose { (y: Int) =>
           (((y * y) <= x) && (((y + 1) * (y + 1)) >= x))
diff --git a/testcases/sas2011-testcases/AmortizedQueue.scala b/testcases/sas2011-testcases/AmortizedQueue.scala
index dd5a75f89735805a74612665e487aa8fa99ec397..52e4ed7e2c313d83b46f766e7694e152ca4c19b9 100644
--- a/testcases/sas2011-testcases/AmortizedQueue.scala
+++ b/testcases/sas2011-testcases/AmortizedQueue.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object AmortizedQueue {
   sealed abstract class List
diff --git a/testcases/sas2011-testcases/AssociativeList.scala b/testcases/sas2011-testcases/AssociativeList.scala
index f5a2fc0415a2cf6023f9ae1f3620e99f9fdc27cb..6567c4786e3ef021d5e1f8a4c2de91562418766e 100644
--- a/testcases/sas2011-testcases/AssociativeList.scala
+++ b/testcases/sas2011-testcases/AssociativeList.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object AssociativeList { 
   sealed abstract class KeyValuePairAbs
diff --git a/testcases/sas2011-testcases/InsertionSort.scala b/testcases/sas2011-testcases/InsertionSort.scala
index d2ae67b3bb465f13437a1eb70a57a8e7e613347a..a29e2116d2783f02f4759d0ffd1e8103420883fe 100644
--- a/testcases/sas2011-testcases/InsertionSort.scala
+++ b/testcases/sas2011-testcases/InsertionSort.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object InsertionSort {
   sealed abstract class List
diff --git a/testcases/sas2011-testcases/ListOperations.scala b/testcases/sas2011-testcases/ListOperations.scala
index a4fc4f8dc44a90f59a772b52b1a05053316e94d2..86d0f522f69633e0321da4d52bb32352b7cc1239 100644
--- a/testcases/sas2011-testcases/ListOperations.scala
+++ b/testcases/sas2011-testcases/ListOperations.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object ListOperations {
     sealed abstract class List
diff --git a/testcases/sas2011-testcases/PropositionalLogic.scala b/testcases/sas2011-testcases/PropositionalLogic.scala
index a35c3ef9be56871900d5e9474b385f0896edccd4..ca410a5ae541201b399dd680fc05a9427e9394ee 100644
--- a/testcases/sas2011-testcases/PropositionalLogic.scala
+++ b/testcases/sas2011-testcases/PropositionalLogic.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object PropositionalLogic { 
 
diff --git a/testcases/sas2011-testcases/RedBlackTree.scala b/testcases/sas2011-testcases/RedBlackTree.scala
index bc2de6ba96ee699736d4558932b752eea9ebba9f..11daef0b03ee0e4eae57db7735128456e3844649 100644
--- a/testcases/sas2011-testcases/RedBlackTree.scala
+++ b/testcases/sas2011-testcases/RedBlackTree.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object RedBlackTree { 
   sealed abstract class Color
diff --git a/testcases/sas2011-testcases/SearchLinkedList.scala b/testcases/sas2011-testcases/SearchLinkedList.scala
index 2c137fd4ad6b9d411f7e14b4ada6b834234c9e9e..02f265f12b1c6cf6e12c0d6fcf5df6dbb3e71558 100644
--- a/testcases/sas2011-testcases/SearchLinkedList.scala
+++ b/testcases/sas2011-testcases/SearchLinkedList.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object SearchLinkedList {
   sealed abstract class List
diff --git a/testcases/sas2011-testcases/SumAndMax.scala b/testcases/sas2011-testcases/SumAndMax.scala
index 0aa4ce7060a391d34dd047338fcd1f638054843f..a3fd5c3a50d6c56592dbd6d48b7bc90ac940d58f 100644
--- a/testcases/sas2011-testcases/SumAndMax.scala
+++ b/testcases/sas2011-testcases/SumAndMax.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object SumAndMax {
   sealed abstract class List
diff --git a/testcases/scala-workshop/AmortizedQueue.scala b/testcases/scala-workshop/AmortizedQueue.scala
index dd5a75f89735805a74612665e487aa8fa99ec397..52e4ed7e2c313d83b46f766e7694e152ca4c19b9 100644
--- a/testcases/scala-workshop/AmortizedQueue.scala
+++ b/testcases/scala-workshop/AmortizedQueue.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object AmortizedQueue {
   sealed abstract class List
diff --git a/testcases/scala-workshop/AmortizedQueueImp.scala b/testcases/scala-workshop/AmortizedQueueImp.scala
index 71d199ea9d1152f708268f073e5cb57fde549100..afaefbca1b6db09abf8e8cc34e7dfd50ec3b7a44 100644
--- a/testcases/scala-workshop/AmortizedQueueImp.scala
+++ b/testcases/scala-workshop/AmortizedQueueImp.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object AmortizedQueue {
   sealed abstract class List
diff --git a/testcases/scala-workshop/Arithmetic.scala b/testcases/scala-workshop/Arithmetic.scala
index 2b90bda91805791950d4c9129196b0ebb30bb3e2..f3f10b892d1dfffd6227ff3fad1aaed2f074c474 100644
--- a/testcases/scala-workshop/Arithmetic.scala
+++ b/testcases/scala-workshop/Arithmetic.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Arithmetic {
 
diff --git a/testcases/scala-workshop/AssociativeList.scala b/testcases/scala-workshop/AssociativeList.scala
index f5a2fc0415a2cf6023f9ae1f3620e99f9fdc27cb..6567c4786e3ef021d5e1f8a4c2de91562418766e 100644
--- a/testcases/scala-workshop/AssociativeList.scala
+++ b/testcases/scala-workshop/AssociativeList.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object AssociativeList { 
   sealed abstract class KeyValuePairAbs
diff --git a/testcases/scala-workshop/AssociativeListImp.scala b/testcases/scala-workshop/AssociativeListImp.scala
index dabf9c994336fb3ddd74b18d5cc170aa7586d995..d15101ec7050f106dc7ad60859f4f60e17fac956 100644
--- a/testcases/scala-workshop/AssociativeListImp.scala
+++ b/testcases/scala-workshop/AssociativeListImp.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object AssociativeListImp { 
   sealed abstract class KeyValuePairAbs
diff --git a/testcases/scala-workshop/ListOperations.scala b/testcases/scala-workshop/ListOperations.scala
index a4fc4f8dc44a90f59a772b52b1a05053316e94d2..86d0f522f69633e0321da4d52bb32352b7cc1239 100644
--- a/testcases/scala-workshop/ListOperations.scala
+++ b/testcases/scala-workshop/ListOperations.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object ListOperations {
     sealed abstract class List
diff --git a/testcases/scala-workshop/ListOperationsImp.scala b/testcases/scala-workshop/ListOperationsImp.scala
index f30c9d0be06e7a0436883f082d28f6ea687b8479..542129826108d067501c5298a0bf34ad125ac25a 100644
--- a/testcases/scala-workshop/ListOperationsImp.scala
+++ b/testcases/scala-workshop/ListOperationsImp.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object ListOperationsImp {
 
diff --git a/testcases/scala-workshop/PropositionalLogic.scala b/testcases/scala-workshop/PropositionalLogic.scala
index a35c3ef9be56871900d5e9474b385f0896edccd4..ca410a5ae541201b399dd680fc05a9427e9394ee 100644
--- a/testcases/scala-workshop/PropositionalLogic.scala
+++ b/testcases/scala-workshop/PropositionalLogic.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object PropositionalLogic { 
 
diff --git a/testcases/scala-workshop/RedBlackTree.scala b/testcases/scala-workshop/RedBlackTree.scala
index bc2de6ba96ee699736d4558932b752eea9ebba9f..11daef0b03ee0e4eae57db7735128456e3844649 100644
--- a/testcases/scala-workshop/RedBlackTree.scala
+++ b/testcases/scala-workshop/RedBlackTree.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object RedBlackTree { 
   sealed abstract class Color
diff --git a/testcases/scala-workshop/SearchLinkedList.scala b/testcases/scala-workshop/SearchLinkedList.scala
index 2c137fd4ad6b9d411f7e14b4ada6b834234c9e9e..02f265f12b1c6cf6e12c0d6fcf5df6dbb3e71558 100644
--- a/testcases/scala-workshop/SearchLinkedList.scala
+++ b/testcases/scala-workshop/SearchLinkedList.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object SearchLinkedList {
   sealed abstract class List
diff --git a/testcases/scala-workshop/Sorting.scala b/testcases/scala-workshop/Sorting.scala
index 3c683e6e5f3873d2eaa4d4413ac9fe9f01a888ff..faae0add05e87d0eda6b8fb46f4c4faca0b901ce 100644
--- a/testcases/scala-workshop/Sorting.scala
+++ b/testcases/scala-workshop/Sorting.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 // Sorting lists is a fundamental problem in CS.
 object Sorting {
diff --git a/testcases/scala-workshop/SumAndMax.scala b/testcases/scala-workshop/SumAndMax.scala
index 0aa4ce7060a391d34dd047338fcd1f638054843f..a3fd5c3a50d6c56592dbd6d48b7bc90ac940d58f 100644
--- a/testcases/scala-workshop/SumAndMax.scala
+++ b/testcases/scala-workshop/SumAndMax.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object SumAndMax {
   sealed abstract class List
diff --git a/testcases/scala-workshop/SumAndMaxImp.scala b/testcases/scala-workshop/SumAndMaxImp.scala
index d6c9896a82aebb711d05a0fa9c3f8de156a51be9..37765f620200fe87abe0b7fc1d6e0cd015098a7b 100644
--- a/testcases/scala-workshop/SumAndMaxImp.scala
+++ b/testcases/scala-workshop/SumAndMaxImp.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object SumAndMaxImp {
 
diff --git a/testcases/synthesis/ADTInduction.scala b/testcases/synthesis/ADTInduction.scala
index 7487247cda198b0a6f51cf7a39f2f922f6736eda..edd5ab10147b9c0b7d0b915a78f2c0edb1c810c7 100644
--- a/testcases/synthesis/ADTInduction.scala
+++ b/testcases/synthesis/ADTInduction.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object SortedList {
   sealed abstract class List
diff --git a/testcases/synthesis/BinaryTree.scala b/testcases/synthesis/BinaryTree.scala
index 7409a2745ce8375e20e32b9b63d1a32562208ba0..a298ca980ff5108c7e118a6b3fd47d8c1dbfed88 100644
--- a/testcases/synthesis/BinaryTree.scala
+++ b/testcases/synthesis/BinaryTree.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinaryTree {
   sealed abstract class Tree
diff --git a/testcases/synthesis/CegisExamples.scala b/testcases/synthesis/CegisExamples.scala
index a7f23e817444ab2c4885d052a18829e6159640b3..1c077055cdc7e545fc563890853ee769113a3da0 100644
--- a/testcases/synthesis/CegisExamples.scala
+++ b/testcases/synthesis/CegisExamples.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object CegisTests {
   sealed abstract class List
diff --git a/testcases/synthesis/CegisFunctions.scala b/testcases/synthesis/CegisFunctions.scala
index a3451d01dd35fbeee1f55c5874c141db1bac0739..3139d130e92ad9649e652e518c74a1a01759b4c1 100644
--- a/testcases/synthesis/CegisFunctions.scala
+++ b/testcases/synthesis/CegisFunctions.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object CegisTests {
   sealed abstract class List
diff --git a/testcases/synthesis/ChooseArith.scala b/testcases/synthesis/ChooseArith.scala
index b910cd4ea699d51566f69f6b2aff3d43c6e6c2c8..bee28c19dbbb327f5a9ae87e0f65be87d8ce111b 100644
--- a/testcases/synthesis/ChooseArith.scala
+++ b/testcases/synthesis/ChooseArith.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object ChooseArith {
   def c1(a : Int) : (Int, Int) = 
diff --git a/testcases/synthesis/ChooseIneq.scala b/testcases/synthesis/ChooseIneq.scala
index fc0241ff0275731401a44af10fabfcfa70e506de..bb5921bea1ab83521ceff5976036eaf8b9f7efa7 100644
--- a/testcases/synthesis/ChooseIneq.scala
+++ b/testcases/synthesis/ChooseIneq.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object ChooseIneq {
   def c1(a: Int, b: Int): (Int, Int) = { 
diff --git a/testcases/synthesis/ChoosePos.scala b/testcases/synthesis/ChoosePos.scala
index 530d20c8120a69579ff3aed4c2cd8c3d42cc84f0..decf2875d424d520267fa90673311d207a01fa89 100644
--- a/testcases/synthesis/ChoosePos.scala
+++ b/testcases/synthesis/ChoosePos.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object ChoosePos {
 
diff --git a/testcases/synthesis/ChurchNumerals.scala b/testcases/synthesis/ChurchNumerals.scala
index 287e4ecefe9ecb24b43e0d5f0a8fded7cdd8e85f..ba858741091239e6f5b9a65e6d9eed31edafe856 100644
--- a/testcases/synthesis/ChurchNumerals.scala
+++ b/testcases/synthesis/ChurchNumerals.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 object ChurchNumerals {
   sealed abstract class Num
   case class Zero() extends Num
diff --git a/testcases/synthesis/DrSuter.scala b/testcases/synthesis/DrSuter.scala
index 12b7dac716b63fd3876b01377e74772c2a684efd..39b5d7edce186427c5b52a608250eea4001a9580 100644
--- a/testcases/synthesis/DrSuter.scala
+++ b/testcases/synthesis/DrSuter.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object DrSuter {
 
diff --git a/testcases/synthesis/FastExp.scala b/testcases/synthesis/FastExp.scala
index 4d094d500f73fd4a077e78ce2f836f92f125c3f0..c230771289952998e15d489aa80949beeb842e65 100644
--- a/testcases/synthesis/FastExp.scala
+++ b/testcases/synthesis/FastExp.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object FastExp {
 
diff --git a/testcases/synthesis/FiniteSort.scala b/testcases/synthesis/FiniteSort.scala
index 249daa5b3248179de21b76cf503f12019a0f960a..e4660ebb47107a7fce36335b97085e077e48994c 100644
--- a/testcases/synthesis/FiniteSort.scala
+++ b/testcases/synthesis/FiniteSort.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object FiniteSort {
 
diff --git a/testcases/synthesis/Injection.scala b/testcases/synthesis/Injection.scala
index 32c91ccad03674a50cd5cfb38f745fb091a046e1..43a4be6768df1056387ef2eb9fc8466020c6cd08 100644
--- a/testcases/synthesis/Injection.scala
+++ b/testcases/synthesis/Injection.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Injection {
   sealed abstract class List
diff --git a/testcases/synthesis/InnerSplit.scala b/testcases/synthesis/InnerSplit.scala
index b584c45e475471cf54316c80efc8e130dafdbc4b..7b2be7741dd6b703703b1c07391073a321a8870b 100644
--- a/testcases/synthesis/InnerSplit.scala
+++ b/testcases/synthesis/InnerSplit.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Test {
   def test(x: Int, y: Int) = choose((z: Int) => z >= x && z >= y && (z == x || z == y))
diff --git a/testcases/synthesis/Justify.scala b/testcases/synthesis/Justify.scala
index cc0227115e8b05e1a665526ef20100b629a5920e..53a362f8a07c2d5a0259fc8c63a3df802f170105 100644
--- a/testcases/synthesis/Justify.scala
+++ b/testcases/synthesis/Justify.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Justify {
 
diff --git a/testcases/synthesis/Matching.scala b/testcases/synthesis/Matching.scala
index 1be8706b677e62c1d366f845edc80b684be0a401..393d64c53a49908eb3a21adafab7b15b9744c208 100644
--- a/testcases/synthesis/Matching.scala
+++ b/testcases/synthesis/Matching.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Matching {
   def t1(a: NatList) = choose( (x: Nat) => Cons(x, Nil()) == a)
diff --git a/testcases/synthesis/NewYearsSong.scala b/testcases/synthesis/NewYearsSong.scala
index 175be9add2a58ceb0a2a866e0163edb952a5143a..9a25333f51161e9fd5da91c5fbc000565256a450 100644
--- a/testcases/synthesis/NewYearsSong.scala
+++ b/testcases/synthesis/NewYearsSong.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object NewYearSong {
 
diff --git a/testcases/synthesis/PrimeHeuristic.scala.off b/testcases/synthesis/PrimeHeuristic.scala.off
index 03f5faab255b41e2b6da430710a2ef21a51a67d2..31a68993597650b3c4c6242a53150456e8a34bd9 100644
--- a/testcases/synthesis/PrimeHeuristic.scala.off
+++ b/testcases/synthesis/PrimeHeuristic.scala.off
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object PrimeHeuristic {
   def maybePrime(n: Int): Boolean = n match {
diff --git a/testcases/synthesis/ScaleWeight.scala b/testcases/synthesis/ScaleWeight.scala
index 7e1c0f2eadc11294b9301b07f8908d33dec43c03..6a47e288616fb51bfdbbcd8e4f1c4c434973ef38 100644
--- a/testcases/synthesis/ScaleWeight.scala
+++ b/testcases/synthesis/ScaleWeight.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object ScaleWeight {
 
diff --git a/testcases/synthesis/Sec2Time.scala b/testcases/synthesis/Sec2Time.scala
index 30f1cf2fe06cd21e8657907f4b7de2ad2082ec61..68e5963c540e8f20a45a824e0c3110c48a8907c6 100644
--- a/testcases/synthesis/Sec2Time.scala
+++ b/testcases/synthesis/Sec2Time.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Sec2Time {
 
diff --git a/testcases/synthesis/Simple.scala b/testcases/synthesis/Simple.scala
index 6c5fdba0f82d0fdaf83c75026028208a940497b3..c8a7e24f8561fdb894ce357657b5a3d4f0b69797 100644
--- a/testcases/synthesis/Simple.scala
+++ b/testcases/synthesis/Simple.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object SimpleSynthesis {
 
diff --git a/testcases/synthesis/SimplestCegis.scala b/testcases/synthesis/SimplestCegis.scala
index d0c5c44d8555c4e50c463df5f921762fe9242b8f..b4b574d64a6eb344f5005b8577515b16eb6f2134 100644
--- a/testcases/synthesis/SimplestCegis.scala
+++ b/testcases/synthesis/SimplestCegis.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Injection {
   sealed abstract class List
diff --git a/testcases/synthesis/SortedList.scala b/testcases/synthesis/SortedList.scala
index 9fde7d0548d1e494d419f3345d9969a5167857ed..378b182ec0c63e95a754ded0abd30c51bc7315f6 100644
--- a/testcases/synthesis/SortedList.scala
+++ b/testcases/synthesis/SortedList.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object SortedList {
   sealed abstract class List
diff --git a/testcases/synthesis/Spt.scala b/testcases/synthesis/Spt.scala
index 6fbac66487957764fbc9ab103ec80624618f1f8a..22d2457c826e60a0ba0940d21d61265b8a2bd20c 100644
--- a/testcases/synthesis/Spt.scala
+++ b/testcases/synthesis/Spt.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 // Examples taken from http://lara.epfl.ch/~psuter/spt/
 object SynthesisProceduresToolkit {
@@ -38,7 +38,7 @@ object SynthesisProceduresToolkit {
   def e6(a: Nat, b: Nat): (Nat, NatList) = if ((a == Succ(b))) {
   (Z(), Nil())
 } else {
-  leon.Utils.error[(Nat, NatList)]("Precondition failed")
+  leon.lang.error[(Nat, NatList)]("Precondition failed")
 }
 
   def e7(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = (choose { (x1: Nat, x2: NatList, x3: Nat, x4: NatList) =>
@@ -49,7 +49,7 @@ object SynthesisProceduresToolkit {
   case Succ(n150) =>
     n150
   case _ =>
-    leon.Utils.error[(Nat)]("Precondition failed")
+    leon.lang.error[(Nat)]("Precondition failed")
 })
 
   abstract class Nat
diff --git a/testcases/synthesis/Unification.scala b/testcases/synthesis/Unification.scala
index c2b111352871aa0c3435774a21321418fb8c8e6e..a73a470c3dd24db5d9f050a6a5a307da75bc5227 100644
--- a/testcases/synthesis/Unification.scala
+++ b/testcases/synthesis/Unification.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object UnificationSynthesis {
 
diff --git a/testcases/synthesis/cav2013/AVLTree.scala b/testcases/synthesis/cav2013/AVLTree.scala
index 9e40228e1c1ab9219e16843a667a7f38f57f6a4c..b5e7c1dd864a8df099cf0f8058e0c3cde01c3836 100644
--- a/testcases/synthesis/cav2013/AVLTree.scala
+++ b/testcases/synthesis/cav2013/AVLTree.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object AVLTree {
   sealed abstract class Tree
diff --git a/testcases/synthesis/cav2013/BinaryTree.scala b/testcases/synthesis/cav2013/BinaryTree.scala
index cbebc3808b24905a9d7a08d86a19bda53719dcdf..e8c1bc742f6f6ff9b3609ebb822b23a7f8e325ef 100644
--- a/testcases/synthesis/cav2013/BinaryTree.scala
+++ b/testcases/synthesis/cav2013/BinaryTree.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinaryTree {
   sealed abstract class Tree
diff --git a/testcases/synthesis/cav2013/List.scala b/testcases/synthesis/cav2013/List.scala
index b7668240194ddcca33f8e1e7b42cb9d37b176ab9..37129a90dd95f37cb1295d31d6cf639d0b9a7f6a 100644
--- a/testcases/synthesis/cav2013/List.scala
+++ b/testcases/synthesis/cav2013/List.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object List {
   sealed abstract class List
diff --git a/testcases/synthesis/cav2013/ListByExample.scala b/testcases/synthesis/cav2013/ListByExample.scala
index b1f0767749b886ede0fc48153d2d063c00301027..87737d02c7e6c7662f432c9154bdcf850d78317b 100644
--- a/testcases/synthesis/cav2013/ListByExample.scala
+++ b/testcases/synthesis/cav2013/ListByExample.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Lists {
   sealed abstract class List
diff --git a/testcases/synthesis/cav2013/ManyTimeSec.scala b/testcases/synthesis/cav2013/ManyTimeSec.scala
index 8e36f1009a22256422ef7b68e5fa1d209848b699..2589c99ea4507c691431d2d89ba341e269a99910 100644
--- a/testcases/synthesis/cav2013/ManyTimeSec.scala
+++ b/testcases/synthesis/cav2013/ManyTimeSec.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object ManyTimeSec { 
   case class Time(h:Int,m:Int,s:Int)
diff --git a/testcases/synthesis/cav2013/SortedList.scala b/testcases/synthesis/cav2013/SortedList.scala
index e07619bffef057b2b203855819a029cf61dc4318..ba9bb3802e5380e9013014c00a15fc287e10d1d7 100644
--- a/testcases/synthesis/cav2013/SortedList.scala
+++ b/testcases/synthesis/cav2013/SortedList.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object SortedList {
   sealed abstract class List
diff --git a/testcases/synthesis/cav2013/Sorting.scala b/testcases/synthesis/cav2013/Sorting.scala
index c9bee62a0344e2a53f2c7757c7615ebec73b93ad..e031995d5d9421161e867f42d9bbdb161d4af1af 100644
--- a/testcases/synthesis/cav2013/Sorting.scala
+++ b/testcases/synthesis/cav2013/Sorting.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 // Sorting lists is a fundamental problem in CS.
 object Sorting {
diff --git a/testcases/synthesis/cav2013/StrictlySortedList.scala b/testcases/synthesis/cav2013/StrictlySortedList.scala
index 9570df701bd4578b9e2d4db807adc47546b10314..efd57e78f172d629462b91ee499616f28767e80d 100644
--- a/testcases/synthesis/cav2013/StrictlySortedList.scala
+++ b/testcases/synthesis/cav2013/StrictlySortedList.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object SortedList {
   sealed abstract class List
diff --git a/testcases/synthesis/cav2013/SynAddresses.scala b/testcases/synthesis/cav2013/SynAddresses.scala
index b1fb6cf2f3b7b7ecb9f8f7a9f71bc7d3574376ce..cf33e9a7358de0a464ed6d162234326d3f9e78ab 100644
--- a/testcases/synthesis/cav2013/SynAddresses.scala
+++ b/testcases/synthesis/cav2013/SynAddresses.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   // list of integers
diff --git a/testcases/synthesis/cav2013/SynTreeListSet.scala b/testcases/synthesis/cav2013/SynTreeListSet.scala
index eae01213973d787269a98afaf00721167d4d8848..d5b4d972a2740490df16a7039d5fa64060656607 100644
--- a/testcases/synthesis/cav2013/SynTreeListSet.scala
+++ b/testcases/synthesis/cav2013/SynTreeListSet.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinaryTree {
   // list of integers
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala
index 027d90bcbc47dba08d0e4d8b5e4c55ade9fea82c..02348024d1f2de125af654d20c34ed0ef3c38b12 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   case class Info(
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala
index 579c6d4b71b0fb5b063b3cec14f19f5cbf87ab1a..9d3087669423ac567f1188ee96cb50b2c34182bf 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   case class Info(
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala
index e47b260075ca097290b0dc1489d603ff48a51223..76537952f27b729cc8bec21fe1768268167fbaf6 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   case class Info(
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala
index 98bb95f59711ab5a212a1764223601bbb5c016c5..96b1e6fd88ea937ff7d112238673956e11f8965f 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala
index 8cb51d2483552623a9d3e329634968ccbd5b993b..21fde00c582edeb128335679209c2b9db36e2ff2 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   case class Info(
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala
index e29c6dfc97fc2953b189bfd5deb58658423786e6..5235d651d517cd4ef0cecf1a2fb9ccfca89ce186 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   case class Info(
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala
index ddf3ca49b60afdb16894c93bda4d6cf4780615b5..de45e44e8befe0f3605ff910822483f751eedcda 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Addresses {
   case class Info(
diff --git a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala
index 4faa50286c879d90d3e9fe12db58856459ee8993..52e582ffb2c850f60dac404f375da2aa486f637f 100644
--- a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala
+++ b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object BatchedQueue {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala
index 1ede1397ff8e041f160b7fa9cc14fcfaa7c6f687..7dbb6bfc37072d53ffb99f65b02a8b79693c4d55 100644
--- a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala
+++ b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object BatchedQueue {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala
index 6541b33b5dbce7b126d0eeac8b46858d286fa59d..26e70e64995bdf559add3538f4cd23355d1303f6 100644
--- a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala
+++ b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object BatchedQueue {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Batch.scala b/testcases/synthesis/oopsla2013/BinaryTree/Batch.scala
index 0a2fb81ef16751781c525e6981bb3106e07362cd..093c645f28c99276a4d04c26f72509dfe63d5ff9 100644
--- a/testcases/synthesis/oopsla2013/BinaryTree/Batch.scala
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Batch.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinaryTree {
   sealed abstract class Tree
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Complete.scala b/testcases/synthesis/oopsla2013/BinaryTree/Complete.scala
index 51aebf173a3b3f07cc63a5464b80d7ea5084622c..c30bcdf788a76c58fada4053f6b8bfb91807be39 100644
--- a/testcases/synthesis/oopsla2013/BinaryTree/Complete.scala
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Complete.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinaryTree {
   sealed abstract class Tree
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Delete.scala b/testcases/synthesis/oopsla2013/BinaryTree/Delete.scala
index 219b3efab110336347c5bb879542021cc60d9159..38b85a26371d4701cdb3bddd2f40e6ed0a10acd5 100644
--- a/testcases/synthesis/oopsla2013/BinaryTree/Delete.scala
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Delete.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinaryTree {
   sealed abstract class Tree
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Diff.scala b/testcases/synthesis/oopsla2013/BinaryTree/Diff.scala
index bd31f758a75c25c58fcb26412fa1e6b191945973..450cecc28cacabac813f8c92c1a7f2385a39c897 100644
--- a/testcases/synthesis/oopsla2013/BinaryTree/Diff.scala
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Diff.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinaryTree {
   sealed abstract class Tree
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Insert.scala b/testcases/synthesis/oopsla2013/BinaryTree/Insert.scala
index 32291ad3ed0cca370b7d5abb915f82abaf2dc5d9..d0a7e50f3c0aa3ab7f3e5e3b96bb400a9f9fa8c1 100644
--- a/testcases/synthesis/oopsla2013/BinaryTree/Insert.scala
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Insert.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinaryTree {
   sealed abstract class Tree
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Union.scala b/testcases/synthesis/oopsla2013/BinaryTree/Union.scala
index c6252a2b7d8738cbf690c79fba50ebec594c82e1..776c21f0daeab2426c041436ffc772e9311d6421 100644
--- a/testcases/synthesis/oopsla2013/BinaryTree/Union.scala
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Union.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinaryTree {
   sealed abstract class Tree
diff --git a/testcases/synthesis/oopsla2013/Church/Add.scala b/testcases/synthesis/oopsla2013/Church/Add.scala
index 7b1b6b95fb9e928e031e91ac359e4f64ae1a663d..f9374897c38824193ef6167ebcdda286f35c0690 100644
--- a/testcases/synthesis/oopsla2013/Church/Add.scala
+++ b/testcases/synthesis/oopsla2013/Church/Add.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 object ChurchNumerals {
   sealed abstract class Num
   case object Z extends Num
diff --git a/testcases/synthesis/oopsla2013/Church/Batch.scala b/testcases/synthesis/oopsla2013/Church/Batch.scala
index 491166f56533c308963396e5e16a5be177a10205..4129382d212fa1d6a0fe5c6f12db12b0fbda64a7 100644
--- a/testcases/synthesis/oopsla2013/Church/Batch.scala
+++ b/testcases/synthesis/oopsla2013/Church/Batch.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 object ChurchNumerals {
   sealed abstract class Num
   case object Z extends Num
diff --git a/testcases/synthesis/oopsla2013/Church/Complete.scala b/testcases/synthesis/oopsla2013/Church/Complete.scala
index c446c789d0b5c5347fdaa817473aa005b73659c2..049bf442cd6c33eef2ffb30a88e7d4fe6e9d5cb2 100644
--- a/testcases/synthesis/oopsla2013/Church/Complete.scala
+++ b/testcases/synthesis/oopsla2013/Church/Complete.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 object ChurchNumerals {
   sealed abstract class Num
   case object Z extends Num
diff --git a/testcases/synthesis/oopsla2013/Church/Distinct.scala b/testcases/synthesis/oopsla2013/Church/Distinct.scala
index a7a0189c20070a28393bb97be7f8066f82939662..9472f04f7922f71d5819bef023b663479b13a5e6 100644
--- a/testcases/synthesis/oopsla2013/Church/Distinct.scala
+++ b/testcases/synthesis/oopsla2013/Church/Distinct.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 object ChurchNumerals {
   sealed abstract class Num
   case object Z extends Num
diff --git a/testcases/synthesis/oopsla2013/Church/Mult.scala b/testcases/synthesis/oopsla2013/Church/Mult.scala
index 42519e663c4f59cb118a47854ed98ad2bd6b22df..bb51979eaafdf4ab9a665666f2e11c6ace81cb98 100644
--- a/testcases/synthesis/oopsla2013/Church/Mult.scala
+++ b/testcases/synthesis/oopsla2013/Church/Mult.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 object ChurchNumerals {
   sealed abstract class Num
   case object Z extends Num
diff --git a/testcases/synthesis/oopsla2013/Church/Squared.scala b/testcases/synthesis/oopsla2013/Church/Squared.scala
index 096f212a617c433eaf474010dc1e203c86cfce7e..08a71c46288b4b6b0a9eb2d0763e06bc8387a763 100644
--- a/testcases/synthesis/oopsla2013/Church/Squared.scala
+++ b/testcases/synthesis/oopsla2013/Church/Squared.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 object ChurchNumerals {
   sealed abstract class Num
   case object Z extends Num
diff --git a/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala b/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala
index f741708ad50de666a76185664ddef9228e4ed56b..310b7e7e28afd45e65d5056dc784b87b36cd5744 100644
--- a/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala
+++ b/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object InsertionSort {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/InsertionSort/Insert.scala b/testcases/synthesis/oopsla2013/InsertionSort/Insert.scala
index c9402ee740fb0a48dcb16b56baf3c0bb3c984beb..a79a061330257fbaaac214f34e9073f5134329b6 100644
--- a/testcases/synthesis/oopsla2013/InsertionSort/Insert.scala
+++ b/testcases/synthesis/oopsla2013/InsertionSort/Insert.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object InsertionSort {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/InsertionSort/Sort.scala b/testcases/synthesis/oopsla2013/InsertionSort/Sort.scala
index e75c803ddf86ac9207e6a82273c49d08cc32df7d..081819ec00542ff7d5f47fc6d968d38c7c71a3bf 100644
--- a/testcases/synthesis/oopsla2013/InsertionSort/Sort.scala
+++ b/testcases/synthesis/oopsla2013/InsertionSort/Sort.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object InsertionSort {
   sealed abstract class List
@@ -49,4 +49,4 @@ object InsertionSort {
   //    case Nil() => Nil()
   //    case Cons(x, xs) => sortedIns(x, sort(xs))
 
-}
\ No newline at end of file
+}
diff --git a/testcases/synthesis/oopsla2013/List/Batch.scala b/testcases/synthesis/oopsla2013/List/Batch.scala
index f008b75755b461c01806245165a31ae8b4071347..c19c5347f8372de5f6d2d08ed4ba0f687d156de0 100644
--- a/testcases/synthesis/oopsla2013/List/Batch.scala
+++ b/testcases/synthesis/oopsla2013/List/Batch.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object List {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/List/Complete.scala b/testcases/synthesis/oopsla2013/List/Complete.scala
index 2f6d74b81a5251131684272577e4476c02647bf1..9a0a19d8460fb96accd012fd0d89daa7482a7b33 100644
--- a/testcases/synthesis/oopsla2013/List/Complete.scala
+++ b/testcases/synthesis/oopsla2013/List/Complete.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/List/Delete.scala b/testcases/synthesis/oopsla2013/List/Delete.scala
index 9fdef981b563018e52f43a49af6fd468e1395dc5..998249371a3ed370b319990662061237e7c9eb9f 100644
--- a/testcases/synthesis/oopsla2013/List/Delete.scala
+++ b/testcases/synthesis/oopsla2013/List/Delete.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Delete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/List/Diff.scala b/testcases/synthesis/oopsla2013/List/Diff.scala
index 3e7121eb18b807f746530aa6c1a165960343e1cf..a6c2c181db716f9f546c80df3c720987d2e985c4 100644
--- a/testcases/synthesis/oopsla2013/List/Diff.scala
+++ b/testcases/synthesis/oopsla2013/List/Diff.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Diff {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/List/Insert.scala b/testcases/synthesis/oopsla2013/List/Insert.scala
index e5b21b45d3fcf090c6af8bd3fa7dd40f45ef00f5..91862f1a6440df3d6dff68ab4e9b5560e922392a 100644
--- a/testcases/synthesis/oopsla2013/List/Insert.scala
+++ b/testcases/synthesis/oopsla2013/List/Insert.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Insert {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/List/Split.scala b/testcases/synthesis/oopsla2013/List/Split.scala
index 5aa4a8f1f309475a19eb466d0e871c72cab416fb..649f0b8b1e50aece88c4095baf9a4e4b215950f9 100644
--- a/testcases/synthesis/oopsla2013/List/Split.scala
+++ b/testcases/synthesis/oopsla2013/List/Split.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/List/Union.scala b/testcases/synthesis/oopsla2013/List/Union.scala
index adcc943fdabb9052c50c84f1ec58e80d8432ef99..c92d0c6c0bcba2cd53738e39e6943e4d365f45af 100644
--- a/testcases/synthesis/oopsla2013/List/Union.scala
+++ b/testcases/synthesis/oopsla2013/List/Union.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Union {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/MergeSort/Complete.scala b/testcases/synthesis/oopsla2013/MergeSort/Complete.scala
index a373e82ca551da34c8b56a4f9fe64022da66e952..062578c96d34459500eca24eeed3e008a3e9a12b 100644
--- a/testcases/synthesis/oopsla2013/MergeSort/Complete.scala
+++ b/testcases/synthesis/oopsla2013/MergeSort/Complete.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object MergeSort {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala
index 987c538c4ab36dc9b378f03fc24592210bcbd62b..e96b37543e7636a2870d25cbf967e312e41f5cd5 100644
--- a/testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala
+++ b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object MergeSort {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala
index 2cccf5c98753a362235d4fb423e2621e84de534a..8df35ea8f7c2377cb1d883416bbfcc79627c7409 100644
--- a/testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala
+++ b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
 
-import leon.Utils._
+import leon.lang._
 
 object MergeSort {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedBinaryTree/Batch.scala b/testcases/synthesis/oopsla2013/SortedBinaryTree/Batch.scala
index 3d430f65c7d418e1e32cfe9cc3e214de91d2431f..643e824211a4e880e2be00641364157443c9d37a 100644
--- a/testcases/synthesis/oopsla2013/SortedBinaryTree/Batch.scala
+++ b/testcases/synthesis/oopsla2013/SortedBinaryTree/Batch.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinaryTree {
   sealed abstract class Tree
diff --git a/testcases/synthesis/oopsla2013/SortedList/Batch.scala b/testcases/synthesis/oopsla2013/SortedList/Batch.scala
index adb1f6de92b69e8aa80c56076fa69113b82dce83..f96978e6cd5a83b616ca521c6da3f71c4e30324f 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Batch.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Batch.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object SortedList {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Complete.scala b/testcases/synthesis/oopsla2013/SortedList/Complete.scala
index ca1086c4c92a5bbbd71027cc80fe848f2f027be2..fecaa26a9d6b436bb2c121137ef64ab28144e704 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Complete.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Complete.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Delete.scala b/testcases/synthesis/oopsla2013/SortedList/Delete.scala
index c3ebd3f787f8b0a83d491017903d341431f5c1d7..e858390aa374c6da50114cb6ef0952868b1540b8 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Delete.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Delete.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Diff.scala b/testcases/synthesis/oopsla2013/SortedList/Diff.scala
index e4fa1dca9968a64e12e7e1264a3c495cca0341f9..df5427f89c4c380ce0bf34f51388f7df5e4eca3f 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Diff.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Diff.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Insert1.scala b/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
index f790fd50c074ca8b96175d30ff88d50dfeffbe98..fdd5d1d5f1667bc748ff1307e502c58cff79a4bc 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Insert2.scala b/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
index 14556e667609a3b7846400a8d9c5851be91eb5df..159ebeaf294aeb98d66cb8f5b489e3e624b9325c 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Sort.scala b/testcases/synthesis/oopsla2013/SortedList/Sort.scala
index 721ea6fa94324be438c7df7386803723c5b06e4b..bd4054c0d4eeceeb7b1487dcafd745693bd5da71 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Sort.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Sort.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/SortInsert.scala b/testcases/synthesis/oopsla2013/SortedList/SortInsert.scala
index d3bf0090d78d199001e03a2e113d5734ef1f8908..6be3478ef0591d6d82cf8b0b0281def47a036374 100644
--- a/testcases/synthesis/oopsla2013/SortedList/SortInsert.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/SortInsert.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/SortMerge.scala b/testcases/synthesis/oopsla2013/SortedList/SortMerge.scala
index bf0794fe7da0fe43d24f32bd401cec2040973f5a..8fefa5089e7f38b98d3c89689899faa5010ffca0 100644
--- a/testcases/synthesis/oopsla2013/SortedList/SortMerge.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/SortMerge.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala b/testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala
index daff218c9e334f496621dce2db05128d9338017f..d9b74a8cdaf11bdcb31d66edc1cd91ce9d5256e7 100644
--- a/testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split.scala b/testcases/synthesis/oopsla2013/SortedList/Split.scala
index 485146c3cccb22decb7341bd71107df7868d8ddb..10118f274f51b3dc64bac70e8c58bbb73bcf601f 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split1.scala b/testcases/synthesis/oopsla2013/SortedList/Split1.scala
index ef2090109ac1a0e33d3157b9013d5ca92bb431b4..6ddf97b380a0b7b6884a90edcda6fcbbd1e4aebc 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split1.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split1.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split2.scala b/testcases/synthesis/oopsla2013/SortedList/Split2.scala
index 37192748ca474c4711ac0b39b01f0ca0523ee0c0..4317e993275c02f3489595558e4a9b4a43f997c9 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split2.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split2.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split3.scala b/testcases/synthesis/oopsla2013/SortedList/Split3.scala
index f764e19e9d4fbfb6bdfb45eef0815f8b77c3d818..02d678eb3240d71fc2887803ac50a00e19f30d3d 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split3.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split3.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Union.scala b/testcases/synthesis/oopsla2013/SortedList/Union.scala
index 5d8767c31ca795cf2d7c9b3ccc79f0e4673213f1..c5b8ec1387b58c36fbb2f59128717f10fd514214 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Union.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Union.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/UnionIO.scala b/testcases/synthesis/oopsla2013/SortedList/UnionIO.scala
index ffaf5f1d14fda31062d75de13f7e7fea7f51b42c..6590525f838b81dd379359e104097624e6f62859 100644
--- a/testcases/synthesis/oopsla2013/SortedList/UnionIO.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/UnionIO.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Batch.scala b/testcases/synthesis/oopsla2013/SparseVector/Batch.scala
index 230aa7ff234d92d2d16c1ec6685b2218b1eab85e..5a0582c98a90ded5b1337ac4d8df85cd341738dd 100644
--- a/testcases/synthesis/oopsla2013/SparseVector/Batch.scala
+++ b/testcases/synthesis/oopsla2013/SparseVector/Batch.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object SparseVector {
   sealed abstract class SparseVector
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Complete.scala b/testcases/synthesis/oopsla2013/SparseVector/Complete.scala
index 21e2d277d5a64e50b93e66121e91454f75dec0fb..66be72a519492e974552fa88f0da53ba04bec9d5 100644
--- a/testcases/synthesis/oopsla2013/SparseVector/Complete.scala
+++ b/testcases/synthesis/oopsla2013/SparseVector/Complete.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object SparseVector {
   sealed abstract class SparseVector
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Delete.scala b/testcases/synthesis/oopsla2013/SparseVector/Delete.scala
index 9a9acedf2cc961d8cf41269f50de85704d9b5a94..b821b2c80cfa28982956a29c682885d0d8abc19a 100644
--- a/testcases/synthesis/oopsla2013/SparseVector/Delete.scala
+++ b/testcases/synthesis/oopsla2013/SparseVector/Delete.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object SparseVector {
   sealed abstract class SparseVector
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Get.scala b/testcases/synthesis/oopsla2013/SparseVector/Get.scala
index 1cf7a4cd2466175550c6d001be9394d845351b68..87e133dd6be56f028b3596d2995764351e372849 100644
--- a/testcases/synthesis/oopsla2013/SparseVector/Get.scala
+++ b/testcases/synthesis/oopsla2013/SparseVector/Get.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object SparseVector {
   sealed abstract class SparseVector
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Set.scala b/testcases/synthesis/oopsla2013/SparseVector/Set.scala
index f36589c39169feee5c70b42a0c42f8194fc0cac1..2699fe291a5c406f478f1997557791a92e670e3a 100644
--- a/testcases/synthesis/oopsla2013/SparseVector/Set.scala
+++ b/testcases/synthesis/oopsla2013/SparseVector/Set.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object SparseVector {
   sealed abstract class SparseVector
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala
index 0be1a7af69055152efe5155bb1af3d72cf56057b..e5f8e453606bcfc316df9ce16719406bee0e2ee1 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object StrictSortedList {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala
index c4a8096decc1f5c331b60b4e555afdf6ba16c706..07ac7201a25d665121e3cc2c9a8edd002f40e861 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
index 4b04ae60de3a718d5a83329573d2730c7e3d2cc0..b75f09401699affd9efda788b48bcdda31df60d8 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Delete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
index aa38b4ca139c7315657d0d4593673394df6c5683..cd059f68d14315be454276bcc37dc4113f14ef03 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
index cac8b1551cfe361b443668b46b2840d7defabaf2..e8d7ff7f449881205923c50fe6edacf325a5a01e 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
index c990996b415fbee85b97a01b9fc3e012f74f5f65..4d835f51afbfb1fc1fc0f09277736c59fbfd4286 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
@@ -1,5 +1,5 @@
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object Complete {
   sealed abstract class List
diff --git a/testcases/testgen/Abs.scala b/testcases/testgen/Abs.scala
index 4aa8307c8ec3da1d9ff941994b084d8590ce3afc..5d98e69490ede4eb2d2ed7ccab4f4287efe0de19 100644
--- a/testcases/testgen/Abs.scala
+++ b/testcases/testgen/Abs.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object Abs {
 
diff --git a/testcases/testgen/Abs2.scala b/testcases/testgen/Abs2.scala
index d640f941bf299ce06e0e84e40e2a2f98c39a4c4c..63d9afcb2ed9aa664811b53466475d5266c29918 100644
--- a/testcases/testgen/Abs2.scala
+++ b/testcases/testgen/Abs2.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object Abs2 {
 
diff --git a/testcases/testgen/Diamond.scala b/testcases/testgen/Diamond.scala
index dbd354e94ffe82de38d7a83997fa1553189f7c0b..bc2ddb9da5e5dd668710aeaf755c0fcef09b2ca7 100644
--- a/testcases/testgen/Diamond.scala
+++ b/testcases/testgen/Diamond.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Diamond {
 
diff --git a/testcases/testgen/Imp.scala b/testcases/testgen/Imp.scala
index 8257e6619ca299a8e56fd3d78076c54f8b731882..e3b94180174bf3ded622bae42c51f78f87f73ad8 100644
--- a/testcases/testgen/Imp.scala
+++ b/testcases/testgen/Imp.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object Imp {
 
diff --git a/testcases/testgen/ImpWaypoint.scala b/testcases/testgen/ImpWaypoint.scala
index 932d362b6faada0d8acf684d96d6bcaada0cca21..08a1eed00456650e2edc452aac13c10a6a9916a3 100644
--- a/testcases/testgen/ImpWaypoint.scala
+++ b/testcases/testgen/ImpWaypoint.scala
@@ -1,6 +1,6 @@
 
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object Imp {
 
diff --git a/testcases/testgen/List.scala b/testcases/testgen/List.scala
index b21928d924998d5dcd89ea2c278928c77aecf46a..6960157a1eec2b3adcdb46c48ae2c224f061d89a 100644
--- a/testcases/testgen/List.scala
+++ b/testcases/testgen/List.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object List {
 
diff --git a/testcases/testgen/MultiCall.scala b/testcases/testgen/MultiCall.scala
index 6742cc4ca224b8bef044745dc6cd12d60683ac80..cdbc3c18c443fedafca039ff41d9d5783411258e 100644
--- a/testcases/testgen/MultiCall.scala
+++ b/testcases/testgen/MultiCall.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object MultiCall {
 
diff --git a/testcases/testgen/Sum.scala b/testcases/testgen/Sum.scala
index 5f1c6c481f36d195f1fe6d58c591a5d91918871b..b08741e448eb2f8fa85ce868df6f6286d6ddfe94 100644
--- a/testcases/testgen/Sum.scala
+++ b/testcases/testgen/Sum.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object Sum {
 
diff --git a/testcases/vstte10competition/AmortizedQueue.scala b/testcases/vstte10competition/AmortizedQueue.scala
index fa9d8f02322ff88bc7a7db6cf5be9d30f74b30af..696d92c40592c7190bcf88ef5fe5cd80ccae80cd 100644
--- a/testcases/vstte10competition/AmortizedQueue.scala
+++ b/testcases/vstte10competition/AmortizedQueue.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object AmortizedQueue {
   sealed abstract class List
diff --git a/testcases/vstte10competition/Injection.scala b/testcases/vstte10competition/Injection.scala
index e20fdcedde55f429bb3c9718ffb2de52336dbce9..22b9d2d25c7f148b15b0f3c0e0c7a2df9a8941b0 100644
--- a/testcases/vstte10competition/Injection.scala
+++ b/testcases/vstte10competition/Injection.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object Injection {
   sealed abstract class List
diff --git a/testcases/vstte10competition/SearchLinkedList.scala b/testcases/vstte10competition/SearchLinkedList.scala
index 2c137fd4ad6b9d411f7e14b4ada6b834234c9e9e..02f265f12b1c6cf6e12c0d6fcf5df6dbb3e71558 100644
--- a/testcases/vstte10competition/SearchLinkedList.scala
+++ b/testcases/vstte10competition/SearchLinkedList.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object SearchLinkedList {
   sealed abstract class List
diff --git a/testcases/vstte10competition/SumAndMax.scala b/testcases/vstte10competition/SumAndMax.scala
index 0aa4ce7060a391d34dd047338fcd1f638054843f..a3fd5c3a50d6c56592dbd6d48b7bc90ac940d58f 100644
--- a/testcases/vstte10competition/SumAndMax.scala
+++ b/testcases/vstte10competition/SumAndMax.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object SumAndMax {
   sealed abstract class List
diff --git a/testcases/xlang/AbsArray.scala b/testcases/xlang/AbsArray.scala
index 0086891cdafc5a62987d5563695b38983de24fb4..9b00259c1405fe974a4bbf03678be32fe75020cf 100644
--- a/testcases/xlang/AbsArray.scala
+++ b/testcases/xlang/AbsArray.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object AbsArray {
 
diff --git a/testcases/xlang/AbsFun.scala b/testcases/xlang/AbsFun.scala
index 8186824b03bca673a899a8505347c09c86e43360..fe37632df68bc4ae1c164bb034902e45b18365c4 100644
--- a/testcases/xlang/AbsFun.scala
+++ b/testcases/xlang/AbsFun.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object AbsFun {
 
diff --git a/testcases/xlang/Add.scala b/testcases/xlang/Add.scala
index 5d125e3c72f29d96fdaa7176756efe11ca36b98a..a23ad05951b0240feddcf11245050410fa26640c 100644
--- a/testcases/xlang/Add.scala
+++ b/testcases/xlang/Add.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 /* VSTTE 2008 - Dafny paper */
 
diff --git a/testcases/xlang/ArrayBinarySearch.scala b/testcases/xlang/ArrayBinarySearch.scala
index 1398f9b9e4c6b31af646c0d3c5e89fafdd23dbab..cfeec91ea3400cf37364cd53266ad5d18838ddef 100644
--- a/testcases/xlang/ArrayBinarySearch.scala
+++ b/testcases/xlang/ArrayBinarySearch.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object BinarySearchFun {
 
diff --git a/testcases/xlang/ArrayBinarySearchProcedural.scala b/testcases/xlang/ArrayBinarySearchProcedural.scala
index 986ee41ae6a057065bc8520c5af010092b67b2b2..e1495e2d8bf302e29ad52f81d891ce417730717f 100644
--- a/testcases/xlang/ArrayBinarySearchProcedural.scala
+++ b/testcases/xlang/ArrayBinarySearchProcedural.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 /* VSTTE 2008 - Dafny paper */
 
diff --git a/testcases/xlang/BinaryTreeImp.scala b/testcases/xlang/BinaryTreeImp.scala
index 6db0d5ec0bde8c8c40c0fc704d1831f4b9c081e8..57542971b6c05714a62cd75c667f1891c04c22ae 100644
--- a/testcases/xlang/BinaryTreeImp.scala
+++ b/testcases/xlang/BinaryTreeImp.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object BinaryTree {
 
diff --git a/testcases/xlang/BubbleSort.scala b/testcases/xlang/BubbleSort.scala
index 3551ebf16416f68bd932adc512177edc6f2611d8..4f29a00b0ecefdc4e7a8a9757102e32281738394 100644
--- a/testcases/xlang/BubbleSort.scala
+++ b/testcases/xlang/BubbleSort.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 /* The calculus of Computation textbook */
 
diff --git a/testcases/xlang/BubbleWeakInvariant.scala b/testcases/xlang/BubbleWeakInvariant.scala
index d335cb81ffce8831f0dc1c203ab47c227d761e7f..36b88b1f30221b737e7118ea779a05b18f4dafea 100644
--- a/testcases/xlang/BubbleWeakInvariant.scala
+++ b/testcases/xlang/BubbleWeakInvariant.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 /* The calculus of Computation textbook */
 
diff --git a/testcases/xlang/InsertionSortImp.scala b/testcases/xlang/InsertionSortImp.scala
index 266905b26329d3cb3c4bd09d45a9356f805c6005..67e37a68665e6b856be711395d4c4bd16fbb71fd 100644
--- a/testcases/xlang/InsertionSortImp.scala
+++ b/testcases/xlang/InsertionSortImp.scala
@@ -1,6 +1,6 @@
 import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
+import leon.annotation._
+import leon.lang._
 
 object InsertionSort {
   sealed abstract class List
diff --git a/testcases/xlang/LinearSearch.scala b/testcases/xlang/LinearSearch.scala
index e18c4039c7d7f7418399ff16483d1b18cc6895a9..904a7c68a65ed777313eb0902dce503b2dafef7b 100644
--- a/testcases/xlang/LinearSearch.scala
+++ b/testcases/xlang/LinearSearch.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 /* The calculus of Computation textbook */
 
diff --git a/testcases/xlang/ListImp.scala b/testcases/xlang/ListImp.scala
index f3887419ecf59c6241ed530febbac6400538f6bd..620615321aca110ba25460987dc6076d0945f7ef 100644
--- a/testcases/xlang/ListImp.scala
+++ b/testcases/xlang/ListImp.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object ListImp {
 
diff --git a/testcases/xlang/MaxSum.scala b/testcases/xlang/MaxSum.scala
index ba724d255c23b782e1b4de716ccc8d50043e2059..3d414f39716f6342eb17e526de03201e39913910 100644
--- a/testcases/xlang/MaxSum.scala
+++ b/testcases/xlang/MaxSum.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 /* VSTTE 2010 challenge 1 */
 
diff --git a/testcases/xlang/Mult.scala b/testcases/xlang/Mult.scala
index 417e9e9cdc74440ccac679b2d55bac33a6381e4a..cdacdaa618f93fbfcd944daba2d61ec8074ed7a8 100644
--- a/testcases/xlang/Mult.scala
+++ b/testcases/xlang/Mult.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 /* VSTTE 2008 - Dafny paper */
 
diff --git a/testcases/xlang/NonDeterministicList.scala b/testcases/xlang/NonDeterministicList.scala
index c766956ed6a862108190880c553ebfd915133184..370198b53d6b42d4fd1d7aa8df5970b6e625528f 100644
--- a/testcases/xlang/NonDeterministicList.scala
+++ b/testcases/xlang/NonDeterministicList.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object NonDeterminism {
 
diff --git a/testcases/xlang/QuickSortImp.scala b/testcases/xlang/QuickSortImp.scala
index dd8e34b32c8262ee804e072872796050ed03d28a..6c721f532c14ac4244d900a4e3457a1148a21b12 100644
--- a/testcases/xlang/QuickSortImp.scala
+++ b/testcases/xlang/QuickSortImp.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object QuickSortImp {
 
diff --git a/testcases/xlang/buggyEpsilon.scala b/testcases/xlang/buggyEpsilon.scala
index b558511a036e9f7b216383e959978ca68de15068..ed47c0bed2702a9f35445ae16587b815e7507f7a 100644
--- a/testcases/xlang/buggyEpsilon.scala
+++ b/testcases/xlang/buggyEpsilon.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Test {
 
diff --git a/testcases/xlang/master-thesis-regis/Arithmetic.scala b/testcases/xlang/master-thesis-regis/Arithmetic.scala
index 2b90bda91805791950d4c9129196b0ebb30bb3e2..f3f10b892d1dfffd6227ff3fad1aaed2f074c474 100644
--- a/testcases/xlang/master-thesis-regis/Arithmetic.scala
+++ b/testcases/xlang/master-thesis-regis/Arithmetic.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Arithmetic {
 
diff --git a/testcases/xlang/master-thesis-regis/ArrayBubbleSort.scala b/testcases/xlang/master-thesis-regis/ArrayBubbleSort.scala
index 14595f2c6cc9424ad7bd92be5947b9aed06f3885..941244b39b7f19ac3ee1f37ebf3f7b9a0d49f30f 100644
--- a/testcases/xlang/master-thesis-regis/ArrayBubbleSort.scala
+++ b/testcases/xlang/master-thesis-regis/ArrayBubbleSort.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object ArrayBubbleSort {
   def sorted(a: Array[Int], l: Int, u: Int): Boolean = {
diff --git a/testcases/xlang/master-thesis-regis/ArrayOperations.scala b/testcases/xlang/master-thesis-regis/ArrayOperations.scala
index 91eb371faa8e550f3d85dfa17d13ba2ef3d6e101..d75d04c048c88a44722f1a6470e41df4bf8af665 100644
--- a/testcases/xlang/master-thesis-regis/ArrayOperations.scala
+++ b/testcases/xlang/master-thesis-regis/ArrayOperations.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object ArrayOperations {
 
diff --git a/testcases/xlang/master-thesis-regis/Constraints.scala b/testcases/xlang/master-thesis-regis/Constraints.scala
index c4b70ed6d8ca7ba34b0f7e6a25e10017e2f0134b..0df85e14fccc73e0fb90d0eec1c7d52e11c4d215 100644
--- a/testcases/xlang/master-thesis-regis/Constraints.scala
+++ b/testcases/xlang/master-thesis-regis/Constraints.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object Epsilon4 {
 
diff --git a/testcases/xlang/master-thesis-regis/ListOperations.scala b/testcases/xlang/master-thesis-regis/ListOperations.scala
index 4bb59c26472cfb9f07a09b6571db86cb62b18db7..5f2844fa0e5045416e763779139e8d14692ed5ca 100644
--- a/testcases/xlang/master-thesis-regis/ListOperations.scala
+++ b/testcases/xlang/master-thesis-regis/ListOperations.scala
@@ -1,5 +1,5 @@
-import leon.Utils._
-import leon.Annotations._
+import leon.lang._
+import leon.annotation._
 
 object ListOperations {
 
diff --git a/testcases/xlang/xplusone.scala b/testcases/xlang/xplusone.scala
index 94e9dfcc855a6878b21bebf9c8241243c4b2d871..baa96abcd2f29dba741b436859fc96f3e1ed1806 100644
--- a/testcases/xlang/xplusone.scala
+++ b/testcases/xlang/xplusone.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
 
 object xplusone {