diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 5516506dfbafa65fc6b0fc2489c469d0eac704ec..9be53d0338a539c1df6ba201c82a8433f61a1974 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -26,7 +26,7 @@ case class LeonValueOption(name: String, value: String) extends LeonOption {
     Some(value.toInt)
   } catch {
     case _ : Throwable =>
-      ctx.reporter.error("Option --%s takes an integer as value.".format(name))
+      ctx.reporter.error(s"Option --$name takes an integer as value.")
       None
   }
 
@@ -34,11 +34,11 @@ case class LeonValueOption(name: String, value: String) extends LeonOption {
     Some(value.toLong)
   } catch {
     case _ : Throwable =>
-      ctx.reporter.error("Option --%s takes a long as value.".format(name))
+      ctx.reporter.error(s"Option --$name takes a long as value.")
       None
   }
 
-  override def toString: String = "--%s=%s".format(name, value)
+  override def toString: String = s"--$name=$value"
 }
 
 sealed abstract class LeonOptionDef {
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index e8ca95a69b8d8a7e370531f28c11f2637fe22741..d39cdeca8c48db56f74b446cab086579e69a62c7 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -48,7 +48,7 @@ object Main {
     reporter.info("usage: leon [--xlang] [--termination] [--synthesis] [--help] [--debug=<N>] [..] <files>")
     reporter.info("")
     for (opt <- topLevelOptions.toSeq.sortBy(_.name)) {
-      reporter.info("%-20s %s".format(opt.usageOption, opt.usageDesc))
+      reporter.info(f"${opt.usageOption}%-20s ${opt.usageDesc}")
     }
     reporter.info("(By default, Leon verifies PureScala programs.)")
     reporter.info("")
@@ -56,17 +56,16 @@ object Main {
 
     for (c <- allComponents.toSeq.sortBy(_.name) if c.definedOptions.nonEmpty) {
       reporter.info("")
-      reporter.info("%s (%s)".format(c.name, c.description))
+      reporter.info(s"${c.name} (${c.description})")
       for(opt <- c.definedOptions.toSeq.sortBy(_.name)) {
         // there is a non-breaking space at the beginning of the string :)
-        reporter.info("%-20s %s".format(opt.usageOption, opt.usageDesc))
+        reporter.info(f"${opt.usageOption}%-20s ${opt.usageDesc}")
       }
     }
     sys.exit(1)
   }
 
   def processOptions(args: Seq[String]): LeonContext = {
-    val phases = allPhases
 
     val initReporter = new DefaultReporter(Settings())
 
diff --git a/src/main/scala/leon/Stopwatch.scala b/src/main/scala/leon/Stopwatch.scala
index 3e0e7d84d4fa66ed1bdfc16cd9ed3b75b344f313..7baeb86cefaf26235c1ecd982e1eefaa889d7965 100644
--- a/src/main/scala/leon/Stopwatch.scala
+++ b/src/main/scala/leon/Stopwatch.scala
@@ -54,18 +54,18 @@ class Stopwatch(name: String = "Stopwatch") {
   }
     
   def profile[T](block: => T): T = {
-    if (isRunning) stop
+    if (isRunning) stop()
     
     start
     val result = block    // call-by-name
-    stop
+    stop()
     
     result
   }
 
   def isRunning = beginning != 0L
 
-  override def toString = "%20s: %5d%sms".format(name, getMillis, if (isRunning) "..." else "")
+  override def toString = f"$name%20s: $getMillis%5d${if (isRunning) "..." else ""}ms"
 }
 
 object StopwatchCollections {
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 25f5fb3848a5f8a26ae879dfb02a03bd15158d92..5175737f5ab16dc82f1a6827c0ab446f0bf8f6af 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -1,6 +1,5 @@
 package leon.purescala
 
-import Common._
 import Definitions._
 import Expressions._
 
@@ -356,7 +355,7 @@ object DefOps {
     val res = p.copy(units = for (u <- p.units) yield {
       u.copy(
         modules = for (m <- u.modules) yield {
-          var newdefs = for (df <- m.defs) yield {
+          val newdefs = for (df <- m.defs) yield {
             df match {
               case `after` =>
                 found = true
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index e7dd7e202c8ae6e1cc35467497fccafc6acce4af..e503f3ac1f7a89e495442a2ede93ce67dbc6ae83 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -515,7 +515,6 @@ object Definitions {
     def postcondition = fd.postcondition.map {
       case post if typesMap.nonEmpty =>
         postCache.getOrElse(post, {
-          val nId = FreshIdentifier(id.name, translated(id.getType)).copiedFrom(id)
           val res = instantiateType(post, typesMap, paramsMap)
           postCache += (post -> res)
           res
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index fe049f5af59c74c55f417814ca8eec06517dd283..d132d4fdf858d3b924761f2fec98126ac7b9c37b 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -7,7 +7,6 @@ import Common._
 import Types._
 import Definitions._
 import Expressions._
-import TypeOps._
 import Extractors._
 import Constructors._
 import DefOps._
@@ -359,8 +358,8 @@ object ExprOps {
           case Variable(i) => subvs + i
           case LetDef(fd,_) => subvs -- fd.params.map(_.id)
           case Let(i,_,_) => subvs - i
-          case MatchLike(_, cses, _) => subvs -- (cses.map(_.pattern.binders).foldLeft(Set[Identifier]())((a, b) => a ++ b))
-          case Passes(_, _ , cses)   => subvs -- (cses.map(_.pattern.binders).foldLeft(Set[Identifier]())((a, b) => a ++ b))
+          case MatchLike(_, cses, _) => subvs -- cses.map(_.pattern.binders).foldLeft(Set[Identifier]())((a, b) => a ++ b)
+          case Passes(_, _ , cses)   => subvs -- cses.map(_.pattern.binders).foldLeft(Set[Identifier]())((a, b) => a ++ b)
           case Lambda(args, body) => subvs -- args.map(_.id)
           case Forall(args, body) => subvs -- args.map(_.id)
           case _ => subvs
@@ -425,7 +424,7 @@ object ExprOps {
       val allBinders: Set[Identifier] = cse.pattern.binders
       val subMap: Map[Identifier,Identifier] = 
         Map(allBinders.map(i => (i, FreshIdentifier(i.name, i.getType, true))).toSeq : _*)
-      val subVarMap: Map[Expr,Expr] = subMap.map(kv => (Variable(kv._1) -> Variable(kv._2)))
+      val subVarMap: Map[Expr,Expr] = subMap.map(kv => Variable(kv._1) -> Variable(kv._2))
       
       MatchCase(
         rewritePattern(cse.pattern, subMap),
@@ -455,19 +454,16 @@ object ExprOps {
   }
   
   def applyAsMatches(p : Passes, f : Expr => Expr) = {
-    import p._
-    
     f(p.asConstraint) match {
       case Equals(newOut, MatchExpr(newIn, newCases)) => {
         val filtered = newCases flatMap {
-          case MatchCase(p,g,`newOut`) => None
+          case MatchCase(p, g, `newOut`) => None
           case other => Some(other)
         }
         Passes(newIn, newOut, filtered)
       }
       case other => other
     }
-    
   }
 
   def normalizeExpression(expr: Expr) : Expr = {
@@ -535,14 +531,14 @@ object ExprOps {
         Some(replace(Map((Variable(i) -> t)), b))
 
       case letExpr @ Let(i,e,b) if isDeterministic(b) => {
-        val occurences = count {
+        val occurrences = count {
           case Variable(x) if x == i => 1
           case _ => 0
         }(b)
 
-        if(occurences == 0) {
+        if(occurrences == 0) {
           Some(b)
-        } else if(occurences == 1) {
+        } else if(occurrences == 1) {
           Some(replace(Map((Variable(i) -> e)), b))
         } else {
           None
@@ -577,7 +573,7 @@ object ExprOps {
 
       case l @ LetTuple(ids, tExpr: Terminal, body) if isDeterministic(body) =>
         val substMap : Map[Expr,Expr] = ids.map(Variable(_) : Expr).zipWithIndex.toMap.map {
-          case (v,i) => (v -> tupleSelect(tExpr, i + 1, true).copiedFrom(v))
+          case (v,i) => v -> tupleSelect(tExpr, i + 1, true).copiedFrom(v)
         }
 
         Some(replace(substMap, body))
@@ -2082,7 +2078,7 @@ object ExprOps {
           var scrutSet = Set[Expr]()
           var conditions = Map[Expr, CaseClassType]()
 
-          var matchingOn = cases.collect { case cc : CaseClassInstanceOf => cc } sortBy(cc => selectorDepth(cc.expr))
+          val matchingOn = cases.collect { case cc : CaseClassInstanceOf => cc } sortBy(cc => selectorDepth(cc.expr))
           for (CaseClassInstanceOf(cct, expr) <- matchingOn) {
             conditions += expr -> cct
 
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index a9c443c4929fc7cff8d567e343706d4beaae1c1c..0f942c85cf81e6a79014c917c616a506780cc1cd 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -8,7 +8,6 @@ import Definitions._
 import Expressions._
 import Extractors._
 import ExprOps._
-import Types._
 import Constructors._
 
 object FunctionClosure extends TransformationPhase {
@@ -51,8 +50,7 @@ object FunctionClosure extends TransformationPhase {
       val capturedConstraints: Set[Expr] = pathConstraints.toSet
 
       val freshIds: Map[Identifier, Identifier] = capturedVars.map(id => (id, id.freshen)).toMap
-      val freshVars: Map[Expr, Expr] = freshIds.map(p => (p._1.toVariable, p._2.toVariable))
-      
+
       val extraValDefOldIds: Seq[Identifier] = capturedVars.toSeq
       val extraValDefFreshIds: Seq[Identifier] = extraValDefOldIds.map(freshIds(_))
       val extraValDefs: Seq[ValDef] = extraValDefFreshIds.map(ValDef(_))
@@ -149,7 +147,6 @@ object FunctionClosure extends TransformationPhase {
         pathConstraints = pathConstraints.tail
         MatchCase(pattern, rGuard, rRhs)
       }
-      val tpe = csesRec.head.rhs.getType
       matchExpr(scrutRec, csesRec).copiedFrom(m)
     }
     case v @ Variable(id) => id2freshId.get(id) match {
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index a54084b5f089045b3941938fd3bf8759e6840f3f..a381d1257a7415150403d5666c45ca93fed7bb2e 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -33,8 +33,8 @@ object PrinterHelpers {
       val printer = ctx.printer
       val sb      = printer.sb
 
-      var strings     = sc.parts.iterator
-      var expressions = args.iterator
+      val strings     = sc.parts.iterator
+      val expressions = args.iterator
 
       var extraInd = 0
       var firstElem = true
@@ -43,7 +43,7 @@ object PrinterHelpers {
         val s = strings.next.stripMargin
 
         // Compute indentation
-        var start = s.lastIndexOf('\n')
+        val start = s.lastIndexOf('\n')
         if(start >= 0 || firstElem) {
           var i = start+1
           while(i < s.length && s(i) == ' ') {
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index 7a1299d68c29ef187bf37985a80619cdf0f1ef98..c9a180d68408e0d7f187b5e308f1e37bfe5454ba 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -66,7 +66,7 @@ class ScopeSimplifier extends Transformer {
         }
 
         var curScope = newScope
-        var newSubPatterns = for (sp <- p.subPatterns) yield {
+        val newSubPatterns = for (sp <- p.subPatterns) yield {
           val (subPattern, subScope) = trPattern(sp, curScope)
           curScope = subScope
           subPattern
@@ -85,7 +85,6 @@ class ScopeSimplifier extends Transformer {
             LiteralPattern(newBinder, lit)
         }
 
-
         (newPattern, curScope)
       }
 
diff --git a/src/main/scala/leon/purescala/SimplifierWithPaths.scala b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
index a3e1e02ec2adacf88ccfd5cdce093de65d372a43..0c417eb9764f321c74c5b717e0b617392a3a1576 100644
--- a/src/main/scala/leon/purescala/SimplifierWithPaths.scala
+++ b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
@@ -66,7 +66,7 @@ class SimplifierWithPaths(sf: SolverFactory[Solver]) extends TransformerWithPC {
     case And(es) =>
       var soFar = path
       var continue = true
-      var r = andJoin(for(e <- es if continue) yield {
+      val r = andJoin(for(e <- es if continue) yield {
         val se = rec(e, soFar)
         if(se == BooleanLiteral(false)) continue = false
         soFar = register(se, soFar)
@@ -83,7 +83,6 @@ class SimplifierWithPaths(sf: SolverFactory[Solver]) extends TransformerWithPC {
       val rs = rec(scrut, path)
 
       var stillPossible = true
-      var pcSoFar = path
 
       val conds = matchCasePathConditions(me, path)
 
@@ -123,7 +122,7 @@ class SimplifierWithPaths(sf: SolverFactory[Solver]) extends TransformerWithPC {
     case Or(es) =>
       var soFar = path
       var continue = true
-      var r = orJoin(for(e <- es if continue) yield {
+      val r = orJoin(for(e <- es if continue) yield {
         val se = rec(e, soFar)
         if(se == BooleanLiteral(true)) continue = false
         soFar = register(Not(se), soFar)
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 2fca2ea893ea15a7efa038199ad8049626a74439..0c5e2a3ac12f710de9cd1d8f55dbf7ce43758695 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -119,8 +119,6 @@ object TypeOps {
 
   def leastUpperBound(t1: TypeTree, t2: TypeTree): Option[TypeTree] = (t1,t2) match {
     case (c1: ClassType, c2: ClassType) =>
-      import scala.collection.immutable.Set
-
 
       def computeChain(ct: ClassType): List[ClassType] = ct.parent match {
         case Some(pct) =>
@@ -129,8 +127,8 @@ object TypeOps {
           List(ct)
       }
 
-      var chain1 = computeChain(c1)
-      var chain2 = computeChain(c2)
+      val chain1 = computeChain(c1)
+      val chain2 = computeChain(c2)
 
       val prefix = (chain1 zip chain2).takeWhile { case (ct1, ct2) => ct1 == ct2 }.map(_._1)
 
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 091914350a5535775d76125df07d46712e6fbe30..9e8db4719f0e9d543f2ec138c8169318f6654732 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -135,7 +135,7 @@ object Types {
       case MultisetType(t) => Some((Seq(t), ts => MultisetType(ts.head)))
       case MapType(from,to) => Some((Seq(from, to), t => MapType(t(0), t(1))))
       case FunctionType(fts, tt) => Some((tt +: fts, ts => FunctionType(ts.tail.toList, ts.head)))
-      case t => Some(Nil, fake => t)
+      case t => Some(Nil, _ => t)
     }
   }
   
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 0c2f298ee1051a7024dfa650d32935ffe1f08526..abcf13841da3017e931ce3353d7d8033938df77a 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -113,8 +113,6 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
           reporter.info(ASCIIHelpers.title("3. Synthesizing"))
           reporter.info(p)
       
-      
-          val t3    = new Timer().start
           synth.synthesize() match {
             case (search, sols) =>
               for (sol <- sols) {
@@ -214,23 +212,18 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
     val Seq(ci) = ChooseInfo.extractFromFunction(program, fd)
 
     val nci = ci.copy(pc = and(ci.pc, guide))
-    val p   = nci.problem
 
     new Synthesizer(ctx, program, nci, soptions)
   }
 
   private def focusRepair(program: Program, fd: FunDef, failingTests: List[Example]): (Expr, Expr) = {
 
-    val pre = fd.precondition.getOrElse(BooleanLiteral(true))
     val args = fd.params.map(_.id)
-    val argsWrapped = tupleWrap(args.map(_.toVariable))
 
     val spec = fd.postcondition.getOrElse(Lambda(Seq(ValDef(FreshIdentifier("res", fd.returnType, true))), BooleanLiteral(true)))
 
     val body = fd.body.get
 
-    val choose = Choose(spec)
-
     val evaluator = new DefaultEvaluator(ctx, program)
 
     // Check how an expression behaves on tests
@@ -403,7 +396,6 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
   
   private def discoverTests: VerificationResult = {
 
-    import bonsai._
     import bonsai.enumerators._
     import utils.ExpressionGrammars.ValueGrammar
 
diff --git a/src/main/scala/leon/solvers/EnumerationSolver.scala b/src/main/scala/leon/solvers/EnumerationSolver.scala
index 5f158c79fd74e1b5ecd8bd036a87eacb455d8dce..56859513929ef22d7fc1c985884f2d987ba2f607 100644
--- a/src/main/scala/leon/solvers/EnumerationSolver.scala
+++ b/src/main/scala/leon/solvers/EnumerationSolver.scala
@@ -8,13 +8,10 @@ import purescala.Common._
 import purescala.Definitions._
 import purescala.Constructors._
 import purescala.Expressions._
-import purescala.Extractors._
 import purescala.ExprOps._
-import purescala.Types._
 
 import datagen._
 
-
 class EnumerationSolver(val context: LeonContext, val program: Program) extends Solver with Interruptible with IncrementalSolver with NaiveAssumptionSolver {
   def name = "Enum"
 
diff --git a/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala b/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
index fb73f5f2918052bbbf2f02602ae59445d2c5a54e..c0331098711b86b1fe616739b11e6fbe5ee83d6e 100644
--- a/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
+++ b/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
@@ -3,14 +3,8 @@
 package leon
 package solvers
 
-import utils._
-import purescala.Common._
-import purescala.Definitions._
 import purescala.Expressions._
-import purescala.Extractors._
 import purescala.Constructors._
-import purescala.ExprOps._
-import purescala.Types._
 
 trait NaiveAssumptionSolver extends AssumptionSolver {
   self: IncrementalSolver =>
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 366f977d203a07318487dadb05586a14e2693bbe..6ab9422e8f2bd4ece1f6451f3cc92def84905247 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -4,18 +4,15 @@ package leon
 package solvers
 package smtlib
 
-import utils._
 import purescala._
 import Common._
 import Expressions._
 import Extractors._
 import Constructors._
 import Types._
-import ExprOps.simplestValue
 
 import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
 import _root_.smtlib.parser.Commands._
-import _root_.smtlib.theories._
 import _root_.smtlib.interpreters.CVC4Interpreter
 
 trait SMTLIBCVC4Target extends SMTLIBTarget {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 30c1a967c1f5b19f9d34e6ab6bd2f18f48068479..fbbacc65602604fc1fc6d99810ec5a2b405d03c2 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -5,14 +5,7 @@ package solvers
 package smtlib
 
 import utils._
-import purescala._
-import Common._
-import Expressions._
-import Extractors._
-import ExprOps._
-import Types._
-import Definitions._
-
+import purescala.Definitions.Program
 
 abstract class SMTLIBSolver(val context: LeonContext,
                             val program: Program)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 6cb34c94b9505cf45e63f691fa6e8fc62abefe9c..8a5b486c6dbda3fd52f4bc2e97e20a259fa59f67 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -250,7 +250,7 @@ trait SMTLIBTarget {
           (freshSym("content"), RawArrayType(Int32Type, base))
         ))
 
-        var cdts = dts + (at -> DataType(sym, Seq(c)))
+        val cdts = dts + (at -> DataType(sym, Seq(c)))
 
         findDependencies(base, cdts)
       } else {
@@ -411,7 +411,7 @@ trait SMTLIBTarget {
        * ===== Map operations =====
        */
       case m @ FiniteMap(elems) =>
-        val mt @ MapType(from, to) = m.getType
+        val mt @ MapType(_, to) = m.getType
         val ms = declareSort(mt)
 
         val opt = declareOptionSort(to)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 376e99b6bedc452e89eb65025986abda20e78e6e..24e435e8d4e784dc9c88ed2eebdd0231de24ccc0 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -4,7 +4,6 @@ package leon
 package solvers
 package smtlib
 
-import utils._
 import purescala._
 import Common._
 import Expressions._
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 1ee5d303d8d93d39c3857992265ecad1c8aa124c..f44ec5b1ae8e0136de826507a58b787d024b8dfb 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -4,7 +4,6 @@ package leon
 package solvers
 package templates
 
-import utils._
 import purescala.Common._
 import purescala.Expressions._
 import purescala.Extractors._
diff --git a/src/main/scala/leon/solvers/templates/TemplateInfo.scala b/src/main/scala/leon/solvers/templates/TemplateInfo.scala
index 0dce3f3246ce9530740e94bae3f36e04710c8de6..6dff30052d12bf4b2d2ae302c13525b2d5457857 100644
--- a/src/main/scala/leon/solvers/templates/TemplateInfo.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateInfo.scala
@@ -5,7 +5,6 @@ package solvers
 package templates
 
 import purescala.Definitions.TypedFunDef
-import purescala.Types.TypeTree
 
 case class TemplateCallInfo[T](tfd: TypedFunDef, args: Seq[T]) {
   override def toString = {
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index 74b453bc148c0a816949fa8c3bd14a758e2e5923..d5a5cbf49f3fc04d69d2dfd193f4de3383f317ec 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -11,8 +11,6 @@ import purescala.ExprOps._
 import purescala.Types._
 import purescala.Definitions._
 
-import evaluators._
-
 case class App[T](caller: T, tpe: TypeTree, args: Seq[T]) {
   override def toString = {
     "(" + caller + " : " + tpe + ")" + args.mkString("(", ",", ")")
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index 443b2f5ab4b84951457ee22a5f34cc4ade1f7f8c..118c1517b5e49668e1ead3feb3cec7ea22b9adba 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -4,15 +4,9 @@ package leon
 package solvers
 package templates
 
-import utils._
 import purescala.Common._
 import purescala.Expressions._
-import purescala.Extractors._
-import purescala.ExprOps._
 import purescala.Types._
-import purescala.Definitions._
-
-import evaluators._
 
 class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[T]) {
   implicit val debugSection = utils.DebugSectionSolver
@@ -220,14 +214,14 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
 
   def promoteBlocker(b: T) = {
     if (callInfo contains b) {
-      val (gen, origGen, ast, fis) = callInfo(b)
+      val (_, origGen, ast, fis) = callInfo(b)
       
       callInfo += b -> (1, origGen, ast, fis)
     }
 
     if (blockerToApp contains b) {
       val app = blockerToApp(b)
-      val (gen, origGen, _, notB, infos) = appInfo(app)
+      val (_, origGen, _, notB, infos) = appInfo(app)
 
       appInfo += app -> (1, origGen, b, notB, infos)
     }
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 529dabf2082ff31a09d1cfb2761fc29d7b0b5317..bc2571639c3d49d8475a8a89903f0f796f47cc80 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -18,7 +18,6 @@ import purescala.ExprOps._
 import purescala.Types._
 
 import scala.collection.mutable.{Map => MutableMap}
-import scala.collection.mutable.{Set => MutableSet}
 
 // This is just to factor out the things that are common in "classes that deal
 // with a Z3 instance"
@@ -198,7 +197,7 @@ trait AbstractZ3Solver
       tupleMetaDecls = Map()
       setCardDecls   = Map()
 
-      prepareSorts
+      prepareSorts()
 
       isInitialized = true
 
@@ -215,7 +214,7 @@ trait AbstractZ3Solver
   protected[leon] def mapRangeSort(toType : TypeTree) : Z3Sort = mapRangeSorts.get(toType) match {
     case Some(z3sort) => z3sort
     case None => {
-      import Z3Context.{ADTSortReference, RecursiveType, RegularSort}
+      import Z3Context.RegularSort
 
       val z3info = z3.mkADTSorts(
         Seq(
@@ -365,7 +364,6 @@ trait AbstractZ3Solver
 
   // Prepares some of the Z3 sorts, but *not* the tuple sorts; these are created on-demand.
   private def prepareSorts(): Unit = {
-    import Z3Context.{ADTSortReference, RecursiveType, RegularSort}
 
     val Seq((us, Seq(unitCons), Seq(unitTester), _)) = z3.mkADTSorts(
       Seq(
@@ -488,8 +486,6 @@ trait AbstractZ3Solver
 
     class CantTranslateException extends Exception
 
-    val varsInformula: Set[Identifier] = variablesOf(expr)
-
     var z3Vars: Map[Identifier,Z3AST] = if(initialMap.nonEmpty) {
       initialMap
     } else {
@@ -643,7 +639,6 @@ trait AbstractZ3Solver
         case tpe@MapType(fromType, toType) =>
           typeToSort(tpe) //had to add this here because the mapRangeNoneConstructors was not yet constructed...
           val fromSort = typeToSort(fromType)
-          val toSort = typeToSort(toType)
           elems.foldLeft(z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())){ case (ast, (k,v)) => z3.mkStore(ast, rec(k), mapRangeSomeConstructors(toType)(rec(v))) }
         case errorType => scala.sys.error("Unexpected type for finite map: " + (ex, errorType))
       }
@@ -791,7 +786,7 @@ trait AbstractZ3Solver
                   case None => throw new CantTranslateException(t)
                   case Some((map, elseZ3Value)) =>
                     val elseValue = rec(elseZ3Value)
-                    var valuesMap = map.map { case (k,v) =>
+                    val valuesMap = map.map { case (k,v) =>
                       val index = rec(k) match {
                         case InfiniteIntegerLiteral(index) => index.toInt
                         case IntLiteral(index) => index
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index e111891c1c41c000ee879f7601b81d8ba574b514..4829f828bffbd549ebc9e0a89501621fbb0db9c5 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -4,17 +4,13 @@ package leon
 package solvers
 package z3
 
-import leon.utils._
-
 import _root_.z3.scala._
 
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
-import purescala.Extractors._
 import purescala.Constructors._
 import purescala.ExprOps._
-import purescala.Types._
 
 import solvers.templates._
 
@@ -101,7 +97,6 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
       }).toMap
 
       val asMap = modelToMap(model, variables) ++ functionsAsMap ++ constantFunctionsAsMap
-      lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
       val evalResult = evaluator.eval(formula, asMap)
 
       evalResult match {
@@ -158,9 +153,9 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
   })
 
 
-  initZ3
+  initZ3()
 
-  val solver = z3.mkSolver
+  val solver = z3.mkSolver()
 
   private var varsInVC = List[Set[Identifier]](Set())
 
@@ -311,7 +306,8 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
         // distinction is made inside.
         case Some(false) =>
 
-          val z3Core = solver.getUnsatCore
+          //@mk this seems to be dead code
+          val z3Core = solver.getUnsatCore()
 
           def coreElemToBlocker(c: Z3AST): (Z3AST, Boolean) = {
             z3.getASTKind(c) match {
@@ -331,7 +327,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
           if (unrollUnsatCores) {
             unrollingBank.decreaseAllGenerations()
 
-            for (c <- solver.getUnsatCore) {
+            for (c <- solver.getUnsatCore()) {
               val (z3ast, pol) = coreElemToBlocker(c)
               assert(pol)
 
@@ -355,7 +351,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
             solver.push() // FIXME: remove when z3 bug is fixed
             val res2 = solver.checkAssumptions(assumptionsAsZ3 : _*)
             solver.pop()  // FIXME: remove when z3 bug is fixed
-            timer.stop
+            timer.stop()
 
             res2 match {
               case Some(false) =>
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index aeaee81e0198da2ea0067d1875198fb6a3ffe84d..782deec3c4cae8314888312bf22b5002bc161219 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -36,9 +36,9 @@ class UninterpretedZ3Solver(val context : LeonContext, val program: Program)
   )
   toggleWarningMessages(true)
 
-  initZ3
+  initZ3()
 
-  val solver = z3.mkSolver
+  val solver = z3.mkSolver()
 
   def push() {
     solver.push()
@@ -62,7 +62,7 @@ class UninterpretedZ3Solver(val context : LeonContext, val program: Program)
   }
 
   def getModel = {
-    modelToMap(solver.getModel, freeVariables)
+    modelToMap(solver.getModel(), freeVariables)
   }
 
   def getUnsatCore = {
diff --git a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
index 2532827ad21ac62cdaa1c845c82d8527c8a14faa..5c628e0e56a6816f8b9d0c01ede383b94a5a4e28 100644
--- a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
+++ b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
@@ -5,7 +5,6 @@ package solvers.z3
 
 import z3.scala._
 import purescala.Common._
-import purescala.Definitions._
 import purescala.Expressions._
 import purescala.ExprOps._
 import purescala.Types._
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index b1ce6099a2ff0895359f2c2635414116f303ab52..05fcc551a448f9733acd500c79ea5e6854f38a61 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -12,8 +12,6 @@ import purescala.Constructors._
 import purescala.Extractors._
 import evaluators._
 import utils.ExpressionGrammars.ValueGrammar
-import leon.utils.StreamUtils.cartesianProduct
-import bonsai._
 import bonsai.enumerators._
 
 class ExamplesFinder(ctx: LeonContext, program: Program) {
@@ -67,7 +65,6 @@ class ExamplesFinder(ctx: LeonContext, program: Program) {
     // Finally, we keep complete tests covering all as++xs
     val allIds  = (p.as ++ p.xs).toSet
     val insIds  = p.as.toSet
-    val outsIds = p.xs.toSet
 
     val examples = testClusters.toSeq.flatMap { t =>
       val ids = t.keySet
diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index 4a9314562068de5fcf0fadf833ce66a3c33323d7..e5ae300888a3c61591dea004da505ff4a05002c8 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/src/main/scala/leon/synthesis/LinearEquations.scala
@@ -3,7 +3,6 @@
 package leon
 package synthesis
 
-import purescala.Definitions._
 import purescala.Expressions._
 import purescala.TreeNormalizations.linearArithmeticForm
 import purescala.Types._
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index 3adc6f35183a99930d7c8a5edbd79099d77a5002..02e42f0d3c5abeb0e5594147ede380e3851976bc 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -6,12 +6,8 @@ package synthesis
 import solvers._
 import solvers.combinators.PortfolioSolverSynth
 import solvers.z3._
-
-import purescala.Expressions._
 import purescala.Definitions.{Program, FunDef}
-import purescala.Common.Identifier
 
-import java.util.concurrent.atomic.AtomicBoolean
 
 /**
  * This is global information per entire search, contains necessary information
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 0da2b6c81aa475056e036465274deeaf13c1bb87..f450c63c5713b8aa97ed2c928bc8bacb27803b21 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -126,7 +126,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
       filterInclusive(options.filterFuns.map(fdMatcher), Some(excludeByDefault _)) compose ciTofd
     }
 
-    var chooses = ChooseInfo.extractFromProgram(p).filter(fdFilter)
+    val chooses = ChooseInfo.extractFromProgram(p).filter(fdFilter)
 
     var functions = Set[FunDef]()
 
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index ee234633f3b06ffe96391a13c68580a6568cab03..f902dbe07663dcb960c52896688e68f69176eaa5 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -9,13 +9,9 @@ import purescala.ExprOps._
 import purescala.Expressions._
 import purescala.Constructors._
 import purescala.ScalaPrinter
-import purescala.Types._
 import solvers._
-import solvers.combinators._
 import solvers.z3._
 
-import java.io.File
-
 import synthesis.graph._
 
 class Synthesizer(val context : LeonContext,
@@ -74,7 +70,6 @@ class Synthesizer(val context : LeonContext,
     import verification.AnalysisPhase._
     import verification.VerificationContext
 
-    val ssol = sol.toSimplifiedExpr(context, program)
     reporter.info("Solution requires validation")
 
     val (npr, fds) = solutionToProgram(sol)
diff --git a/src/main/scala/leon/synthesis/rules/ADTInduction.scala b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
index e993c73dd3a4641a815205e3feccc3cb70ca7a51..dfac6b7a9a394a407267d473761a393709c87882 100644
--- a/src/main/scala/leon/synthesis/rules/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
@@ -4,7 +4,6 @@ package leon
 package synthesis
 package rules
 
-import solvers._
 import purescala.Common._
 import purescala.Expressions._
 import purescala.Extractors._
diff --git a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
index 2c0817ce1dbd0fe43231f8d7a5aab41aa438585e..36a37059ae1f050fa7b77ecbb500ffe056803f92 100644
--- a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
@@ -4,7 +4,6 @@ package leon
 package synthesis
 package rules
 
-import solvers._
 import purescala.Common._
 import purescala.Expressions._
 import purescala.Extractors._
diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
index 51e63ec0d879cac095e280fba4c7b146142394e6..2190e473c3e01f85fdf80c0c1c2efff3c493b764 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
@@ -32,7 +32,7 @@ abstract class BottomUpTEGISLike[T <% Typed](name: String) extends Rule(name) {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
     val ef = new ExamplesFinder(hctx.context, hctx.program)
 
-    var tests = ef.extractTests(p).collect {
+    val tests = ef.extractTests(p).collect {
       case io: InOutExample => (io.ins, io.outs)
     }
 
@@ -46,8 +46,6 @@ abstract class BottomUpTEGISLike[T <% Typed](name: String) extends Rule(name) {
           //val evaluator             = new DefaultEvaluator(sctx.context, sctx.program)
           val evaluator             = new DualEvaluator(sctx.context, sctx.program, evalParams)
 
-          val interruptManager      = sctx.context.interruptManager
-
           val grammar               = getGrammar(sctx, p)
 
           val nTests = tests.size
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index e4c2c1ad19690f445ef7c2523c37b3fad97ddf1c..19e902ad95dde7d343e1731201f5780046709c42 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -8,19 +8,13 @@ import leon.utils.SeqUtils
 import solvers._
 import solvers.z3._
 
-import verification._
 import purescala.Expressions._
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Types._
 import purescala.ExprOps._
 import purescala.DefOps._
-import purescala.TypeOps._
-import purescala.Extractors._
 import purescala.Constructors._
-import purescala.ScalaPrinter
-import purescala.PrinterOptions
-import utils.Helpers._
 
 import scala.collection.mutable.{HashMap=>MutableMap, ArrayBuffer}
 
@@ -30,7 +24,6 @@ import codegen.CodeGenParams
 
 import utils._
 
-
 abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
   case class CegisParams(
@@ -52,7 +45,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
     val ctx  = sctx.context
 
     // CEGIS Flags to activate or deactivate features
-    val useUnsatCores         = sctx.settings.cegisUseUnsatCores
+    //val useUnsatCores         = sctx.settings.cegisUseUnsatCores
     val useOptTimeout         = sctx.settings.cegisUseOptTimeout
     val useVanuatoo           = sctx.settings.cegisUseVanuatoo
     val useCETests            = sctx.settings.cegisUseCETests
@@ -150,7 +143,6 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
        * Returns all possible assignments to Bs in order to enumerate all possible programs
        */
       def allPrograms(): Traversable[Set[Identifier]] = {
-        import SeqUtils._
 
         if (allProgramsCount() > nProgramsLimit) {
            return Seq()
@@ -218,7 +210,6 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
           }
         }
 
-        val resLets = p.xs.map(defFor)
         val res = tupleWrap(p.xs.map(defFor))
 
         val substMap : Map[Expr,Expr] = bsOrdered.zipWithIndex.map {
@@ -434,7 +425,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
                   }
               }
             } finally {
-              solver.free
+              solver.free()
             }
           }
 
@@ -691,7 +682,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
               None
           }
         } finally {
-          solver.free
+          solver.free()
         }
       }
 
@@ -720,7 +711,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
               None
           }
         } finally {
-          solver.free
+          solver.free()
         }
       }
 
@@ -734,9 +725,6 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
         var result: Option[RuleApplication]   = None
         val sctx = hctx.sctx
 
-        var ass = p.as.toSet
-        var xss = p.xs.toSet
-
         val ndProgram = new NonDeterministicProgram(p)
         var unfolding = 1
         val maxUnfoldings = params.maxUnfoldings
@@ -819,8 +807,6 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
           baseExampleInputs.iterator ++ cachedInputIterator
         }
 
-        val tpe = tupleTypeWrap(p.xs.map(_.getType))
-
         try {
           do {
             var skipCESearch = false
@@ -833,7 +819,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
             }
 
             // Compute all programs that have not been excluded yet
-            var prunedPrograms: Set[Set[Identifier]] = ndProgram.allPrograms.toSet
+            var prunedPrograms: Set[Set[Identifier]] = ndProgram.allPrograms().toSet
 
             val nInitial = prunedPrograms.size
             sctx.reporter.debug("#Programs: "+nInitial)
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index 6b7e42599475f05459a72f60265957405fb4bac9..e62271a8e3c17e44a06402c5c292ff77a2580925 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -5,11 +5,9 @@ package synthesis
 package rules
 
 import purescala.Expressions._
-import purescala.Definitions._
 import purescala.Common._
 import purescala.Types._
 import purescala.ExprOps._
-import purescala.Extractors._
 import purescala.Constructors._
 
 case object DetupleInput extends NormalizingRule("Detuple In") {
diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
index d41bfb8dfb9e9c905df994ffc7c864f3fdc95abe..f4a911c50cfa8740bf799882c76a09f924a4d3fc 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
@@ -5,7 +5,6 @@ package synthesis
 package rules
 
 import purescala.Expressions._
-import purescala.Definitions._
 import purescala.Common._
 import purescala.Types._
 import purescala.Constructors._
@@ -23,7 +22,7 @@ case object DetupleOutput extends Rule("Detuple Out") {
 
       val (subOuts, outerOuts) = p.xs.map { x =>
         if (isDecomposable(x)) {
-          val ct @ CaseClassType(ccd @ CaseClassDef(name, _, _, _), tpes) = x.getType
+          val ct = x.getType.asInstanceOf[CaseClassType]
 
           val newIds = ct.fields.map{ vd => FreshIdentifier(vd.id.name, vd.getType, true) }
 
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 17792cad82e6fbe62af2ec1864318b238305615c..c2ca60a31747d5a3ce2c8147a021050bff90d300 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -16,8 +16,6 @@ case object Ground extends Rule("Ground") {
         def apply(hctx: SearchContext): RuleApplication = {
           val solver = SimpleSolverAPI(new TimeoutSolverFactory(hctx.sctx.solverFactory, 10000L))
 
-          val tpe = tupleTypeWrap(p.xs.map(_.getType))
-
           val result = solver.solveSAT(p.phi) match {
             case (Some(true), model) =>
               val sol = Solution(BooleanLiteral(true), Set(), tupleWrap(p.xs.map(valuateWithModel(model))))
diff --git a/src/main/scala/leon/synthesis/rules/IntInduction.scala b/src/main/scala/leon/synthesis/rules/IntInduction.scala
index 216ce8ad769329382122e9975144c141a6697f2e..e0ab4d87668669d8d90f62ec48a6c186292da0bf 100644
--- a/src/main/scala/leon/synthesis/rules/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/IntInduction.scala
@@ -8,7 +8,6 @@ import purescala.Common._
 import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.ExprOps._
 import purescala.Types._
 import purescala.Definitions._
 
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index 478d3fbd2562be62f5ba00552118ed4f5566a6c0..251534646dae760ab1ca081f077d97d73ab3728c 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -11,7 +11,6 @@ import purescala.Constructors._
 import purescala.ExprOps._
 import purescala.TreeNormalizations._
 import purescala.Types._
-import purescala.Definitions._
 import LinearEquations.elimVariable
 import evaluators._
 
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 3430bf8ab6ab718674682070c809f19d6d366f41..23d7f5197abddf3827dbe7692e8a9fef9fd6b1be 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -13,14 +13,12 @@ import purescala.TreeNormalizations.NonLinearExpressionException
 import purescala.Types._
 import purescala.Constructors._
 import purescala.Definitions._
-import LinearEquations.elimVariable
 import leon.synthesis.Algebra.lcm
 
 case object IntegerInequalities extends Rule("Integer Inequalities") {
   def instantiateOn(implicit hctx: SearchContext, problem: Problem): Traversable[RuleInstantiation] = {
     val TopLevelAnds(exprs) = problem.phi
 
-
     //assume that we only have inequalities
     var lhsSides: List[Expr] = Nil
     var exprNotUsed: List[Expr] = Nil
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 56cc85223b56e472906857526caf88ab359807d8..e8d680c07480e0c4131d87eac6e2f6d5d97909c7 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -21,10 +21,8 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
           val xss = p.xs.toSet
           val ass = p.as.toSet
 
-          val tpe = tupleTypeWrap(p.xs.map(_.getType))
-
           var i = 0
-          var maxTries = 3
+          val maxTries = 3
 
           var result: Option[RuleApplication] = None
           var continue                        = true
@@ -35,7 +33,6 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
             //println("SOLVING " + phi + " ...")
             solver.solveSAT(phi) match {
               case (Some(true), satModel) =>
-                val satXsModel = satModel.filterKeys(xss) 
 
                 val newPhi = valuateWithModelIn(phi, xss, satModel)
 
diff --git a/src/main/scala/leon/synthesis/rules/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
index 78fbd8a5b0f4397736501a0cf73e1bded31e49cf..c33886a0344cc43df7575cddb6251594e190b72a 100644
--- a/src/main/scala/leon/synthesis/rules/TEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
@@ -41,8 +41,6 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
           val evalParams            = CodeGenParams(maxFunctionInvocations = 2000, checkContracts = true)
           val evaluator             = new DualEvaluator(sctx.context, sctx.program, evalParams)
 
-          val interruptManager      = sctx.context.interruptManager
-
           val enum = new MemoizedEnumerator[T, Expr](grammar.getProductions)
 
           val targetType = tupleTypeWrap(p.xs.map(_.getType))
@@ -64,20 +62,18 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
 
               sctx.reporter.debug("Got expression "+e)
               timers.testing.start()
-              if (tests.forall{ case t =>
-                  val ts = System.currentTimeMillis
-                  val res = evaluator.eval(exprToTest, p.as.zip(t).toMap) match {
-                    case EvaluationResults.Successful(BooleanLiteral(true)) =>
-                      sctx.reporter.debug("Test "+t+" passed!")
-                      true
-                    case _ =>
-                      sctx.reporter.debug("Test "+t+" failed on "+e)
-                      failStat += t -> (failStat(t) + 1)
-                      false
-                  }
-                  res
-                }) {
-
+              if (tests.forall{ t =>
+                val res = evaluator.eval(exprToTest, p.as.zip(t).toMap) match {
+                  case EvaluationResults.Successful(BooleanLiteral(true)) =>
+                    sctx.reporter.debug("Test "+t+" passed!")
+                    true
+                  case _ =>
+                    sctx.reporter.debug("Test "+t+" failed on "+e)
+                    failStat += t -> (failStat(t) + 1)
+                    false
+                }
+                res
+              }) {
                 candidate = Some(tupleWrap(Seq(e)))
               }
               timers.testing.stop()
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index 3718972884807ded519442067f963be40eedd787..1ba461dc00b5b924b2c345332e716b49c6f208c5 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -6,9 +6,7 @@ package termination
 import leon.purescala.Definitions._
 import leon.purescala.Expressions._
 import leon.purescala.ExprOps._
-import leon.purescala.Types._
 import leon.purescala.Constructors._
-import leon.purescala.TypeOps._
 import leon.purescala.Common._
 
 import scala.collection.mutable.{Map => MutableMap}
@@ -57,7 +55,7 @@ final case class Chain(relations: List[Relation]) {
         (e: Expr) => replace(map, funDef.translated(e))
       }
 
-      val Relation(_, path, fi @ FunctionInvocation(fitfd, args), _) = relations.head
+      val Relation(_, path, FunctionInvocation(fitfd, args), _) = relations.head
       val tfd = TypedFunDef(fitfd.fd, fitfd.tps.map(funDef.translated))
 
       lazy val newArgs = args.map(translate)
@@ -127,7 +125,7 @@ trait ChainBuilder extends RelationBuilder { self: TerminationChecker with Stren
 
       def decreasing(relations: List[Relation]): Boolean = {
         val constraints = relations.map(relation => relationConstraints.getOrElse(relation, {
-          val Relation(funDef, path, FunctionInvocation(fd, args), _) = relation
+          val Relation(funDef, path, FunctionInvocation(_, args), _) = relation
           val (e1, e2) = (tupleWrap(funDef.params.map(_.toVariable)), tupleWrap(args))
           val constraint = if (solver.definitiveALL(implies(andJoin(path), self.softDecreasing(e1, e2)))) {
             if (solver.definitiveALL(implies(andJoin(path), self.sizeDecreasing(e1, e2)))) {
@@ -147,7 +145,7 @@ trait ChainBuilder extends RelationBuilder { self: TerminationChecker with Stren
       }
 
       def chains(seen: Set[FunDef], chain: List[Relation]) : (Set[FunDef], Set[Chain]) = {
-        val Relation(_, _, FunctionInvocation(tfd, _), _) :: xs = chain
+        val Relation(_, _, FunctionInvocation(tfd, _), _) :: _ = chain
         val fd = tfd.fd
 
         if (!self.program.callGraph.transitivelyCalls(fd, funDef)) {
diff --git a/src/main/scala/leon/termination/ChainComparator.scala b/src/main/scala/leon/termination/ChainComparator.scala
index 5f923fb0a5845f419ba6c6342c1c8d6c1039266c..bcaa86c4e9c9ea501893871eb1b38d02fe21e37f 100644
--- a/src/main/scala/leon/termination/ChainComparator.scala
+++ b/src/main/scala/leon/termination/ChainComparator.scala
@@ -7,7 +7,6 @@ import purescala.Expressions._
 import purescala.ExprOps._
 import purescala.Types._
 import purescala.TypeOps._
-import purescala.Definitions._
 import purescala.Constructors._
 import purescala.Common._
 
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index 3bb3e17a096d616050e05b11c3286d49921d43d6..3f1c0b43718cb88018909ac44d992a231f82f78c 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -4,15 +4,10 @@ package leon
 package termination
 
 import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Types._
 import purescala.Common._
-import purescala.Extractors._
 import purescala.Definitions._
 import purescala.Constructors.tupleWrap
 
-import scala.collection.mutable.{Map => MutableMap}
-
 class ChainProcessor(val checker: TerminationChecker with ChainBuilder with ChainComparator with Strengthener with StructuralSize) extends Processor with Solvable {
 
   val name: String = "Chain Processor"
diff --git a/src/main/scala/leon/termination/LoopProcessor.scala b/src/main/scala/leon/termination/LoopProcessor.scala
index 4765a73c4daabe09010d12927563ea5d7106703c..3fedb900da115189b896054a483f78d31cc45653 100644
--- a/src/main/scala/leon/termination/LoopProcessor.scala
+++ b/src/main/scala/leon/termination/LoopProcessor.scala
@@ -6,7 +6,6 @@ package termination
 import purescala.Definitions._
 import purescala.Common._
 import purescala.Expressions._
-import purescala.ExprOps._
 import purescala.Constructors._
 
 import scala.collection.mutable.{Map => MutableMap}
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index 42cc27a2a89df581db500e635d895f981608ffa6..55a820841f0b62e0b45e6e94b217880120833ce5 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -4,7 +4,6 @@ package leon
 package termination
 
 import purescala.Expressions._
-import purescala.ExprOps._
 import purescala.Common._
 import purescala.Definitions._
 
@@ -37,7 +36,6 @@ trait Solvable extends Processor {
   val checker : TerminationChecker with Strengthener with StructuralSize
 
   private val solver: SolverFactory[Solver] = SolverFactory(() => {
-    val structDefs = checker.defs
     val program     : Program     = checker.program
     val context     : LeonContext = checker.context
     val sizeModule  : ModuleDef   = ModuleDef(FreshIdentifier("$size"), checker.defs.toSeq, false)
@@ -115,9 +113,9 @@ class ProcessingPipeline(program: Program, context: LeonContext, _processors: Pr
     val sb = new StringBuilder()
     sb.append("- Processing Result:\n")
     for(result <- results) result match {
-      case Cleared(fd) => sb.append("    %-10s %s\n".format(fd.id, "Cleared"))
-      case Broken(fd, args) => sb.append("    %-10s %s\n".format(fd.id, "Broken for arguments: " + args.mkString("(", ",", ")")))
-      case MaybeBroken(fd, args) => sb.append("    %-10s %s\n".format(fd.id, "HO construct application breaks for arguments: " + args.mkString("(", ",", ")")))
+      case Cleared(fd) => sb.append(f"    ${fd.id}%-10s Cleared\n")
+      case Broken(fd, args) => sb.append(f"    ${fd.id}%-10s ${"Broken for arguments: " + args.mkString("(", ",", ")")}\n")
+      case MaybeBroken(fd, args) => sb.append(f"    ${fd.id}%-10s ${"HO construct application breaks for arguments: " + args.mkString("(", ",", ")")}\n")
     }
     reporter.debug(sb.toString)
   }
@@ -138,7 +136,7 @@ class ProcessingPipeline(program: Program, context: LeonContext, _processors: Pr
 
     def hasNext : Boolean      = problems.nonEmpty
     def next()  : (String, List[Result]) = {
-      printQueue
+      printQueue()
       val (problem, index) = problems.head
       val processor : Processor = processors(index)
       reporter.debug("Running " + processor.name)
diff --git a/src/main/scala/leon/termination/SimpleTerminationChecker.scala b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
index 6ba21e23f9bcb8dc69ca973a83d0d1f634eac187..68e40730e4684f6be296fee144e5a88e61c3e9d9 100644
--- a/src/main/scala/leon/termination/SimpleTerminationChecker.scala
+++ b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
@@ -34,8 +34,6 @@ class SimpleTerminationChecker(context: LeonContext, program: Program) extends T
     i -> dsts
   }).toMap
 
-  private def callees(funDef: FunDef): Set[FunDef] = callGraph.getOrElse(funDef, Set.empty)
-
   private val answerCache = MutableMap.empty[FunDef, TerminationGuarantee]
 
   def initialize() {}
diff --git a/src/main/scala/leon/termination/Strengthener.scala b/src/main/scala/leon/termination/Strengthener.scala
index d0c8bf1641d94fa35f041309202b97a11a1ad191..7ab70ee6e4c2b0a0bbf7a2f63133a5777d008099 100644
--- a/src/main/scala/leon/termination/Strengthener.scala
+++ b/src/main/scala/leon/termination/Strengthener.scala
@@ -25,7 +25,6 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
         val postcondition = {
           val res = FreshIdentifier("res", funDef.returnType, true)
           val post = old.map{application(_, Seq(Variable(res)))}.getOrElse(BooleanLiteral(true))
-          val args = funDef.params.map(_.toVariable)
           val sizePost = cmp(tupleWrap(funDef.params.map(_.toVariable)), res.toVariable)
           Lambda(Seq(ValDef(res)), and(post, sizePost))
         }
diff --git a/src/main/scala/leon/termination/TerminationReport.scala b/src/main/scala/leon/termination/TerminationReport.scala
index 5acdef237ae770da8a942b18a9125e94b18b32fc..e08d3d861bc5679439cf6083698762d2c53e21c2 100644
--- a/src/main/scala/leon/termination/TerminationReport.scala
+++ b/src/main/scala/leon/termination/TerminationReport.scala
@@ -22,19 +22,20 @@ case class TerminationReport(results : Seq[(FunDef,TerminationGuarantee)], time
           "Terminates (" + reason + ")"
         case _ => g.toString
       }
-      sb.append("- %-30s %s %-30s\n".format(fd.id.name, result, toPrint))
+      sb.append(f"- ${fd.id.name}%-30s $result $toPrint%-30s\n")
     }
-    sb.append("\n[Analysis time: %7.3f]\n".format(time))
+    sb.append(f"\n[Analysis time: $time%7.3f]\n")
     sb.toString
   }
 
   def evaluationString : String = {
     val sb = new StringBuilder
     for((fd,g) <- results) {
-      sb.append("- %-30s %s\n".format(fd.id.name, g match {
+      val guar = g match {
         case NoGuarantee => "u"
         case t => if (t.isGuaranteed) "t" else "n"
-      }))
+      }
+      sb.append(f"- ${fd.id.name}%-30s $guar\n")
     }
     sb.toString
   }
diff --git a/src/main/scala/leon/utils/StreamUtils.scala b/src/main/scala/leon/utils/StreamUtils.scala
index 8e1caa684f7516faca0fa16d1a541725bd09aa2b..73114c1f2f66f528ef98389264afc4237643939c 100644
--- a/src/main/scala/leon/utils/StreamUtils.scala
+++ b/src/main/scala/leon/utils/StreamUtils.scala
@@ -53,7 +53,7 @@ object StreamUtils {
       var tuple : List[T] = Nil
 
       while(continue && d < dimensions) {
-        var i = is.head
+        val i = is.head
         if(bounds(d).exists(i > _)) {
           continue = false
         } else try {
diff --git a/src/main/scala/leon/utils/TimeoutFor.scala b/src/main/scala/leon/utils/TimeoutFor.scala
index fad71ac27e54e5f29cf29c1d3d6873273c65caf9..171d6d439bcee602300af625e5bc7e68b71e11a5 100644
--- a/src/main/scala/leon/utils/TimeoutFor.scala
+++ b/src/main/scala/leon/utils/TimeoutFor.scala
@@ -35,7 +35,7 @@ class TimeoutFor(it: Interruptible) {
 
     timer.start()
     val res = body
-    timer.finishedRunning
+    timer.finishedRunning()
 
     if (reachedTimeout) {
       it.recoverInterrupt()
diff --git a/src/main/scala/leon/utils/Timer.scala b/src/main/scala/leon/utils/Timer.scala
index cc8b07a41108168483326871e13cc6b2caee2af1..a0984dc752cee7865d24a50c9e50aea12eefd5ea 100644
--- a/src/main/scala/leon/utils/Timer.scala
+++ b/src/main/scala/leon/utils/Timer.scala
@@ -44,11 +44,11 @@ class Timer() {
       val min = runs.min
       val max = runs.max
 
-      "(min: %3d, avg: %3d, max: %3d, n: %3d) %6d ms".format(min, tot/n, max, n, tot)
+      f"(min: $min%3d, avg: ${tot / n}%3d, max: $max%3d, n: $n%3d) $tot%6d ms"
     } else {
       val tot = runs.sum
 
-      "%6d ms".format(tot)
+      f"$tot%6d ms"
     }
   }
 }
@@ -88,7 +88,7 @@ class TimerStorage extends Dynamic {
   def timed[T](b: => T): T = {
     start()
     val res = b
-    stop
+    stop()
     res
   }
 
diff --git a/src/main/scala/leon/utils/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
index 660f6e12324c06109f8728818978c2d08128ad2c..fe98cd488d79636ef90fa6caf612365f808bcd6f 100644
--- a/src/main/scala/leon/utils/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -6,7 +6,6 @@ package utils
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
-import xlang.Trees._
 import purescala.Extractors._
 import purescala.Constructors._
 import purescala.Types._
@@ -133,7 +132,6 @@ object UnitElimination extends TransformationPhase {
         val csesRec = cses.map{ cse =>
           MatchCase(cse.pattern, cse.optGuard map removeUnit, removeUnit(cse.rhs))
         }
-        val tpe = csesRec.head.rhs.getType
         matchExpr(scrutRec, csesRec).setPos(m)
       }
       case _ => sys.error("not supported: " + expr)
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 143f6a5cd48aaaa96f4ca71c78d852d99f101c95..e0d97b931548aea887079489260d529b316db527 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -7,15 +7,8 @@ import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.ExprOps._
-import purescala.Types._
 
 import solvers._
-import solvers.z3._
-import solvers.combinators._
-
-import scala.collection.mutable.{Set => MutableSet}
-
-import _root_.smtlib.interpreters.Z3Interpreter
 
 object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
   val name = "Analysis"
@@ -80,9 +73,6 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
   ) : VerificationReport = {
     import vctx.reporter
     import vctx.solverFactory
-    import vctx.program
-
-    import utils.ASCIIHelpers.subTitle
     
     val interruptManager = vctx.context.interruptManager
 
@@ -92,8 +82,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
 
       // Check if vc targets abstract methods
       val targets = functionCallsOf(vc).map(_.tfd.fd)
-      val callsAbstract = (vctx.program.callGraph.transitiveCallees(targets) ++ targets).exists(_.annotations("abstract"))
-    
+
       val s = solverFactory.getNewSolver
       try {
         
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 6ba584014fc813ce12b05b1147eaa1667ea113f8..06b35faddb3beb47ca35542a175bb1bfd72a87e1 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -8,8 +8,6 @@ import purescala.ExprOps._
 import purescala.Definitions._
 import purescala.Constructors._
 
-import scala.collection.mutable.{Map => MutableMap}
-
 class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
     val description = "Default verification condition generation approach"
     override val shortDescription = "default"
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index b68abfa480731ee12dc7436f22ac6c4f1ba8f3af..4420428a78c00893ba33881ff8f4783bd66e208b 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -3,7 +3,6 @@
 package leon
 package verification
 
-import purescala.Common._
 import purescala.Expressions._
 import purescala.ExprOps._
 import purescala.Types._
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index f0bb893ae670952d81f50a975e8778c05ccf2b03..e174830946f07b16113f62bb37ac6a6a2872f275 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -5,7 +5,7 @@ package leon.verification
 import leon.purescala.Expressions._
 import leon.purescala.Definitions._
 import leon.purescala.Common._
-import leon.utils.{Position, Positioned}
+import leon.utils.Positioned
 
 import leon.solvers._
 
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 219acc60141cc5da8fc37904c2ee61178600260e..5622b4e44bc3d297731f2d3c9490e0bc6fa91ae6 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -3,14 +3,11 @@
 package leon
 package xlang
 
-import leon.TransformationPhase
-import leon.LeonContext
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Expressions._
 import leon.purescala.Extractors._
 import leon.purescala.Constructors._
-import leon.purescala.Types._
 import leon.purescala.ExprOps._
 import leon.purescala.TypeOps._
 import leon.xlang.Trees._
@@ -228,7 +225,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
         //Recall that here the nested function should not access mutable variables from an outside scope
         val newFd = fd.body match {
           case Some(b) =>
-            val (fdRes, fdScope, fdFun) = toFunction(b)
+            val (fdRes, fdScope, _) = toFunction(b)
             fd.body = Some(fdScope(fdRes))
             fd
           case None =>
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 226e69c03423eaf0c49fc33e65dfaa1b3197edb3..095340622137be9d19d98468530fe58cf88fd0ab 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -13,11 +13,6 @@ import utils._
 object Trees {
   import purescala.PrinterHelpers._
 
-  private def ind(sb: StringBuffer, lvl: Int) : StringBuffer = {
-    sb.append("  " * lvl)
-    sb
-  }
-
   case class Block(exprs: Seq[Expr], last: Expr) extends Expr with NAryExtractable with PrettyPrintable {
     def extract: Option[(Seq[Expr], (Seq[Expr])=>Expr)] = {
       Some((exprs :+ last, exprs => Block(exprs.init, exprs.last)))
diff --git a/src/test/scala/leon/test/codegen/CodeGenTests.scala b/src/test/scala/leon/test/codegen/CodeGenTests.scala
index ac17f0bda060483ac3a48693ce418f1e4cb025d9..39f8563cf9045c6947c958f2c0e3142455cd74f8 100644
--- a/src/test/scala/leon/test/codegen/CodeGenTests.scala
+++ b/src/test/scala/leon/test/codegen/CodeGenTests.scala
@@ -10,8 +10,6 @@ import leon.purescala.Types._
 import leon.evaluators.{CodeGenEvaluator,EvaluationResults}
 import EvaluationResults._
 
-import java.io._
-
 /*
  * To add a new test:
  * - Add your test, preferably in a new module, in the test variable
diff --git a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
index 9f3c7969fb79b641f9945a2a6e1b8afcc12cc352..bb4bcea9f5ba3c73eb06c0e84ec77f93970128f3 100644
--- a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
+++ b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
@@ -3,15 +3,10 @@
 package leon.test.evaluators
 
 import leon._
-import leon.evaluators._ 
-
-import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
-import leon.frontends.scalac.ExtractionPhase
-
+import leon.evaluators._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Expressions._
-import leon.purescala.DefOps._
 import leon.purescala.Types._
 import leon.purescala.Constructors._
 
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 2642dba5cbd5787bc6c4b6e4ac73a6d2f2374611..60d251dd641586617cee48c02053a1c2b51af17e 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -8,7 +8,6 @@ import leon.evaluators._
 import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
 import leon.frontends.scalac.ExtractionPhase
 
-import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Expressions._
 import leon.purescala.DefOps._
@@ -30,7 +29,6 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
     val pipeline = TemporaryInputPhase andThen ExtractionPhase andThen PreprocessingPhase
 
     val errorsBefore   = leonContext.reporter.errorCount
-    val warningsBefore = leonContext.reporter.warningCount
 
     val program = pipeline.run(leonContext)((str, Nil))
 
@@ -46,7 +44,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
       case Some(fd: FunDef) =>
         FunctionInvocation(fd.typed, args.toSeq)
       case _ =>
-        throw new AssertionError("No function named '%s' defined in program.".format(fn))
+        throw new AssertionError(s"No function named '$fn' defined in program.")
     }
   }
 
@@ -55,7 +53,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
       case Some(ccd: CaseClassDef) =>
         CaseClass(CaseClassType(ccd, Nil), args.toSeq)
       case _ =>
-        throw new AssertionError("No case class named '%s' defined in program.".format(name))
+        throw new AssertionError(s"No case class named '$name' defined in program.")
     }
   }
 
@@ -64,10 +62,10 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
 
     evaluator.eval(in) match {
       case RuntimeError(msg) =>
-        throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have succeeded, but it failed (%s).".format(in, evaluator.name, msg))
+        throw new AssertionError(s"Evaluation of '$in' with evaluator '${evaluator.name}' should have succeeded, but it failed ($msg).")
 
       case EvaluatorError(msg) =>
-        throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have succeeded, but the evaluator had an internal error (%s).".format(in, evaluator.name, msg))
+        throw new AssertionError(s"Evaluation of '$in' with evaluator '${evaluator.name}' should have succeeded, but the evaluator had an internal error ($msg).")
 
       case Successful(result) =>
         result
@@ -77,7 +75,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
   private def checkComp(evaluator : Evaluator, in : Expr, out : Expr) {
     val result = checkCompSuccess(evaluator, in)
     if(result != out)
-      throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have produced '%s' but produced '%s' instead.".format(in, evaluator.name, out, result))
+      throw new AssertionError(s"Evaluation of '$in' with evaluator '${evaluator.name}' should have produced '$out' but produced '$result' instead.")
   }
 
   private def checkSetComp(evaluator : Evaluator, in : Expr, out : Set[Int]) {
@@ -101,7 +99,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
         ;
 
       case _ =>
-        throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have produced a set '%s', but it produced '%s' instead.".format(in, evaluator.name, out, result))
+        throw new AssertionError(s"Evaluation of '$in' with evaluator '${evaluator.name}' should have produced a set '$out', but it produced '$result' instead.")
     }
   }
 
@@ -126,7 +124,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
         ;
 
       case _ =>
-        throw new AssertionError("Evaluation of '%s' with evaluator '%s' should produced a map '%s', but it produced '%s' instead.".format(in, evaluator.name, out, result))
+        throw new AssertionError(s"Evaluation of '$in' with evaluator '${evaluator.name}' should produced a map '$out', but it produced '$result' instead.")
     }
   }
 
@@ -135,10 +133,10 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
 
     evaluator.eval(in) match {
       case EvaluatorError(msg) =>
-        throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have failed, but it produced an internal error (%s).".format(in, evaluator.name, msg))
+        throw new AssertionError(s"Evaluation of '$in' with evaluator '${evaluator.name}' should have failed, but it produced an internal error ($msg).")
 
       case Successful(result) =>
-        throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have failed, but it produced the result '%s' instead.".format(in, evaluator.name, result))
+        throw new AssertionError(s"Evaluation of '$in' with evaluator '${evaluator.name}' should have failed, but it produced the result '$result' instead.")
 
       case RuntimeError(_) =>
         // that's the desired outcome
@@ -150,10 +148,10 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
 
     evaluator.eval(in) match {
       case RuntimeError(msg) =>
-        throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have produced an internal error, but it failed instead (%s).".format(in, evaluator.name, msg))
+        throw new AssertionError(s"Evaluation of '$in' with evaluator '${evaluator.name}' should have produced an internal error, but it failed instead ($msg).")
 
       case Successful(result) =>
-        throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have produced an internal error, but it produced the result '%s' instead.".format(in, evaluator.name, result))
+        throw new AssertionError(s"Evaluation of '$in' with evaluator '${evaluator.name}' should have produced an internal error, but it produced the result '$result' instead.")
 
       case EvaluatorError(_) =>
         // that's the desired outcome
@@ -284,7 +282,6 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
     val cons12a = mkCaseClass("Cons", IL(1), mkCaseClass("Cons", IL(2), mkCaseClass("Nil")))
     val cons12b = mkCaseClass("Cons", IL(1), mkCaseClass("Cons", IL(2), mkCaseClass("Nil")))
     val sing1 = mkCaseClass("MySingleton", IL(1))
-    val sing2 = mkCaseClass("MySingleton", IL(2))
 
     for(e <- evaluators) {
       checkComp(e, mkCall("size", nil), IL(0))
@@ -324,7 +321,6 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
     val nil = mkCaseClass("Nil")
     val cons12 = mkCaseClass("Cons", IL(1), mkCaseClass("Cons", IL(2), mkCaseClass("Nil")))
 
-    val semp = EmptySet(Int32Type)
     val s123 = NonemptySet(Set(IL(1), IL(2), IL(3)))
     val s246 = NonemptySet(Set(IL(2), IL(4), IL(6)))
 
diff --git a/src/test/scala/leon/test/frontends/ImportsTests.scala b/src/test/scala/leon/test/frontends/ImportsTests.scala
index 01645c5a99f8352eb448429286109e5ebe8e2bc2..4cee3a326d5e8c8a4fca7bfdd394d23022a9b166 100644
--- a/src/test/scala/leon/test/frontends/ImportsTests.scala
+++ b/src/test/scala/leon/test/frontends/ImportsTests.scala
@@ -36,6 +36,7 @@ class ImportsTests extends LeonTestSuite {
   // Print and reparse tests
   private def testPrint(name : String, strs : List[String]) { test(name){
     val orig = parseStrings(strs )
+    // FIXME This is just nonsense. What are we reparsing?
     val output = orig.units map { ScalaPrinter(_) }
     // If we can reparse, we consider it successful.
     val after = parseStrings(strs)
diff --git a/src/test/scala/leon/test/purescala/DataGen.scala b/src/test/scala/leon/test/purescala/DataGen.scala
index 45c7f066bb65b390d7b304673c1552d7ffc534ff..e2b89ad050a14ab7cae64b456f0be14f0d01e963 100644
--- a/src/test/scala/leon/test/purescala/DataGen.scala
+++ b/src/test/scala/leon/test/purescala/DataGen.scala
@@ -2,7 +2,6 @@
 
 package leon.test.purescala
 
-import leon._
 import leon.test._
 import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
 import leon.frontends.scalac.ExtractionPhase
@@ -15,8 +14,6 @@ import leon.datagen._
 
 import leon.evaluators._
 
-import org.scalatest.FunSuite
-
 class DataGen extends LeonTestSuite {
   private def parseString(str : String) : Program = {
     val pipeline = TemporaryInputPhase andThen ExtractionPhase andThen PreprocessingPhase
@@ -81,8 +78,6 @@ class DataGen extends LeonTestSuite {
 
     assert(generator.generate(listType).take(100).toSet.size === 100, "Should be able to generate 100 different lists")
 
-    val evaluator = new CodeGenEvaluator(testContext, prog)
-
     val a = Variable(FreshIdentifier("a", Int32Type))
     val b = Variable(FreshIdentifier("b", Int32Type))
     val x = Variable(FreshIdentifier("x", listType))
diff --git a/src/test/scala/leon/test/purescala/DefOpsTests.scala b/src/test/scala/leon/test/purescala/DefOpsTests.scala
index 380973e6357d41cd52f91f97c421c33ff3c86c50..2ceb1649364eed23ca8c1cfc0e74deac6fbc5ffe 100644
--- a/src/test/scala/leon/test/purescala/DefOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/DefOpsTests.scala
@@ -5,16 +5,12 @@ package leon.test.purescala
 import leon._
 import purescala.Definitions._
 import purescala.DefOps._
-import purescala.ScalaPrinter
 import frontends.scalac._
 import utils._
 import leon.test.LeonTestSuite
 
 private [purescala] object DefOpsHelper extends LeonTestSuite { 
   private def parseStrings(strs : List[String]) : Program = {
-    val settings : Settings = Settings(
-      verify = false
-    )
     val c = createLeonContext()
     val context : LeonContext = c.copy(settings = 
       c.settings.copy(verify = false)
diff --git a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
index 36b802cca7b0eba1d10116b5aa4e99f89cbf3650..d507826401fe86ecdfca1809f347028e9b2bdc47 100644
--- a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
@@ -2,13 +2,11 @@
 
 package leon.test.purescala
 
-import leon._
 import leon.test._
 import leon.purescala.Common._
 import leon.purescala.Expressions._
 import leon.purescala.Types._
 
-
 class LikelyEqSuite extends LeonTestSuite with WithLikelyEq {
   def i(x: Int) = InfiniteIntegerLiteral(x)
 
diff --git a/src/test/scala/leon/test/purescala/TransformationTests.scala b/src/test/scala/leon/test/purescala/TransformationTests.scala
index e2c2bb7a836c7130c89ac8fc98d7ae6d9949bc10..b56f9fd549e2ece0e1f88886b29c8c5c177c820e 100644
--- a/src/test/scala/leon/test/purescala/TransformationTests.scala
+++ b/src/test/scala/leon/test/purescala/TransformationTests.scala
@@ -2,17 +2,13 @@
 
 package leon.test.purescala
 
-import leon._
 import leon.test._
-import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
+import leon.utils. PreprocessingPhase
 import leon.frontends.scalac.ExtractionPhase
 
-import leon.purescala.ScalaPrinter
-import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Expressions._
 import leon.purescala.ExprOps._
-import leon.purescala.Types._
 
 import leon.solvers.z3.UninterpretedZ3Solver
 import leon.solvers._
diff --git a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
index f898dfee0b352b206b6d7dc724702311a2706495..f5b0cf3f32893e25caedcc02f57ed1d465de892c 100644
--- a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
@@ -2,14 +2,11 @@
 
 package leon.test.purescala
 
-import leon._
 import leon.test._
 
 import leon.purescala.Common._
-import leon.purescala.Definitions._
 import leon.purescala.Types._
 import leon.purescala.Expressions._
-import leon.purescala.ExprOps._
 import leon.purescala.TreeNormalizations._
 
 class TreeNormalizationsTests extends LeonTestSuite with WithLikelyEq {
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index 19ba9ae5dcc524424d862a5199a6b7ed2ee11bb9..de57844017d7f5fb100b4836cae5498466042e37 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -2,19 +2,12 @@
 
 package leon.test.purescala
 
-import leon._
 import leon.test._
-
-import leon.LeonContext
-
 import leon.purescala.Common._
-import leon.purescala.Definitions._
 import leon.purescala.Expressions._
 import leon.purescala.Types._
 import leon.purescala.ExprOps._
 
-import leon.solvers.z3._
-
 class TreeOpsTests extends LeonTestSuite with WithLikelyEq {
   
   test("Path-aware simplifications") {
diff --git a/src/test/scala/leon/test/purescala/TreeTests.scala b/src/test/scala/leon/test/purescala/TreeTests.scala
index 254441004b29e4f750d0ac6a833f31ab952f8c7a..9a7bd357e34aa9fb3cf198ff5d0ec9fea702f247 100644
--- a/src/test/scala/leon/test/purescala/TreeTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeTests.scala
@@ -2,11 +2,9 @@
 
 package leon.test.purescala
 
-import leon._
 import leon.test._
 
 import leon.purescala.Common._
-import leon.purescala.Definitions._
 import leon.purescala.Constructors._
 import leon.purescala.Expressions._
 import leon.purescala.Types._
diff --git a/src/test/scala/leon/test/purescala/WithLikelyEq.scala b/src/test/scala/leon/test/purescala/WithLikelyEq.scala
index 988247a5986ee4d8200813279e9ef64f3703b388..68da72895183567bd583e5b9f5ec749dad04d3a0 100644
--- a/src/test/scala/leon/test/purescala/WithLikelyEq.scala
+++ b/src/test/scala/leon/test/purescala/WithLikelyEq.scala
@@ -2,7 +2,6 @@
 
 package leon.test.purescala
 
-import leon._
 import leon.test._
 import leon.evaluators._
 import leon.purescala.Common._
@@ -48,7 +47,6 @@ trait WithLikelyEq {
         val counters: Array[Int] = vsOrder.map(_ => min)
         var i = 0
 
-        var cont = true
         while(i < counters.size && isEq) {
           val m: Map[Expr, Expr] = vsOrder.zip(counters).map{case (v, c) => (Variable(v), InfiniteIntegerLiteral(c))}.toMap
           val ne1 = replace(m, e1)
diff --git a/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala b/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
index 332777cd4ffa667c18d77400afc35e6f7f705d50..eff32f75b1db4f18d88ff48596a286febec6fd54 100644
--- a/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
@@ -2,11 +2,8 @@
 
 package leon.test.solvers
 
-import leon._
 import leon.test._
-import leon.utils.Interruptible
 import leon.solvers._
-import leon.solvers.combinators._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Expressions._
diff --git a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
index 8759d03ba5f614605417d0b0094aa795df116c6c..4525fcdc3667f0f81a9c1fb3b404aaa77a189f15 100644
--- a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
@@ -6,7 +6,6 @@ import leon._
 import leon.test._
 import leon.utils.Interruptible
 import leon.solvers._
-import leon.solvers.combinators._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Expressions._
@@ -46,7 +45,7 @@ class TimeoutSolverTests extends LeonTestSuite {
   }
 
   private def check(sf: SolverFactory[Solver], e: Expr): Option[Boolean] = {
-    val s = sf.getNewSolver
+    val s = sf.getNewSolver()
     s.assertCnstr(e)
     s.check
   }
diff --git a/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala b/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
index 0966c8b08e063123f1cdc7aca8b131f2c9f69b26..2df3a148170a6ae71d697732f451f16abb22bb8c 100644
--- a/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
@@ -1,6 +1,5 @@
 package leon.test.solvers
 
-import leon._
 import leon.test._
 import leon.purescala.Expressions._
 import leon.purescala.Types._
@@ -32,10 +31,10 @@ class UnrollingSolverTests extends LeonTestSuite {
   private val sf = SolverFactory(() => new UnrollingSolver(testContext, program, new UninterpretedZ3Solver(testContext, program)))
   private def check(expr: Expr, expected: Option[Boolean], msg: String) : Unit = {
     test(msg) {
-      val solver = sf.getNewSolver
+      val solver = sf.getNewSolver()
       solver.assertCnstr(expr)
       assert(solver.check == expected)
-      solver.free
+      solver.free()
     }
   }
 
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index e170dea4be5a7a0025799147a02e3ab71faee15d..c94fe6f783ec4fa460bc3cfd0f087d6357dc2a86 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -6,7 +6,6 @@ import leon.test._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Expressions._
-import leon.purescala.ExprOps._
 import leon.purescala.Types._
 
 import leon.solvers._
@@ -87,18 +86,18 @@ class FairZ3SolverTests extends LeonTestSuite {
     val f = And(b1, Not(b2))
 
     locally {
-      val (result, model) = solver.solveSAT(f)
+      val (result, _) = solver.solveSAT(f)
       assert(result === Some(true))
     }
 
     locally {
-      val (result, model, core) = solver.solveSATWithCores(f, Set(b1))
+      val (result, _, core) = solver.solveSATWithCores(f, Set(b1))
       assert(result === Some(true))
       assert(core.isEmpty)
     }
 
     locally {
-      val (result, model, core) = solver.solveSATWithCores(f, Set(b1, b2))
+      val (result, _, core) = solver.solveSATWithCores(f, Set(b1, b2))
       assert(result === Some(false))
       assert(core === Set(b2))
     }
diff --git a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
index 46c35cb9ef75dc67fc4574ab2216d8c5e3501880..cdf4d38d1ee7a0d496e3e461e6a99af861d60a56 100644
--- a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
+++ b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
@@ -10,7 +10,6 @@ import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.test.purescala.WithLikelyEq
 import leon.evaluators._
-import leon.LeonContext
 
 import leon.synthesis.LinearEquations._
 
@@ -105,7 +104,6 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
   
   test("particularSolution basecase") {
     def toExpr(es: Array[Expr]): Expr = {
-      val coef: Array[Expr] = es
       val vars: Array[Expr] = Array[Expr](i(1)) ++ Array[Expr](x, y)
       es.zip(vars).foldLeft[Expr](i(0))( (acc: Expr, p: (Expr, Expr)) => Plus(acc, Times(p._1, p._2)) )
     }
@@ -127,7 +125,6 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
 
   test("particularSolution preprocess") {
     def toExpr(es: Array[Expr], vs: Array[Expr]): Expr = {
-      val coef: Array[Expr] = es
       val vars: Array[Expr] = Array[Expr](i(1)) ++ vs
       es.zip(vars).foldLeft[Expr](i(0))( (acc: Expr, p: (Expr, Expr)) => Plus(acc, Times(p._1, p._2)) )
     }
diff --git a/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
index 1a2f205d381ed1eac9d4d51fa1d623dec73c693e..822e201dadf6424b41624ff65198e6c3ab206a75 100644
--- a/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
@@ -11,7 +11,6 @@ import leon.purescala.PrinterContext
 import leon.purescala.PrinterOptions
 import leon.synthesis._
 
-import scala.collection.mutable
 import scala.collection.mutable.Stack
 import scala.io.Source
 
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index a1ffa10812feb8e5335af877e00086ffed85051a..02199d28ef136221dd6e846159cfc5ed0fb01651 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -5,12 +5,7 @@ import leon.test._
 
 import leon._
 import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.ExprOps._
-import leon.solvers.z3._
-import leon.solvers.Solver
 import leon.synthesis._
-import leon.synthesis.utils._
 
 import java.io.File
 
@@ -45,7 +40,7 @@ class SynthesisRegressionSuite extends LeonTestSuite {
     for (ci <- chooses) {
       test(cat+": "+f.getName+" - "+ci.fd.id.name) {
         val synthesizer = new Synthesizer(ctx, program, ci, opts)
-        val (search, sols) = synthesizer.synthesize()
+        val (_, sols) = synthesizer.synthesize()
         if (sols.isEmpty) {
           fail("Solution was not found. (Search bound: "+bound+")")
         }
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 9f3a3aa5d2e5dd54b60940ec1448d77cd581c4cb..9abd14c6ed9f54e0762bc141f968a0f5f4450526 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -82,7 +82,7 @@ class SynthesisSuite extends LeonTestSuite {
   }
 
   def forProgram(title: String, opts: SynthesisSettings = SynthesisSettings())(content: String)(strats: PartialFunction[String, SynStrat]) {
-      test("Synthesizing %3d: [%s]".format(nextInt(), title)) {
+      test(f"Synthesizing ${nextInt()}%3d: [$title]") {
         val ctx = testContext.copy(settings = Settings(
             synthesis = true,
             xlang     = false,
@@ -94,7 +94,7 @@ class SynthesisSuite extends LeonTestSuite {
         val (program, results) = pipeline.run(ctx)((content, Nil))
 
         for ((f,cis) <- results; ci <- cis) {
-          info("%-20s".format(ci.fd.id.toString))
+          info(f"${ci.fd.id.toString}%-20s")
 
 
           val sctx = SynthesisContext(ctx,
diff --git a/src/test/scala/leon/test/termination/TerminationRegression.scala b/src/test/scala/leon/test/termination/TerminationRegression.scala
index c3b53c9f338cc72a8364feb1c61d3f43f2d8c3b3..12e0c0aaa5b9d535e885321ff34b10f36ff52e1d 100644
--- a/src/test/scala/leon/test/termination/TerminationRegression.scala
+++ b/src/test/scala/leon/test/termination/TerminationRegression.scala
@@ -30,9 +30,9 @@ class TerminationRegression extends LeonTestSuite {
       fullName
     }
 
-    test("%3d: %s %s".format(nextInt(), displayName, leonOptions.mkString(" "))) {
+    test(f"${nextInt()}%3d: $displayName ${leonOptions.mkString(" ")}") {
       assert(file.exists && file.isFile && file.canRead,
-             "Benchmark %s is not a readable file".format(displayName))
+             s"Benchmark $displayName is not a readable file")
 
       val ctx = testContext.copy(
         settings = Settings(
diff --git a/src/test/scala/leon/test/utils/Streams.scala b/src/test/scala/leon/test/utils/Streams.scala
index dfca447258abc2396a58930b61a36f213d3808f7..44849cad633241ad077a6c189f164a71c441b9c0 100644
--- a/src/test/scala/leon/test/utils/Streams.scala
+++ b/src/test/scala/leon/test/utils/Streams.scala
@@ -2,22 +2,10 @@
 
 package leon.test.purescala
 
-import leon._
 import leon.test._
-import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
-import leon.frontends.scalac.ExtractionPhase
-
 import leon.purescala.Common._
-import leon.purescala.Expressions._
-import leon.purescala.Definitions._
-import leon.purescala.Types._
-import leon.datagen._
 import leon.utils.StreamUtils._
 
-import leon.evaluators._
-
-import org.scalatest.FunSuite
-
 class Streams extends LeonTestSuite {
   test("Cartesian Product 1") {
     val s1 = FreshIdentifier("B", alwaysShowUniqueID = true) #::
diff --git a/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala b/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
index b945059b8a20ffa470259a35e50cd8516e4d23ac..e65a62167c795c502bfacfbfd36641f4c6fed77e 100644
--- a/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
@@ -4,10 +4,6 @@ package leon.test.verification
 
 import leon._
 import leon.test._
-
-
-import java.io.File
-
 import leon.frontends.scalac.ExtractionPhase
 import leon.utils.PreprocessingPhase
 import leon.verification.AnalysisPhase
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 51aa4fced083cb589898609bc089c8a684bd941c..f2bfc13743573cf79a8b85e841a40b9d2f5c4783 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -3,17 +3,10 @@
 package leon.test.verification
 
 import leon._
-import leon.test._
-
-import leon.verification.{AnalysisPhase,VerificationReport}
-import leon.purescala.Definitions.Program
-import leon.frontends.scalac.ExtractionPhase
-import leon.utils.PreprocessingPhase
+import leon.verification.AnalysisPhase
 
 import _root_.smtlib.interpreters._
 
-import java.io.File
-
 // If you add another regression test, make sure it contains one object whose name matches the file name
 // This is because we compile all tests from each folder separately.
 class PureScalaVerificationRegression extends VerificationRegression {
diff --git a/src/test/scala/leon/test/verification/VerificationRegression.scala b/src/test/scala/leon/test/verification/VerificationRegression.scala
index 210a5ab7e5e3a67e02fbc4c63ce6b61f63162b60..398d4e2f0e1ea67081a0d49242b44ddbe9fe8b59 100644
--- a/src/test/scala/leon/test/verification/VerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/VerificationRegression.scala
@@ -43,7 +43,7 @@ trait VerificationRegression extends LeonTestSuite {
       val (user, lib) = ast.units partition { _.isMainUnit }
       user map { u => Program(u.id.freshen, u :: lib) }
     }
-    for (p <- programs; displayName = p.id.name) test("%3d: %s %s".format(nextInt(), displayName, leonOptions.mkString(" "))) {
+    for (p <- programs; displayName = p.id.name) test(f"${nextInt()}%3d: $displayName ${leonOptions.mkString(" ")}") {
       val report = pipeBack.run(ctx)(p)
       block(Output(report, ctx.reporter))
     }
@@ -54,7 +54,7 @@ trait VerificationRegression extends LeonTestSuite {
 
     fs foreach { file => 
       assert(file.exists && file.isFile && file.canRead,
-        "Benchmark %s is not a readable file".format(file.getName))
+        s"Benchmark ${file.getName} is not a readable file")
     }
 
     val files = fs map { _.getPath }