diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index f0817f3bc732995036113f3d2d81fedec81a5c80..71c91c551c42e8848f2d025439cfd0970c3f9d94 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -2,27 +2,16 @@
 
 package leon.purescala
 
-import leon.purescala
-import leon.solvers.{ Model, SolverFactory }
+import Constructors._
+import Expressions._
+import Types._
+import Common._
+import Definitions._
+import leon.evaluators._
 import leon.LeonContext
-import leon.evaluators
 import leon.utils.StreamUtils
-import leon.purescala.Quantification._
-import leon.utils.DebugSectionEvaluation
-import purescala.Definitions.Program
-import purescala.Expressions._
-import purescala.Types.StringType
-import purescala.Constructors._
-import purescala.ExprOps._
-import purescala.Expressions._
-import purescala.Expressions.{Choose }
-import purescala.Extractors._
-import purescala.TypeOps._
-import purescala.Types._
-import purescala.Common._
-import purescala.Definitions._
+
 import scala.collection.mutable.ListBuffer
-import leon.evaluators.DefaultEvaluator
 
 object SelfPrettyPrinter {
   def prettyPrintersForType(inputType: TypeTree)(implicit ctx: LeonContext, program: Program): Stream[Lambda] = {
@@ -185,7 +174,7 @@ class SelfPrettyPrinter extends PrettyPrinterFinder[Lambda, Lambda] { top =>
               orElse
           }
         } catch {
-          case e: evaluators.ContextualEvaluator#EvalError =>
+          case e: ContextualEvaluator#EvalError =>
             ctx.reporter.debug("Error "  + e.msg)
             orElse
         }
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index dfb6da0752c5e788ad89377fc3c6e087f185c798..cc20b71fb495703d7bfeecf4a01f3a538ac5da79 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -69,7 +69,7 @@ case object StringRender extends Rule("StringRender") {
   
   val booleanTemplate = (a: Expr) => StringTemplateGenerator(Hole => IfExpr(a, Hole, Hole))
   
-  import StringSolver.{StringFormToken, StringForm, Problem => SProblem, Equation, Assignment}
+  import StringSolver.{StringFormToken, Problem => SProblem, Equation, Assignment}
   
   /** Augment the left-hand-side to have possible function calls, such as x + "const" + customToString(_) ...
    *  Function calls will be eliminated when converting to a valid problem.
diff --git a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
index 06abffdefb888208b7cfb7904efba5d3434eb835..ed9be0442e637a9398e42741864b489a4414d4d1 100644
--- a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
@@ -5,7 +5,6 @@ package leon.regression.synthesis
 import leon.test._
 
 import leon._
-import leon.purescala.Definitions._
 import leon.synthesis._
 
 import java.io.File