diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index 8eea31aa7b604f4cae1da2091038be6af6557e17..adeb162f4ff4350bf53623ab9df5bbbf57ee81d3 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -4,7 +4,6 @@ package leon
import leon.utils._
-import purescala.Definitions.Program
import java.io.File
/** Everything that is part of a compilation unit, except the actual program tree.
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index cc39c108e5ec8f00f8d1bb68db85c3b51503e745..9bd1a983f6096d68cbb870097db16ac386209bcc 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -4,11 +4,6 @@ package leon
import utils._
-import purescala.Definitions.Definition
-import purescala.Trees.Expr
-import purescala.PrettyPrinter
-import scala.annotation.implicitNotFound
-
abstract class Reporter(settings: Settings) {
abstract class Severity
diff --git a/src/main/scala/leon/codegen/CodeGenPhase.scala b/src/main/scala/leon/codegen/CodeGenPhase.scala
index 2d9abd0b2a403ffed57480b8cb6dbdb4eefcda4d..8acf1fa619d7b8b4642f82babc149149965e6ecf 100644
--- a/src/main/scala/leon/codegen/CodeGenPhase.scala
+++ b/src/main/scala/leon/codegen/CodeGenPhase.scala
@@ -5,13 +5,8 @@ package codegen
import scala.util.control.NonFatal
-import purescala.Common._
import purescala.Definitions._
-import cafebabe._
-import cafebabe.ClassFileTypes.U2
-import cafebabe.Flags._
-
object CodeGenPhase extends LeonPhase[Program,CompilationResult] {
val name = "CodeGen"
val description = "Compiles a Leon program into Java methods"
diff --git a/src/main/scala/leon/codegen/CompiledExpression.scala b/src/main/scala/leon/codegen/CompiledExpression.scala
index dc2f9767a50474ea62921b4c76d38f64c6b7ce04..78cca61d102e038cef7e6172738b318d12e2dd2b 100644
--- a/src/main/scala/leon/codegen/CompiledExpression.scala
+++ b/src/main/scala/leon/codegen/CompiledExpression.scala
@@ -4,15 +4,9 @@ package leon
package codegen
import purescala.Common._
-import purescala.Definitions._
import purescala.Trees._
-import purescala.TypeTrees._
import cafebabe._
-import cafebabe.AbstractByteCodes._
-import cafebabe.ByteCodes._
-import cafebabe.ClassFileTypes._
-import cafebabe.Flags._
import runtime.{LeonCodeGenRuntimeMonitor => LM }
diff --git a/src/main/scala/leon/codegen/runtime/GenericValues.scala b/src/main/scala/leon/codegen/runtime/GenericValues.scala
index 790f35a5ca64a7971d45109820e440135999534f..dee6b18503b843873ae68aa2747f49e0d3d2fe9f 100644
--- a/src/main/scala/leon/codegen/runtime/GenericValues.scala
+++ b/src/main/scala/leon/codegen/runtime/GenericValues.scala
@@ -3,17 +3,9 @@
package leon
package codegen.runtime
-import utils._
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Trees.{Tuple => LeonTuple, _}
-import purescala.TreeOps.valuateWithModel
-import purescala.TypeTrees._
-
+import purescala.Trees.GenericValue
import scala.collection.immutable.{Map => ScalaMap}
-import synthesis._
-
object GenericValues {
private[this] var counter = 0;
diff --git a/src/main/scala/leon/datagen/NaiveDataGen.scala b/src/main/scala/leon/datagen/NaiveDataGen.scala
index 212b3ba226bee348ad4a4cc6c0eaa957fe39afff..b447778728d90730833b63a8fba3251c09e6c49e 100644
--- a/src/main/scala/leon/datagen/NaiveDataGen.scala
+++ b/src/main/scala/leon/datagen/NaiveDataGen.scala
@@ -5,7 +5,6 @@ package datagen
import purescala.Common._
import purescala.Trees._
-import purescala.TreeOps._
import purescala.TypeTrees._
import purescala.Definitions._
import utils.StreamUtils._
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index e13a0d216adee3ecd5017d3449fb3ed3f4d4569a..c21315468e5f948fcedc626eb4b597b25cfd4ea3 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -5,9 +5,7 @@ package evaluators
import purescala.Common._
import purescala.Definitions._
-import purescala.TreeOps._
import purescala.Trees._
-import purescala.TypeTrees._
import codegen.CompilationUnit
import codegen.CodeGenParams
diff --git a/src/main/scala/leon/frontends/scalac/AddTypeAnnotations.scala b/src/main/scala/leon/frontends/scalac/AddTypeAnnotations.scala
index 3bfe34f49a0957e16c226fe5f510aa5ab2dee38d..98f6160344dc2b145a294747bf2c3ca6e03f8b09 100644
--- a/src/main/scala/leon/frontends/scalac/AddTypeAnnotations.scala
+++ b/src/main/scala/leon/frontends/scalac/AddTypeAnnotations.scala
@@ -4,11 +4,9 @@ package leon
package frontends.scalac
import scala.tools.nsc._
-import scala.tools.nsc.plugins._
trait AddTypeAnnotations extends SubComponent with ASTExtractors {
import global._
- import global.definitions._
import ExtractorHelpers._
val phaseName = "addtypeannotations"
diff --git a/src/main/scala/leon/frontends/scalac/LeonExtraction.scala b/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
index 36ba8587dae30245af64b3e561bd088beee21cac..acb427180ee22b26e92d9a12032ec7759ef1287b 100644
--- a/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
@@ -4,10 +4,6 @@ package leon
package frontends.scalac
import scala.tools.nsc._
-import scala.tools.nsc.plugins._
-
-import purescala.Definitions.Program
-import purescala.Definitions.{ModuleDef => LeonModuleDef, _}
trait LeonExtraction extends SubComponent with CodeExtraction {
import global._
diff --git a/src/main/scala/leon/frontends/scalac/SaveImports.scala b/src/main/scala/leon/frontends/scalac/SaveImports.scala
index dc941d197a0ab541525657a6fc0b7a1b298295d7..fddabd5215a580d0c0c70e49d33064802ca7d704 100644
--- a/src/main/scala/leon/frontends/scalac/SaveImports.scala
+++ b/src/main/scala/leon/frontends/scalac/SaveImports.scala
@@ -12,7 +12,6 @@ import utils.{Position => LeonPosition, RangePosition => LeonRangePosition, Offs
trait SaveImports extends SubComponent {
import global._
- import global.definitions._
val phaseName = "imports"
diff --git a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala b/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
index 5d67a2286078187dfd52aa0ccce96a394ef2b83f..c3e2ba46cb3202f91ee03a191d42f48d1696a650 100644
--- a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
+++ b/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
@@ -6,9 +6,6 @@ package purescala
import Common._
import Definitions._
import Trees._
-import Extractors._
-import TreeOps._
-import TypeTrees._
object CompleteAbstractDefinitions extends TransformationPhase {
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 34e634e127388647ce591be2df48a8c0244a4039..8f1b5f57ff5aa810def235999063225ec3146b58 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -3,8 +3,6 @@
package leon
package purescala
-import utils._
-
object Constructors {
import Trees._
import TreeOps._
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index f056671dafc62d9d3b710dd0ee1cec784b2eaeaf..95942afe54d2468aa958afcbde291bcf68d15880 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -10,8 +10,6 @@ object Definitions {
import Common._
import Trees._
import TreeOps._
- import DefOps._
- import Extractors._
import TypeTrees._
import TypeTreeOps._
diff --git a/src/main/scala/leon/purescala/FunctionMapping.scala b/src/main/scala/leon/purescala/FunctionMapping.scala
index 8efa25c866eb363adc8bfb830186d5eebc6147cf..c11c80a39b090d0c6825c76370ac5d37649e24da 100644
--- a/src/main/scala/leon/purescala/FunctionMapping.scala
+++ b/src/main/scala/leon/purescala/FunctionMapping.scala
@@ -3,10 +3,8 @@
package leon
package purescala
-import Common._
import Definitions._
import Trees._
-import Extractors._
import TreeOps._
import TypeTrees._
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index f43546154830878fdde3e5f767e5cdb0ed425660..b82f1e71ed5115d5ca6f86fe49eeb73b6323dc49 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -3,21 +3,16 @@
package leon
package purescala
-import Common._
-import Trees._
-import TypeTrees._
-import Definitions._
-import DefOps._
-
-import utils._
-
-import java.lang.StringBuffer
-import PrinterHelpers._
-import TreeOps.{isListLiteral, simplestValue, variablesOf}
-import TypeTreeOps.leastUpperBound
-import Extractors._
-
-import synthesis.Witnesses._
+import leon.purescala.Common._
+import leon.purescala.DefOps._
+import leon.purescala.Definitions._
+import leon.purescala.Extractors._
+import leon.purescala.PrinterHelpers._
+import leon.purescala.TreeOps.{isListLiteral, simplestValue}
+import leon.purescala.Trees._
+import leon.purescala.TypeTreeOps.leastUpperBound
+import leon.purescala.TypeTrees._
+import leon.synthesis.Witnesses._
case class PrinterContext(
current: Tree,
@@ -556,7 +551,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
|"""
case PackageImport(pack) =>
- import DefOps._
+ import leon.purescala.DefOps._
val newPack = ( for (
scope <- ctx.scope;
unit <- unitOf(scope);
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 666f728d6dfae94c606b712766dc14beef3e82d6..e38418c0a247f5200e244f53c80bc807cf10d681 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -3,10 +3,6 @@
package leon
package purescala
-import Common._
-import Trees._
-import TypeTrees._
-import Definitions._
import Constructors._
import Extractors._
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index 525c5f26dddc25c769f64955845a17c6e3c6f9b7..74cb530c762ccf69a3e0d4a16ae59d568b0a39cb 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -6,10 +6,7 @@ package purescala
import Common._
import Definitions._
import Trees._
-import TypeTrees._
-import TreeOps._
import Extractors._
-import Constructors._
class ScopeSimplifier extends Transformer {
case class Scope(inScope: Set[Identifier] = Set(), oldToNew: Map[Identifier, Identifier] = Map(), funDefs: Map[FunDef, FunDef] = Map()) {
diff --git a/src/main/scala/leon/purescala/TreeNormalizations.scala b/src/main/scala/leon/purescala/TreeNormalizations.scala
index 3558ad5984eae73f95a7b00ab6d8ea870ac73fc1..73bc15aef2a6a47b5d31dda4365e5a84e1ec5ca8 100644
--- a/src/main/scala/leon/purescala/TreeNormalizations.scala
+++ b/src/main/scala/leon/purescala/TreeNormalizations.scala
@@ -6,10 +6,8 @@ package purescala
object TreeNormalizations {
import Common._
import TypeTrees._
- import Definitions._
import Trees._
import TreeOps._
- import Extractors._
/* TODO: we should add CNF and DNF at least */
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 5773f17166a0790ebf577750f33d0113cfd4b8d3..57e85d91ff30735202eb1b3059af9542b7d6d5cd 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -8,7 +8,6 @@ import utils._
/** AST definitions for Pure Scala. */
object Trees {
import Common._
- import TreeOps.variablesOf
import TypeTrees._
import TypeTreeOps._
import Definitions._
diff --git a/src/main/scala/leon/repair/RepairCostModel.scala b/src/main/scala/leon/repair/RepairCostModel.scala
index 25c19cc2a880746e4393ee819e1583d4b73e06b4..43e25dcb0201653ad19e2b67e9d7c1873a95067f 100644
--- a/src/main/scala/leon/repair/RepairCostModel.scala
+++ b/src/main/scala/leon/repair/RepairCostModel.scala
@@ -3,17 +3,10 @@
package leon
package repair
import synthesis._
-import Witnesses._
import synthesis.rules._
import repair.rules._
-import purescala.Definitions._
-import purescala.Trees._
-import purescala.DefOps._
-import purescala.TreeOps._
-import purescala.Extractors._
-
case class RepairCostModel(cm: CostModel) extends WrappedCostModel(cm, "Repair("+cm.name+")") {
import graph._
diff --git a/src/main/scala/leon/repair/RepairPhase.scala b/src/main/scala/leon/repair/RepairPhase.scala
index c6e1e4466677fd7ee37c17c9a2aef5625e74970b..d030327b5e52f7a0835bf6fc95ef6a397ce66c66 100644
--- a/src/main/scala/leon/repair/RepairPhase.scala
+++ b/src/main/scala/leon/repair/RepairPhase.scala
@@ -3,16 +3,9 @@
package leon
package repair
-import purescala.Common._
import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Constructors._
import purescala.DefOps._
-import java.io.FileWriter
-
object RepairPhase extends LeonPhase[Program, Program] {
val name = "Repair"
val description = "Repairing"
diff --git a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
index 22c4cb2716a63b1826ea8b72152ac4f26fb49e8b..4446f786c608f7166f8eda9cf0313d6978aae033 100644
--- a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
@@ -8,7 +8,6 @@ import leon.purescala.TypeTrees._
import leon.purescala.Definitions._
import leon.LeonContext
import leon.evaluators.RecursiveEvaluator
-import leon.synthesis._
/**
* This evaluator tracks all dependencies between function calls (.fullCallGraph)
diff --git a/src/main/scala/leon/solvers/combinators/DNFSolver.scala b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
index 755e9a6e22e0d4f17b1c25c2ba32071ea683172b..1fc16886f2304c2b62e70c09fa34166c11037b15 100644
--- a/src/main/scala/leon/solvers/combinators/DNFSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
@@ -5,11 +5,9 @@ package solvers
package combinators
import purescala.Common._
-import purescala.Definitions._
import purescala.Constructors._
import purescala.Trees._
import purescala.TreeOps._
-import purescala.TypeTrees._
class DNFSolver(val context: LeonContext,
underlyings: SolverFactory[Solver]) extends Solver {
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index f9fd8a7d4beaad38ebb352ba3406bba5484eb048..942f7519169dbbfbf60dea3281628a84a0fd454d 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -5,17 +5,12 @@ package solvers
package combinators
import purescala.Common._
-import purescala.Definitions._
import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
import utils.Interruptible
import scala.concurrent._
import scala.concurrent.duration._
-import scala.collection.mutable.{Map=>MutableMap}
-
import ExecutionContext.Implicits.global
class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext, solvers: Seq[SolverFactory[S]])
diff --git a/src/main/scala/leon/solvers/combinators/RewritingSolver.scala b/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
index c7579ef3bbfb8e7a03db617a95004721e6ee029d..5b089883b7a60cd08b27e8e6a61a18981bac1f1e 100644
--- a/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
@@ -5,10 +5,7 @@ package solvers
package combinators
import purescala.Common._
-import purescala.Definitions._
import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
abstract class RewritingSolver[+S <: Solver, T](underlying: S) {
val context = underlying.context
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 6ff60b5deab6a3082e74aafdad381a9b8d2566c7..3239bdd9794875141f65cd941da85cc7ea5570ef 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -9,7 +9,6 @@ import purescala.Definitions._
import purescala.Constructors._
import purescala.Trees._
import purescala.TreeOps._
-import purescala.TypeTrees._
import solvers.templates._
import utils.Interruptible
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 91a074d5eb7f2e00a2f71c06caf5b2787987cec7..74cf6d03106e57433153bce6e745e595af470ea7 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -2,7 +2,6 @@ package leon
package solvers
package smtlib
-import utils.Interruptible
import purescala._
import Common._
import Trees.{Assert => _, _}
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index 841247dd2b2bc15785f99e2c626708dc31e75f70..72ac87a52210ba779859ff14cc4171bac3b44dca 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -3,12 +3,10 @@
package leon
package synthesis
-import purescala.Common._
import purescala.Definitions._
import purescala.Constructors._
import purescala.Trees._
import purescala.TreeOps._
-import purescala.DefOps._
import Witnesses._
case class ChooseInfo(fd: FunDef,
diff --git a/src/main/scala/leon/synthesis/ConvertWithOracles.scala b/src/main/scala/leon/synthesis/ConvertWithOracles.scala
index 8b130c7ad1a9fbf0d369dafac6e3dff1d614fe40..e35c6e58127835bbc476b68886c4e4b53918519c 100644
--- a/src/main/scala/leon/synthesis/ConvertWithOracles.scala
+++ b/src/main/scala/leon/synthesis/ConvertWithOracles.scala
@@ -3,7 +3,6 @@
package leon
package synthesis
-import purescala.Common._
import purescala.Trees._
import purescala.TreeOps._
import purescala.Definitions._
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index cdabf6eb6085795b07e819eda2ec2cb84ed157f6..0e81f6f6c19f8ea6c27e5b35d8a19f90aaaa9f2e 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -5,7 +5,7 @@ package synthesis
import purescala.Trees._
import purescala.Common.Tree
-import purescala.Definitions.{Definition,FunDef}
+import purescala.Definitions.Definition
import purescala.ScalaPrinter
import purescala.PrinterOptions
import purescala.PrinterContext
diff --git a/src/main/scala/leon/synthesis/PartialSolution.scala b/src/main/scala/leon/synthesis/PartialSolution.scala
index f76355b7851f59d4515fbfbb0feaa3e6504d4f22..2f05eb1a723f2005b36a0dbf4a6edcee391fbdd0 100644
--- a/src/main/scala/leon/synthesis/PartialSolution.scala
+++ b/src/main/scala/leon/synthesis/PartialSolution.scala
@@ -4,9 +4,6 @@ package leon
package synthesis
import purescala.Trees._
-import purescala.TreeOps._
-import purescala.DefOps._
-import purescala.Common._
import graph._
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 71c12af51a5874121752883755174a751c40239b..297b3210fde52ba4dc89d714743cd6242b7343aa 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -4,7 +4,6 @@ package leon
package synthesis
import leon.purescala.Trees._
-import leon.purescala.Definitions._
import leon.purescala.TreeOps._
import leon.purescala.TypeTrees._
import leon.purescala.Common._
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 3ae642fc327dbdd1684f2a39cfdd3c8f8db220d9..a4a0686c1c6e3a4e63893c5f29bc46558c5e60e7 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -7,7 +7,6 @@ import purescala.Common._
import purescala.Trees._
import purescala.TypeTrees._
import purescala.TreeOps._
-import purescala.Constructors._
import rules._
abstract class Rule(val name: String) extends RuleDSL {
diff --git a/src/main/scala/leon/synthesis/SearchContext.scala b/src/main/scala/leon/synthesis/SearchContext.scala
index 853314f08e2b3fd226f1a8edd29af2b2a7bb5ca0..531ae4514ed593b02c177c7f5278a92702b5d534 100644
--- a/src/main/scala/leon/synthesis/SearchContext.scala
+++ b/src/main/scala/leon/synthesis/SearchContext.scala
@@ -3,7 +3,6 @@
package leon
package synthesis
-import purescala.Trees.Choose
import graph._
/**
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index bc93ce0c7849e8b2fa99e699e1f64d6a01061530..2eb1e73f1352ecb703f473451e2ad5916bce065f 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -8,10 +8,7 @@ import purescala.Trees._
import purescala.TypeTrees.{TypeTree,TupleType}
import purescala.Definitions._
import purescala.TreeOps._
-import purescala.ScopeSimplifier
import purescala.Constructors._
-import solvers.z3._
-import solvers._
import leon.utils.Simplifiers
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 0944851f5a99e73bda0b601e7c099fcffc45aab6..a6f794ca73faff97ea4bd303455dab5258253421 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -3,10 +3,7 @@ package leon
package synthesis
import purescala.TreeOps._
-import solvers.z3._
-import purescala.Trees._
-import purescala.Common._
import purescala.ScalaPrinter
import purescala.Definitions.{Program, FunDef}
import leon.utils.ASCIIHelpers
diff --git a/src/main/scala/leon/synthesis/graph/DotGenerator.scala b/src/main/scala/leon/synthesis/graph/DotGenerator.scala
index 4694044cc17a99056415f78f96953dad7bf80caa..c4ee0d758c7012bf8e442f7087c8b472227fb825 100644
--- a/src/main/scala/leon/synthesis/graph/DotGenerator.scala
+++ b/src/main/scala/leon/synthesis/graph/DotGenerator.scala
@@ -2,8 +2,6 @@ package leon.synthesis.graph
import java.io.{File, FileWriter, BufferedWriter}
-import leon.synthesis.Histogram
-
class DotGenerator(g: Graph) {
private[this] var _nextID = 0
diff --git a/src/main/scala/leon/synthesis/graph/Search.scala b/src/main/scala/leon/synthesis/graph/Search.scala
index 82e3e1175fe269b07203984478f2ffb607ae0764..b5f37629f5fdd987e73e4aaf1a46739c0131e72f 100644
--- a/src/main/scala/leon/synthesis/graph/Search.scala
+++ b/src/main/scala/leon/synthesis/graph/Search.scala
@@ -4,9 +4,6 @@ package graph
import scala.annotation.tailrec
-import purescala.Trees.Choose
-import leon.utils.StreamUtils.cartesianProduct
-
import scala.collection.mutable.ArrayBuffer
import leon.utils.Interruptible
import java.util.concurrent.atomic.AtomicBoolean
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 3e11b4d656ba9b5bed3562ca280417be3095d965..eff8465aa0b921d3e28aac64ea9945b42cbcf58a 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -4,7 +4,6 @@ package leon
package synthesis
package rules
-import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
import purescala.Constructors._
diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
index 1259a50a79e463e064d7ac39282ad22e26b0b10d..d08a1e07724800020f76e692f33e169128aba8b5 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
@@ -4,23 +4,11 @@ package leon
package synthesis
package rules
-import solvers._
-import solvers.z3._
-
import purescala.Trees._
import purescala.Common._
-import purescala.Definitions._
import purescala.TypeTrees._
-import purescala.TreeOps._
-import purescala.TypeTreeOps._
-import purescala.Extractors._
-import purescala.ScalaPrinter
import purescala.Constructors._
-
-import scala.collection.mutable.{Map=>MutableMap, ArrayBuffer}
-
import evaluators._
-import datagen._
import codegen.CodeGenParams
import utils._
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index b09dbd703222f6bf02a453f28b91b59bebe7ecac..203a35b7df3589d4658e5865c95beddf47cafc1a 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -5,8 +5,6 @@ package synthesis
package rules
import purescala.Trees._
-import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
case object CaseSplit extends Rule("Case-Split") {
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 6d989c4ef4126e8391a47a9fa048fcd7d8efd92b..4cf48c204279c34277f6c98bb04e07a1a9006554 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -4,23 +4,7 @@ package leon
package synthesis
package rules
-import purescala.Trees._
import purescala.TypeTrees._
-import purescala.Common._
-import purescala.Definitions._
-import utils.Helpers._
-import purescala.TypeTrees._
-import purescala.TreeOps._
-import purescala.DefOps._
-import purescala.TypeTreeOps._
-import purescala.Extractors._
-import purescala.ScalaPrinter
-
-import scala.collection.mutable.{Map=>MutableMap}
-
-import evaluators._
-import datagen._
-import codegen.CodeGenParams
import utils._
diff --git a/src/main/scala/leon/synthesis/rules/Cegless.scala b/src/main/scala/leon/synthesis/rules/Cegless.scala
index 914003fec53cabbed959e445865634e81da1789a..893657d4cfa45fe2407fcbb30b7f241e2b0b6be7 100644
--- a/src/main/scala/leon/synthesis/rules/Cegless.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegless.scala
@@ -4,11 +4,8 @@ package leon
package synthesis
package rules
-import purescala.Trees._
import purescala.TreeOps._
import purescala.TypeTrees._
-import purescala.Common._
-import purescala.Definitions._
import purescala.Extractors._
import utils._
import utils.ExpressionGrammars._
diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
index 4cb86162496913c8b69fb7e8b9925c9ed4626436..1ec3858fc1a2c291199cb2b3bd7b40b161e16766 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
@@ -8,8 +8,6 @@ import purescala.Trees._
import purescala.Definitions._
import purescala.Common._
import purescala.TypeTrees._
-import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
case object DetupleOutput extends Rule("Detuple Out") {
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
index 53c69e252d5423cf58becdbf066f6386b8c9e667..812a0c11901cdbb017d2d64f58e8ba01209013dd 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -5,8 +5,6 @@ package synthesis
package rules
import purescala.Trees._
-import purescala.TypeTrees._
-import purescala.TreeOps._
import purescala.Extractors._
import purescala.Constructors._
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index 0a3be81d44929320b693987794a5ea0655f692f5..087c9d9d14889386f79edab803a468c509605fbf 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -5,10 +5,6 @@ package synthesis
package rules
import purescala.Trees._
-import purescala.Common._
-import purescala.TypeTrees._
-import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
import solvers._
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 43d2ead6204b5e87c384a5aee9a6f12be5f017ce..a2a6f9955eefe6b673c3a06908d68fbb189fb115 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -6,9 +6,7 @@ package rules
import solvers._
import purescala.Trees._
-import purescala.TypeTrees._
import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
case object Ground extends Rule("Ground") {
diff --git a/src/main/scala/leon/synthesis/rules/IfSplit.scala b/src/main/scala/leon/synthesis/rules/IfSplit.scala
index dff14901ad8d9fa0150cc1afaca98a18ecfff2f4..ea115e42c17d5ccae1a37d6b821a46898c01dc7a 100644
--- a/src/main/scala/leon/synthesis/rules/IfSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/IfSplit.scala
@@ -6,7 +6,6 @@ package rules
import purescala.Trees._
import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
case object IfSplit extends Rule("If-Split") {
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index a71574fdaf243c388014f0c73c1f49773e512db1..f6edb6bb2a5f3403575a30f67f342beec18ad344 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -6,10 +6,6 @@ package rules
import purescala.Trees._
import purescala.TypeTrees._
-import purescala.Common._
-import purescala.TypeTrees._
-import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
import solvers._
diff --git a/src/main/scala/leon/synthesis/rules/InlineHoles.scala b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
index 7e1cd161186b1deb2547f50ed79f0c4c0b0b7c79..de4c61916c0b86b337c90a02d3a409253695038d 100644
--- a/src/main/scala/leon/synthesis/rules/InlineHoles.scala
+++ b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
@@ -6,16 +6,12 @@ package rules
import scala.annotation.tailrec
-import leon.utils._
-
import solvers._
import purescala.Common._
import purescala.Definitions._
import purescala.Trees._
import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Extractors._
import purescala.Constructors._
case object InlineHoles extends Rule("Inline-Holes") {
diff --git a/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala b/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala
index 637bdeeb96c0092de7eb3e9d31c6ee43ef3365b9..f87751e0d60421e14eb8ae67dae1a8bdaf580578 100644
--- a/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala
@@ -5,8 +5,6 @@ package synthesis
package rules
import purescala.Trees._
-import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
case object InnerCaseSplit extends Rule("Inner-Case-Split"){
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index bc46805aeee24d9b9fb16db30ec2ca0c3dac551b..13d79428e78ca1ea7a2474a3c545033b5fe30307 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -5,9 +5,7 @@ package synthesis
package rules
import purescala.Trees._
-import purescala.TypeTrees._
import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
import solvers._
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala b/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
index d6ccc416fd183f45f05e5734f16c89b9f1d46a2b..299bdeb0f75e2e3a893e9da1de384cdd0247290b 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
@@ -4,13 +4,9 @@ package leon
package synthesis
package rules
-import purescala.Common._
import purescala.Trees._
import purescala.Extractors._
import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Definitions._
case object OptimisticInjection extends Rule("Opt. Injection") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
diff --git a/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala b/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
index e79d857d403d6cd184c2d73d9f334e09b5a4b5ef..b8877d78356021d189d4f562403982f82309e7c9 100644
--- a/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
@@ -4,13 +4,9 @@ package leon
package synthesis
package rules
-import purescala.Common._
import purescala.Trees._
import purescala.Extractors._
import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Definitions._
case object SelectiveInlining extends Rule("Sel. Inlining") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
diff --git a/src/main/scala/leon/synthesis/rules/Tegis.scala b/src/main/scala/leon/synthesis/rules/Tegis.scala
index 273e170ecbf8c30aeb84bbfe63bca216e916f37f..06bf87c601067623faae922a556e9bd23278f757 100644
--- a/src/main/scala/leon/synthesis/rules/Tegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Tegis.scala
@@ -4,15 +4,7 @@ package leon
package synthesis
package rules
-import purescala.Trees._
-import purescala.Common._
-import purescala.Definitions._
import purescala.TypeTrees._
-import purescala.Constructors._
-
-import evaluators._
-import datagen._
-
import utils._
case object TEGIS extends TEGISLike[TypeTree]("TEGIS") {
diff --git a/src/main/scala/leon/synthesis/rules/TegisLike.scala b/src/main/scala/leon/synthesis/rules/TegisLike.scala
index 51bbf8a6e8614345964c330d4deb418d3d28ba2a..864f5302b2797a7b511ead9f0633585ca0561711 100644
--- a/src/main/scala/leon/synthesis/rules/TegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TegisLike.scala
@@ -5,19 +5,14 @@ package synthesis
package rules
import purescala.Trees._
-import purescala.Common._
-import purescala.Definitions._
import purescala.TypeTrees._
-import purescala.Extractors._
import purescala.Constructors._
import evaluators._
-import datagen._
import codegen.CodeGenParams
import utils._
-import bonsai._
import bonsai.enumerators._
abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
diff --git a/src/main/scala/leon/synthesis/rules/Tegless.scala b/src/main/scala/leon/synthesis/rules/Tegless.scala
index e1880752a41c2e1c373aed0027eb73e2ddfb6a33..f182305ac23e504d6d62dc783d020bc954699f4d 100644
--- a/src/main/scala/leon/synthesis/rules/Tegless.scala
+++ b/src/main/scala/leon/synthesis/rules/Tegless.scala
@@ -4,11 +4,7 @@ package leon
package synthesis
package rules
-import purescala.Trees._
-import purescala.TreeOps._
import purescala.TypeTrees._
-import purescala.Common._
-import purescala.Definitions._
import purescala.Extractors._
import utils._
import utils.ExpressionGrammars._
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index e41d3f64b60c7fc6b41afa8e4af48dac25fc5ed2..3b42bf379b6fa8c1f717f7a5added8e5c5bd5b4b 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -6,7 +6,6 @@ package rules
import purescala.Trees._
import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index c0e865b574fcc5c32eb268a42133d6de07747c8b..db2e8b6d163ed103b81f8ef493c950bb93a772be 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -5,7 +5,6 @@ package synthesis
package rules
import purescala.Trees._
-import purescala.TypeTrees._
import purescala.TreeOps._
import purescala.Extractors._
import purescala.Constructors._
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index b463a2725dfea5d8873952196c05fab5b13843f2..467a106436b2b8c3765117ed59bd8469463fa7ec 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -4,9 +4,7 @@ package leon
package synthesis
package rules
-import purescala.Trees._
import purescala.TreeOps._
-import purescala.Extractors._
case object UnusedInput extends NormalizingRule("UnusedInput") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
diff --git a/src/main/scala/leon/synthesis/utils/Helpers.scala b/src/main/scala/leon/synthesis/utils/Helpers.scala
index 88b154c5b9543661f4f3b0b5983f6b08061a6199..617ae9462543a93888beba3f3c277e951ee4fe4c 100644
--- a/src/main/scala/leon/synthesis/utils/Helpers.scala
+++ b/src/main/scala/leon/synthesis/utils/Helpers.scala
@@ -9,7 +9,6 @@ import purescala.TypeTrees._
import purescala.Extractors._
import purescala.TypeTreeOps._
import purescala.Trees._
-import purescala.TreeOps._
import purescala.DefOps._
import purescala.Common._
import Witnesses._
diff --git a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
index 0034e0588f5344eda2a415f93b3ad80585a9a7de..658a4b532a7ca8c0f2b8368f6876e23f08e2f9fb 100644
--- a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
+++ b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
@@ -4,11 +4,7 @@ package leon
package synthesis
package utils
-import purescala.Trees._
-import purescala.TreeOps._
import purescala.Definitions._
-import solvers.z3._
-import solvers.Solver
object SynthesisProblemExtractionPhase extends LeonPhase[Program, (Program, Map[FunDef, Seq[ChooseInfo]])] {
val name = "Synthesis Problem Extraction"
diff --git a/src/main/scala/leon/termination/ComponentProcessor.scala b/src/main/scala/leon/termination/ComponentProcessor.scala
index b541a7477ad5b5f1a8e5f85ceca408a240542389..6fd32320cd82a4496b4761a6dc1f81f21abf1908 100644
--- a/src/main/scala/leon/termination/ComponentProcessor.scala
+++ b/src/main/scala/leon/termination/ComponentProcessor.scala
@@ -3,7 +3,6 @@
package leon
package termination
-import purescala.TreeOps._
import purescala.Definitions._
import scala.collection.mutable.{Map => MutableMap}
diff --git a/src/main/scala/leon/termination/RecursionProcessor.scala b/src/main/scala/leon/termination/RecursionProcessor.scala
index 0238612e41b3843afab8bdc67e52503a7451c315..89824297a36a1bae532bd441b9c60fe8c60ba939 100644
--- a/src/main/scala/leon/termination/RecursionProcessor.scala
+++ b/src/main/scala/leon/termination/RecursionProcessor.scala
@@ -5,7 +5,6 @@ package termination
import purescala.Trees._
import purescala.Common._
-import purescala.Definitions._
import scala.annotation.tailrec
diff --git a/src/main/scala/leon/termination/RelationBuilder.scala b/src/main/scala/leon/termination/RelationBuilder.scala
index 3f62a4a5507caa708fd468b1fe8e43dc2f1d3b96..c14a56a585efce8efdaa7143014f8d87f19dc732 100644
--- a/src/main/scala/leon/termination/RelationBuilder.scala
+++ b/src/main/scala/leon/termination/RelationBuilder.scala
@@ -5,8 +5,6 @@ package termination
import purescala.Trees._
import purescala.TreeOps._
-import purescala.Extractors._
-import purescala.Common._
import purescala.Definitions._
import scala.collection.mutable.{Map => MutableMap}
diff --git a/src/main/scala/leon/termination/RelationComparator.scala b/src/main/scala/leon/termination/RelationComparator.scala
index eb886d5eaa53e543338d90e00101227b17e39f93..d50458d329bee652614bb888bca4471ea44bec33 100644
--- a/src/main/scala/leon/termination/RelationComparator.scala
+++ b/src/main/scala/leon/termination/RelationComparator.scala
@@ -4,10 +4,6 @@ package leon
package termination
import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Definitions._
-import purescala.Common._
trait RelationComparator { self : StructuralSize =>
diff --git a/src/main/scala/leon/utils/OracleTraverser.scala b/src/main/scala/leon/utils/OracleTraverser.scala
index d70d1fb5d0a9f024227924636f8748f2c4b84982..8c40f5f9eb2286d3319cc3672fbc770be4584c8b 100644
--- a/src/main/scala/leon/utils/OracleTraverser.scala
+++ b/src/main/scala/leon/utils/OracleTraverser.scala
@@ -6,7 +6,6 @@ package utils
import purescala.Trees._
import purescala.TypeTrees._
import purescala.Definitions._
-import utils._
case class OracleTraverser(oracle: Expr, tpe: TypeTree, program: Program) {
private def call(name: String) = {
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 6ecd9f720dc1993fad20b1e346debfc1b6ecaecb..e297bcd16df0021cece3f100917f0378777cb1dd 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -3,10 +3,8 @@
package leon
package verification
-import purescala.Common._
import purescala.Trees._
import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Definitions._
import purescala.Constructors._
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index b50bb42122c8767ccd5c2f749b1f6c0748aeb3f9..6844f776e38d68fa9027e4bab1104a1c46aedbad 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -3,7 +3,6 @@
package leon
package utils
-import purescala.Common._
import purescala.Trees._
import xlang.Trees._
import purescala.TreeOps._
diff --git a/src/main/scala/leon/verification/VerificationContext.scala b/src/main/scala/leon/verification/VerificationContext.scala
index c28f2ca399c932bb702f7ed780cfc86c5e50d9d6..f2837ee11dd13832c69e4e3a122eb93dd7d1f301 100644
--- a/src/main/scala/leon/verification/VerificationContext.scala
+++ b/src/main/scala/leon/verification/VerificationContext.scala
@@ -6,8 +6,6 @@ package verification
import purescala.Definitions.Program
import solvers._
-import java.util.concurrent.atomic.AtomicBoolean
-
case class VerificationContext (
context: LeonContext,
program: Program,
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index 5c4b314ea7426211edb23de946372a07c959c682..2f03dbaa417028e1e2e7bee36625eb1a05382c02 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -9,7 +9,6 @@ import leon.purescala.Definitions._
import leon.purescala.Trees._
import leon.xlang.Trees._
import leon.purescala.Extractors._
-import leon.purescala.Constructors._
import leon.purescala.TypeTrees._
object ArrayTransformation extends TransformationPhase {
diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index e90c537070c87e6c9f1ec13931535f290cad0076..9828e45f0098cd8b485c93aa5212d4d1b3a03c4f 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -8,7 +8,6 @@ import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Trees._
import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
import leon.xlang.Trees._
object EpsilonElimination extends TransformationPhase {
diff --git a/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
index 0c6f11a8d48b650bea8c6b93c8ec9a76ac6e82aa..8484b9840874376290c1391369becb585a13e9d4 100644
--- a/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
+++ b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
@@ -3,12 +3,8 @@
package leon
package xlang
-import purescala.Common._
-import purescala.TypeTrees._
-import purescala.Trees._
import purescala.TreeOps.collect
import purescala.Definitions._
-import purescala.Constructors._
import utils.Position
diff --git a/src/main/scala/leon/xlang/TreeOps.scala b/src/main/scala/leon/xlang/TreeOps.scala
index ce2944a8f0a575e1a285e39409e0834ac7bab0b0..b76186d296a152a6eee0f57a1d0c7d7676e3c456 100644
--- a/src/main/scala/leon/xlang/TreeOps.scala
+++ b/src/main/scala/leon/xlang/TreeOps.scala
@@ -3,13 +3,9 @@
package leon
package xlang
-import purescala.Common._
-import purescala.TypeTrees._
-import purescala.Definitions._
import purescala.Trees._
import xlang.Trees._
import purescala.TreeOps._
-import purescala.Extractors._
object TreeOps {
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 6c3864204b2431085a27ccabb5cbac6fdf321aca..e3d23d2cce5f557ab9e41048371bc00723fb9056 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -6,9 +6,8 @@ package xlang
import purescala.Common._
import purescala.TypeTrees._
import purescala.Trees._
-import purescala.Definitions._
import purescala.Extractors._
-import purescala.{PrettyPrinter, PrettyPrintable, ScalaPrinter, PrinterContext}
+import purescala.{PrettyPrintable, PrinterContext}
import utils._
object Trees {