diff --git a/src/main/scala/leon/datagen/SolverDataGen.scala b/src/main/scala/leon/datagen/SolverDataGen.scala
index 78b3753cfff8887d438477c2ad1176b8218254b1..027cc41e02cc18813ca6366e34c0d6761f412b8c 100644
--- a/src/main/scala/leon/datagen/SolverDataGen.scala
+++ b/src/main/scala/leon/datagen/SolverDataGen.scala
@@ -8,12 +8,7 @@ import purescala.Types._
 import purescala.Definitions._
 import purescala.Common._
 import purescala.Constructors._
-import purescala.Extractors._
-import evaluators._
 import solvers._
-import solvers.combinators._
-import solvers.smtlib._
-import solvers.z3._
 import utils._
 
 
@@ -68,7 +63,7 @@ class SolverDataGen(ctx: LeonContext, pgm: Program, sff: ((LeonContext, Program)
             sizeFor(tupleSelect(of, i+1, tps.size))
           }
 
-          exprs.foldLeft(InfiniteIntegerLiteral(1): Expr)(plus _)
+          exprs.foldLeft(InfiniteIntegerLiteral(1): Expr)(plus)
 
         case _ =>
           InfiniteIntegerLiteral(1)
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 1751a1e55c51a222f0e90d4ea3989bee27f2616a..72a905b82af310110c1aa83e72ec2409d4406fa7 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -280,20 +280,18 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
     // Split conjunctions
     val TopLevelAnds(ands) = satisfying
 
-    val runners = ands.map(a => compile(a, ins) match {
+    val runners = ands.flatMap(a => compile(a, ins) match {
       case Some(runner) => Some(runner)
       case None =>
-        ctx.reporter.error("Could not compile predicate "+a)
+        ctx.reporter.error("Could not compile predicate " + a)
         None
-    }).flatten
+    })
 
 
     val gen = new StubGenerator[Expr, TypeTree]((ints.values ++ bigInts.values ++ booleans.values).toSeq,
                                                 Some(getConstructors _),
                                                 treatEmptyStubsAsChildless = true)
 
-    var found = Set[Seq[Expr]]()
-
     /**
      * Gather at most <n> isomoprhic models  before skipping them
      * - Too little means skipping many excluding patterns
@@ -315,7 +313,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
           theNext = computeNext()
         }
 
-        theNext != None
+        theNext.isDefined
       }
 
       def next() = {
diff --git a/src/main/scala/leon/evaluators/TracingEvaluator.scala b/src/main/scala/leon/evaluators/TracingEvaluator.scala
index d6388822cf58f7ac89bb73a069e0c3c3f3cf7225..ea5ad3e0d76b5fa5230aa203d29ba214c7d3f15f 100644
--- a/src/main/scala/leon/evaluators/TracingEvaluator.scala
+++ b/src/main/scala/leon/evaluators/TracingEvaluator.scala
@@ -14,7 +14,7 @@ class TracingEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 1000) ex
 
   def initRC(mappings: Map[Identifier, Expr]) = TracingRecContext(mappings, 2)
 
-  def initGC = new TracingGlobalContext(Nil)
+  def initGC() = new TracingGlobalContext(Nil)
 
   class TracingGlobalContext(var values: List[(Tree, Expr)]) extends GlobalContext
 
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 919118dd9ce638bf80d4c154e06c254f67203da9..3c4818737dcc4012665a837bf81609c7dfce0854 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -575,7 +575,7 @@ trait ASTExtractors {
         case a @ Apply(
               TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "withOracle"), types),
               Function(vds, body) :: Nil) =>
-            Some(((types zip vds.map(_.symbol)), body))
+            Some((types zip vds.map(_.symbol), body))
         case _ => None
       }
     }
@@ -592,7 +592,7 @@ trait ASTExtractors {
         case a @ Apply(
             TypeApply(s @ ExSymbol("leon", "lang", "forall"), types),
             Function(vds, predicateBody) :: Nil) =>
-          Some(((types zip vds.map(_.symbol)), predicateBody))
+          Some((types zip vds.map(_.symbol), predicateBody))
         case _ => None
       }
     }
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index 461f145019edf1c136e896065d8402174052099b..17503361e0bb20a87ed15047eeea99b04688a803 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -4,8 +4,6 @@ package leon
 package frontends.scalac
 
 import purescala.Definitions.Program
-import purescala.Common.FreshIdentifier
-
 import utils._
 
 import scala.tools.nsc.{Settings,CompilerCommand}
diff --git a/src/main/scala/leon/frontends/scalac/SimpleReporter.scala b/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
index d04cebb3e04eaa78a555c33f1093c1a1e6935849..c203ee63c17585c9bcf5922762e3046e8662c888 100644
--- a/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
+++ b/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
@@ -51,7 +51,6 @@ class SimpleReporter(val settings: Settings, reporter: leon.Reporter) extends Ab
       case NoPosition =>
         printMessage(msg, LeonNoPosition, severity)
       case _ =>
-        val buf = new StringBuilder(msg)
         val lpos = LeonOffsetPosition(pos.line, pos.column, pos.point, pos.source.file.file)
         printMessage(msg, lpos, severity)
     }
diff --git a/src/main/scala/leon/grammars/SizeBoundedGrammar.scala b/src/main/scala/leon/grammars/SizeBoundedGrammar.scala
index 697120356afceac724ee6cf7257f96756cff3f60..8756b136abf0f6bbffe6721bb3439aebc76a0a6b 100644
--- a/src/main/scala/leon/grammars/SizeBoundedGrammar.scala
+++ b/src/main/scala/leon/grammars/SizeBoundedGrammar.scala
@@ -4,9 +4,6 @@ package leon
 package grammars
 
 import purescala.Types._
-import purescala.Expressions._
-import purescala.TypeOps._
-
 import leon.utils.SeqUtils.sumTo
 
 case class SizedLabel[T <% Typed](underlying: T, size: Int) extends Typed {
diff --git a/src/main/scala/leon/grammars/ValueGrammar.scala b/src/main/scala/leon/grammars/ValueGrammar.scala
index 2b7bb140b63b110a60d1d97c104329db2dd61eb8..5442b4ee7723fb124aab8aea65647ed762a9f0ec 100644
--- a/src/main/scala/leon/grammars/ValueGrammar.scala
+++ b/src/main/scala/leon/grammars/ValueGrammar.scala
@@ -5,8 +5,6 @@ package grammars
 
 import purescala.Types._
 import purescala.Expressions._
-import purescala.Constructors._
-
 
 case object ValueGrammar extends ExpressionGrammar[TypeTree] {
   def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = t match {
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index a8a043047c616311bc134c95d9cf231b5448aa7c..0433affa5cd69d958f9359adec8157f54a436b28 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -93,7 +93,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
 
             bh += be
 
-            bh.write
+            bh.write()
           }
 
           if (synth.settings.generateDerivationTrees) {
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index 262d40580c6896099a8c679ccd904fb3a3c461e2..8c1694dbda953071d51226782965e488b406b607 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -5,25 +5,17 @@ package repair
 package rules
 
 import synthesis._
-
-import leon.utils.Simplifiers
-
-import purescala.ScalaPrinter
-
 import evaluators._
 
 import purescala.Expressions._
-import purescala.Definitions._
 import purescala.Common._
 import purescala.Types._
 import purescala.ExprOps._
-import purescala.Extractors._
 import purescala.Constructors._
 import purescala.Extractors._
 
 import Witnesses._
 
-import solvers._
 import graph.AndNode
 
 case object Focus extends PreprocessingRule("Focus") {
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index 8470a974459017ed90c3d6ac69c9e4ea703dc0d0..0c6106127ce7187ff4dded02b18863fcd332677b 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -90,7 +90,7 @@ final case class Chain(relations: List[Relation]) {
   }
   */
 
-  lazy val cycles : Seq[List[Relation]] = (0 to relations.size - 1).map { index =>
+  lazy val cycles : Seq[List[Relation]] = relations.indices.map { index =>
     val (start, end) = relations.splitAt(index)
     end ++ start
   }
diff --git a/src/main/scala/leon/termination/ChainComparator.scala b/src/main/scala/leon/termination/ChainComparator.scala
index a3ab3f8f4fb40eac7871bc4eee73ec4bb3414213..0c3cbd8756a79222d85468fea16b73ce7f73d9bd 100644
--- a/src/main/scala/leon/termination/ChainComparator.scala
+++ b/src/main/scala/leon/termination/ChainComparator.scala
@@ -37,7 +37,7 @@ trait ChainComparator { self : StructuralSize =>
           rec(fieldTpe).map(recons => (e: Expr) => recons(caseClassSelector(cct, e, fieldId)))
         })
       case TupleType(tpes) =>
-        powerSetToFunSet((0 until tpes.length).flatMap { case index =>
+        powerSetToFunSet(tpes.indices.flatMap { case index =>
           rec(tpes(index)).map(recons => (e: Expr) => recons(tupleSelect(e, index + 1, true)))
         })
       case _ => Set((e: Expr) => e)
@@ -53,7 +53,7 @@ trait ChainComparator { self : StructuralSize =>
           rec(fieldTpe).map(recons => (e: Expr) => recons(caseClassSelector(cct, e, fieldId)))
         }.toSet
       case TupleType(tpes) =>
-        (0 until tpes.length).flatMap { case index =>
+        tpes.indices.flatMap { case index =>
           rec(tpes(index)).map(recons => (e: Expr) => recons(tupleSelect(e, index + 1, true)))
         }.toSet
       case _ => Set((e: Expr) => e)
diff --git a/src/main/scala/leon/termination/ComplexTerminationChecker.scala b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
index eef8ddaac7d2f99d47e3f713b6f71925826202ab..83638aa84233775b256e7e44d43d77b906c7a4c7 100644
--- a/src/main/scala/leon/termination/ComplexTerminationChecker.scala
+++ b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
@@ -4,7 +4,6 @@ package leon
 package termination
 
 import purescala.Definitions._
-import purescala.Expressions._
 
 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 db91c8602558b7c8bb787a09efe6da3ab54fccd8..91590dd4aca8e82c846b8c970475b500db07e785 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -10,7 +10,6 @@ import purescala.Definitions._
 import scala.concurrent.duration._
 
 import leon.solvers._
-import leon.solvers.z3._
 
 trait Processor {
 
diff --git a/src/main/scala/leon/termination/RecursionProcessor.scala b/src/main/scala/leon/termination/RecursionProcessor.scala
index 2a93aa85320567c46e555b024a575a80d92c49b8..72c64f62aa1a3ceb28d3e23f9bace1e40e06209b 100644
--- a/src/main/scala/leon/termination/RecursionProcessor.scala
+++ b/src/main/scala/leon/termination/RecursionProcessor.scala
@@ -50,5 +50,3 @@ class RecursionProcessor(val checker: TerminationChecker, val rb: RelationBuilde
     }
   }
 }
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/main/scala/leon/termination/RelationProcessor.scala b/src/main/scala/leon/termination/RelationProcessor.scala
index 2909d6c4f58ebeafc71fbe05e0e79455ef997e85..d71a6fa3ae5c57e0244bf4a1e194605d9eda4a7d 100644
--- a/src/main/scala/leon/termination/RelationProcessor.scala
+++ b/src/main/scala/leon/termination/RelationProcessor.scala
@@ -4,10 +4,6 @@ package leon
 package termination
 
 import leon.purescala.Expressions._
-import leon.purescala.ExprOps._
-import leon.purescala.Types._
-import leon.purescala.Common._
-import leon.purescala.Extractors._
 import leon.purescala.Constructors._
 import leon.purescala.Definitions._
 
diff --git a/src/main/scala/leon/termination/SelfCallsProcessor.scala b/src/main/scala/leon/termination/SelfCallsProcessor.scala
index 8b53f7cd166c8adeb52e9a2c9f3107cf6fd26936..b8fe65f48b3776d8a8f3dae6782133c6518ec00d 100644
--- a/src/main/scala/leon/termination/SelfCallsProcessor.scala
+++ b/src/main/scala/leon/termination/SelfCallsProcessor.scala
@@ -6,7 +6,6 @@ package termination
 import purescala.Definitions._
 import purescala.Common._
 import purescala.Expressions._
-import purescala.Constructors._
 
 class SelfCallsProcessor(val checker: TerminationChecker) extends Processor {
 
diff --git a/src/main/scala/leon/termination/Strengthener.scala b/src/main/scala/leon/termination/Strengthener.scala
index 192e78599edbb4cb9801324a24099a9302001b23..dc3d0818830accf356fdfc93853df45f0d8e1198 100644
--- a/src/main/scala/leon/termination/Strengthener.scala
+++ b/src/main/scala/leon/termination/Strengthener.scala
@@ -20,7 +20,7 @@ trait Strengthener { self : RelationComparator =>
 
   def strengthenPostconditions(funDefs: Set[FunDef])(implicit solver: Processor with Solvable) {
     // Strengthen postconditions on all accessible functions by adding size constraints
-    val callees : Set[FunDef] = funDefs.map(fd => checker.program.callGraph.transitiveCallees(fd)).flatten
+    val callees : Set[FunDef] = funDefs.flatMap(fd => checker.program.callGraph.transitiveCallees(fd))
     val sortedCallees : Seq[FunDef] = callees.toSeq.sortWith((fd1, fd2) => checker.program.callGraph.transitivelyCalls(fd2, fd1))
 
     for (funDef <- sortedCallees if !strengthenedPost(funDef) && funDef.hasBody && checker.terminates(funDef).isGuaranteed) {
@@ -175,6 +175,3 @@ trait Strengthener { self : RelationComparator =>
     }
   }
 }
-
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 99b3c18f66237796d0dfae14c9d24ebb06c26a3b..cb8fa053864dddcc288bb8cc4f93e55ecf8c84b5 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -90,7 +90,7 @@ trait StructuralSize {
   def lexicographicDecreasing(s1: Seq[Expr], s2: Seq[Expr], strict: Boolean, sizeOfOneExpr: Expr => Expr): Expr = {
     // Note: The Equal and GreaterThan ASTs work for both BigInt and Bitvector
     
-    val sameSizeExprs = for ((arg1, arg2) <- (s1 zip s2)) yield Equals(sizeOfOneExpr(arg1), sizeOfOneExpr(arg2))
+    val sameSizeExprs = for ((arg1, arg2) <- s1 zip s2) yield Equals(sizeOfOneExpr(arg1), sizeOfOneExpr(arg2))
     
     val greaterBecauseGreaterAtFirstDifferentPos =
       orJoin(for (firstDifferent <- 0 until scala.math.min(s1.length, s2.length)) yield and(
@@ -107,5 +107,3 @@ trait StructuralSize {
 
   def defs : Set[FunDef] = Set(sizeCache.values.toSeq : _*)
 }
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index b13c109ad4a6257c315d2591903cee125aeff496..a9f7ef77b616a8a08e0b438a162b385135deee50 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -4,7 +4,6 @@ package leon
 package termination
 
 import purescala.Definitions._
-import purescala.DefOps._
 
 object TerminationPhase extends LeonPhase[Program,TerminationReport] {
   val name = "Termination"
diff --git a/src/main/scala/leon/utils/Benchmarks.scala b/src/main/scala/leon/utils/Benchmarks.scala
index c3927ad12b089001ac0922545007b83b99948e57..71d948949a6d7d9cf8f6ce8501d71c451f18c2f4 100644
--- a/src/main/scala/leon/utils/Benchmarks.scala
+++ b/src/main/scala/leon/utils/Benchmarks.scala
@@ -6,7 +6,7 @@ package utils
 import java.io.{File, PrintWriter}
 import scala.io.Source
 
-import com.fasterxml.jackson.databind.{DeserializationFeature, ObjectMapper}
+import com.fasterxml.jackson.databind.ObjectMapper
 import com.fasterxml.jackson.module.scala.experimental.ScalaObjectMapper
 import com.fasterxml.jackson.module.scala.DefaultScalaModule
 
@@ -38,7 +38,7 @@ class BenchmarksHistory(file: File) {
     try {
       pw.write(json)
     } finally {
-      pw.close
+      pw.close()
     }
   }
 
diff --git a/src/main/scala/leon/utils/FreeableIterator.scala b/src/main/scala/leon/utils/FreeableIterator.scala
index a15922640077052f8164780df49d51866ac5fa4f..f6ad42937c4000891a0639fc7a9e1b3ef7097c0e 100644
--- a/src/main/scala/leon/utils/FreeableIterator.scala
+++ b/src/main/scala/leon/utils/FreeableIterator.scala
@@ -4,7 +4,7 @@ package utils
 abstract class FreeableIterator[T] extends Iterator[T] {
   private[this] var nextElem: Option[T] = None
 
-  def hasNext() = {
+  def hasNext = {
     nextElem = computeNext()
     nextElem.nonEmpty
   }
diff --git a/src/main/scala/leon/utils/Graphs.scala b/src/main/scala/leon/utils/Graphs.scala
index 604bef784df0cfbb4cabf04056676b27bd187089..b3aeef558790ce9427e376d0e0adba2851813b7b 100644
--- a/src/main/scala/leon/utils/Graphs.scala
+++ b/src/main/scala/leon/utils/Graphs.scala
@@ -172,7 +172,7 @@ object Graphs {
         } else {
           seen += v
           val ins = inEdges(v).map(_.v1)
-          ins ++ ins.map(rec).flatten
+          ins ++ ins.flatMap(rec)
         }
       }
       rec(v)
@@ -186,7 +186,7 @@ object Graphs {
         } else {
           seen += v
           val outs = outEdges(v).map(_.v2)
-          outs ++ outs.map(rec).flatten
+          outs ++ outs.flatMap(rec)
         }
       }
       rec(v)
@@ -203,7 +203,7 @@ object Graphs {
           if (outs(v2)) {
             true
           } else {
-            outs.map(rec).contains(true)
+            outs.exists(rec)
           }
         }
       }
diff --git a/src/main/scala/leon/utils/ModelEnumerator.scala b/src/main/scala/leon/utils/ModelEnumerator.scala
index d492826396674077a9351d5c771aebe0c056875c..7494e0c463051e0a1337287c4e9e8310d3d23106 100644
--- a/src/main/scala/leon/utils/ModelEnumerator.scala
+++ b/src/main/scala/leon/utils/ModelEnumerator.scala
@@ -49,9 +49,9 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
         s.check match {
           case Some(true) =>
             val model = s.getModel
-            val idsModel = (ids.map { id =>
+            val idsModel = ids.map { id =>
               id -> model.getOrElse(id, simplestValue(id.getType))
-            }).toMap
+            }.toMap
 
             // Vary the model
             s.assertCnstr(not(andJoin(idsModel.toSeq.sortBy(_._1).map { case (k, v) => equality(k.toVariable, v) })))
@@ -148,9 +148,9 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
           s.check match {
             case Some(true) =>
               val sm = s.getModel
-              val m = (ids.map { id =>
+              val m = ids.map { id =>
                 id -> sm.getOrElse(id, simplestValue(id.getType))
-              }).toMap
+              }.toMap
 
               evaluator.eval(measure, m).result match {
                 case Some(InfiniteIntegerLiteral(measureVal)) =>
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 3128567904b2e21165ff6ba8a35759114af5313e..ba23961e3cd8e3eaa37d9f581c35b0df5d91b646 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -65,7 +65,7 @@ case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option
         }
 
         if (strings.nonEmpty) {
-          val max = strings.map(_._1.size).max
+          val max = strings.map(_._1.length).max
 
           for ((id, v) <- strings) {
             reporter.warning(("  %-"+max+"s -> %s").format(id, v))