diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
index 1e5e0c261124ba0cb4242d7b2abe90c647e8156d..b74b46e8960f6a4eae63382464c3410f80440893 100644
--- a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
+++ b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
@@ -4,11 +4,8 @@ package leon
 package codegen.runtime
 
 import utils._
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Expressions.{Tuple => LeonTuple, _}
+import purescala.Expressions._
 import purescala.ExprOps.valuateWithModel
-import purescala.Types._
 import purescala.Constructors._
 import solvers.TimeoutSolver
 import solvers.z3._
diff --git a/src/main/scala/leon/datagen/GrammarDataGen.scala b/src/main/scala/leon/datagen/GrammarDataGen.scala
index c483233e6324752575dfaab275c3313ece077db0..614af333bbb79452ad49cc7491e70d7a2731cf09 100644
--- a/src/main/scala/leon/datagen/GrammarDataGen.scala
+++ b/src/main/scala/leon/datagen/GrammarDataGen.scala
@@ -3,24 +3,14 @@
 package leon
 package datagen
 
-import purescala.Common._
 import purescala.Expressions._
-import purescala.Types._
-import purescala.Definitions._
-import utils.StreamUtils._
-
-import purescala.Definitions._
-import purescala.ExprOps._
 import purescala.Types.TypeTree
 import purescala.Common._
 import purescala.Constructors._
 import purescala.Extractors._
 import evaluators._
-import synthesis.utils._
 import bonsai.enumerators._
 
-import scala.collection.mutable.{Map=>MutableMap}
-
 import synthesis.utils._
 
 /** Utility functions to generate values of a given type.
diff --git a/src/main/scala/leon/frontends/scalac/SaveImports.scala b/src/main/scala/leon/frontends/scalac/SaveImports.scala
index 8edc6dc04186b0544a40370f4b5a202171c8d006..ff7b052408a1ed503ae4c775a1681652d0563d0a 100644
--- a/src/main/scala/leon/frontends/scalac/SaveImports.scala
+++ b/src/main/scala/leon/frontends/scalac/SaveImports.scala
@@ -4,10 +4,6 @@ package leon
 package frontends.scalac
 
 import scala.tools.nsc._
-import scala.tools.nsc.plugins._
-
-import purescala.Definitions.Program
-import purescala.Definitions.{ModuleDef => LeonModuleDef, _}
 import utils.{Position => LeonPosition, RangePosition => LeonRangePosition, OffsetPosition => LeonOffsetPosition}
 
 trait SaveImports extends SubComponent {
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index eeca5d984724bc784d3bdaef0d6ee79238bf0df8..b586ecdbee24329e6fc3bc52924738517bff4be0 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -5,17 +5,14 @@ package purescala
 
 import Constructors._
 import Extractors._
-
 import PrinterHelpers._
+import Common._
+import Expressions._
+import Types._
+import Definitions._
 
 /** This pretty-printer only print valid scala syntax */
 class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) extends PrettyPrinter(opts, sb) {
-  import Common._
-  import Expressions._
-  import Types._
-  import Definitions._
-
-  import java.lang.StringBuffer
 
   override def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
    
diff --git a/src/main/scala/leon/purescala/Transformer.scala b/src/main/scala/leon/purescala/Transformer.scala
index 498a9c4bfdae7c4ac87c3b2d7ff8cecaed002cbc..bddbe0325ea1f48564d095dee91dd9ed6dcdae5b 100644
--- a/src/main/scala/leon/purescala/Transformer.scala
+++ b/src/main/scala/leon/purescala/Transformer.scala
@@ -3,7 +3,7 @@
 package leon
 package purescala
 
-import purescala.Expressions._
+import purescala.Expressions.Expr
 
 trait Transformer {
   def transform(e: Expr): Expr
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index b72db6530f81f7a764998ac26e43ef652620a366..1a83522343f1c2ffd7a7f4238658e554c8725e8c 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -5,11 +5,12 @@ package purescala
 
 import scala.language.implicitConversions
 
+import Common._
+import Expressions._
+import Definitions._
+import TypeOps._
+
 object Types {
-  import Common._
-  import Expressions._
-  import Definitions._
-  import TypeOps._
 
   trait Typed {
     def getType: TypeTree
diff --git a/src/main/scala/leon/repair/RepairCostModel.scala b/src/main/scala/leon/repair/RepairCostModel.scala
index 65ba355b9dc7d29704091f3eefa665cb76070537..0d6837f1c028b0bc220394b19458ccda062a1cd7 100644
--- a/src/main/scala/leon/repair/RepairCostModel.scala
+++ b/src/main/scala/leon/repair/RepairCostModel.scala
@@ -2,8 +2,8 @@
 
 package leon
 package repair
-import synthesis._
 
+import synthesis._
 import synthesis.rules._
 import repair.rules._
 
diff --git a/src/main/scala/leon/repair/RepairPhase.scala b/src/main/scala/leon/repair/RepairPhase.scala
index 913e722c9ff067c10f87c51f7bb3b35a76f9ac3c..0b4c0d4c622ec69aca9b314b43a9149180b78cf2 100644
--- a/src/main/scala/leon/repair/RepairPhase.scala
+++ b/src/main/scala/leon/repair/RepairPhase.scala
@@ -13,8 +13,8 @@ object RepairPhase extends LeonPhase[Program, Program] {
   implicit val debugSection = utils.DebugSectionRepair
 
   def run(ctx: LeonContext)(program: Program): Program = {
-    var repairFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.FunctionsOptionDef)
-    var verifTimeoutMs: Option[Long] = ctx.findOption(SharedOptions.Timeout) map { _ * 1000 }
+    val repairFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.FunctionsOptionDef)
+    val verifTimeoutMs: Option[Long] = ctx.findOption(SharedOptions.Timeout) map { _ * 1000 }
 
     val reporter = ctx.reporter
 
diff --git a/src/main/scala/leon/repair/rules/GuidedCloser.scala b/src/main/scala/leon/repair/rules/GuidedCloser.scala
index 1fc70941acc5d83d6926af216cf6af54aa51256f..aa80a394b45422a8359b57ccb4739e8ab435f448 100644
--- a/src/main/scala/leon/repair/rules/GuidedCloser.scala
+++ b/src/main/scala/leon/repair/rules/GuidedCloser.scala
@@ -8,16 +8,12 @@ import synthesis._
 
 import leon.utils.Simplifiers
 import purescala.Expressions._
-import purescala.Definitions._
-import purescala.Common._
-import purescala.Types._
 import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
 import Witnesses._
 
-import solvers._
 import graph._
 
 case object GuidedCloser extends NormalizingRule("Guided Closer") {
diff --git a/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala b/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
index 1c51be6d587a7fa16efb6ec969519b6f7bab7cf5..cc382dd41cf0fdb74b3c077914528c40ff161c89 100644
--- a/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
+++ b/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
@@ -3,8 +3,8 @@
 package leon
 package solvers
 
-import purescala.Common._
-import purescala.Expressions._
+import purescala.Common.Identifier
+import purescala.Expressions.Expr
 
 class SimpleAssumptionSolverAPI(sf: SolverFactory[AssumptionSolver]) extends SimpleSolverAPI(sf) {
 
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 04a98e76507056f02050f72d7fdb1279ec697e12..3703464cf25e36c329203ffd39f5558825e4778b 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -3,7 +3,7 @@
 package leon
 package solvers
 
-import utils._
+import utils.DebugSectionSolver
 import purescala.Expressions.Expr
 import purescala.Common.Identifier
 
diff --git a/src/main/scala/leon/synthesis/SynthesisSettings.scala b/src/main/scala/leon/synthesis/SynthesisSettings.scala
index caacfea8ecc5a31ddd24b5c87ac73a10a5413ccc..9a52e58d68319f0c1255a67d326025a9a0321c86 100644
--- a/src/main/scala/leon/synthesis/SynthesisSettings.scala
+++ b/src/main/scala/leon/synthesis/SynthesisSettings.scala
@@ -3,7 +3,6 @@
 package leon
 package synthesis
 
-import scala.language.existentials
 import leon.purescala.Definitions.FunDef
 
 case class SynthesisSettings(
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index a482a471de050e1a17145a7ac7409dbbef8b5b0d..9dabc12332e6f805b6a69d2308c169dc9c0d92f2 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 
 import purescala.Common._
-import purescala.Definitions.{Program, FunDef, ModuleDef, DefType, ValDef}
+import purescala.Definitions._
 import purescala.ExprOps._
 import purescala.Expressions._
 import purescala.Constructors._
diff --git a/src/main/scala/leon/utils/ASCIIHelpers.scala b/src/main/scala/leon/utils/ASCIIHelpers.scala
index affd0ff09c76268a433cfcf9343ac6e6a84c1754..524d1fc04206a093af84bcf7434c353814c0bd76 100644
--- a/src/main/scala/leon/utils/ASCIIHelpers.scala
+++ b/src/main/scala/leon/utils/ASCIIHelpers.scala
@@ -28,7 +28,7 @@ object ASCIIHelpers {
 
             val cols = constraints.getOrElse(k, 1)
 
-            val size = c.vString.size
+            val size = c.vString.length
 
             constraints += k -> (cols max size)
 
@@ -67,13 +67,13 @@ object ASCIIHelpers {
     def render: String = {
       val colSizes = computeColumnSizes
 
-      val fullWidth = Math.max(colSizes.sum + colSizes.size*2, title.size + 7)
+      val fullWidth = Math.max(colSizes.sum + colSizes.size*2, title.length + 7)
 
       val sb = new StringBuffer
 
-      sb append "  ┌─"+("─"*title.size)+"─┐\n"
-      sb append "╔═╡ "+      title     +" ╞" + ("═" * (fullWidth-title.size-5)) + "╗\n"
-      sb append "║ └─"+("─"*title.size)+"─┘" + (" " * (fullWidth-title.size-5)) + "║\n"
+      sb append "  ┌─"+("─"*title.length)+"─┐\n"
+      sb append "╔═╡ "+      title     +" ╞" + ("═" * (fullWidth-title.length-5)) + "╗\n"
+      sb append "║ └─"+("─"*title.length)+"─┘" + (" " * (fullWidth-title.length-5)) + "║\n"
 
       for (r <- rows) r match {
         case Separator =>