diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 7ae02d83e0a6245c7345ef7349211e6c246221ac..7ad5c222bb2c252faa1f9f710ea41b589091cfeb 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -17,8 +17,6 @@ import xlang.Expressions._
 import purescala.ExprOps._
 import purescala.Types._
 
-import scala.collection.mutable.{Map => MutableMap}
-
 case class UnsoundExtractionException(ast: Z3AST, msg: String)
   extends Exception("Can't extract " + ast + " : " + msg)
 
@@ -705,7 +703,7 @@ trait AbstractZ3Solver extends Solver {
                     val elems = r.elems.flatMap {
                       case (k, CaseClass(leonSome, Seq(x))) => Some(k -> x)
                       case (k, _) => None
-                    }.toMap
+                    }
 
                     FiniteMap(elems, from, to)
                 }
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 0c9adeb86aff8da5395b15436f65ea83c6b75dac..128d7299da70987e1a408f100619b8a42a46b92a 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -570,8 +570,6 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
       // are minimal we make sure we exclude only Bs that are used.
       def excludeProgram(bs: Set[Identifier], isMinimal: Boolean): Unit = {
 
-
-
         def filterBTree(c: Identifier): Set[Identifier] = {
           val (b, _, subcs) = cTree(c).find(sub => bs(sub._1)).get
           subcs.flatMap(filterBTree).toSet + b
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index 50a38abc6fe5dbe434b799caaeb67ee48274cbf8..afabdad92c61127c5bb6399edce8743002641e1f 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -4,15 +4,11 @@ package leon
 package synthesis
 package rules
 
-import leon.purescala.Common.Identifier
+import purescala.Common.Identifier
 import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
 
-import solvers._
-
-import scala.concurrent.duration._
-
 /** For every pair of input variables of the same type,
   * checks equality and output an If-Then-Else statement with the two new branches. */
 case object EqualitySplit extends Rule("Eq. Split") {