diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index 8302168801bdae6e6b3a0857dd785c16ebb5bedb..f02cce59c78a4e81b3071248b747127fdce4797d 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -3,7 +3,6 @@
 package leon
 package solvers.smtlib
 
-import purescala.Common.Identifier
 import purescala.Definitions.Program
 import purescala.Expressions.Expr
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
index b882bafe2fd9a9e82b3d56dd987b16a717fd7e5f..737b8535cdb684123163576400d8858adf4fd944 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
@@ -4,12 +4,8 @@ package leon
 package solvers
 package smtlib
 
-import purescala.Common._
 import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
 import purescala.Constructors._
-import purescala.Types._
 import purescala.Definitions._
 import purescala.DefOps.typedTransitiveCallees
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index d5515b42e0e2d51d9a1e1cceb1e3a0bac291550e..620a294edf2ef6b6df0c60d697380958f7ccc23d 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -6,7 +6,6 @@ package smtlib
 
 import purescala.Common._
 import purescala.Expressions._
-import purescala.Extractors._
 import purescala.Constructors._
 import purescala.Types._
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
index fbaa73cc2a417addc2ae1de2354ed13d89b8758b..ba0187239bbd71e75cc656928fa451fa308b809c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
@@ -5,7 +5,6 @@ package solvers
 package smtlib
 
 import purescala.Common.Identifier
-import purescala.Expressions.Expr
 import verification.VC
 
 trait SMTLIBQuantifiedSolver {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
index 7aa281b677f13b65df6008508575f8dfb7a0c9e7..b6d6fbfb313a15deb9030424da48ba56a65c4524 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
@@ -8,11 +8,8 @@ import purescala.Expressions._
 import purescala.Definitions._
 import purescala.Constructors._
 import purescala.ExprOps._
-import purescala.DefOps.typedTransitiveCallees
 
-import _root_.smtlib.parser.Commands.{Assert => SMTAssert, FunDef => _, _}
-import _root_.smtlib.parser.Terms.{Exists => SMTExists, Forall => SMTForall, _ }
-import _root_.smtlib.theories.Core.Equals
+import _root_.smtlib.parser.Commands.{Assert => _, FunDef => _, _}
 
 trait SMTLIBQuantifiedTarget extends SMTLIBTarget {
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index edb558e95cf53b540cca505ee89307ed2473bf59..05476ac11bd106e1d313695757445ce40b1efd1e 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -4,21 +4,14 @@ package leon
 package solvers
 package smtlib
 
-import utils._
 import purescala.Common._
 import purescala.Expressions._
-import purescala.Extractors._
 import purescala.ExprOps._
-import purescala.Types._
-import purescala.Constructors._
 import purescala.Definitions._
 
-import _root_.smtlib.common._
 import _root_.smtlib.parser.Commands.{Assert => SMTAssert, _}
 import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
 import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
-import _root_.smtlib.theories._
-import _root_.smtlib.interpreters.ProcessInterpreter
 
 abstract class SMTLIBSolver(val context: LeonContext, val program: Program) 
                            extends Solver with SMTLIBTarget with NaiveAssumptionSolver {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
index 0735b2396ba7f5b8b64cbe87fc8850a71d74da7e..4c8eedce5fb981ff037349eba6b0f6e69d595e88 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
@@ -4,19 +4,13 @@ package leon
 package solvers
 package smtlib
 
-import purescala.Common._
 import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
 import purescala.Constructors._
-import purescala.Types._
 import purescala.Definitions._
 import purescala.DefOps.typedTransitiveCallees
 
 import _root_.smtlib.parser.Commands.{Assert => SMTAssert, FunDef => _, _}
 import _root_.smtlib.parser.Terms.{Exists => SMTExists, Forall => SMTForall, _ }
-import _root_.smtlib.theories.Core.{Equals => SMTEquals}
-import _root_.smtlib.parser.Commands._
 
 trait SMTLIBZ3QuantifiedTarget extends SMTLIBZ3Target with SMTLIBQuantifiedTarget {
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index 0e289ff80468380744e56d8741baa293cee0eb0a..86cf40f474e62859acfd1fe2c0953e588590d6df 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -8,10 +8,10 @@ import purescala.Definitions.Program
 import purescala.Common.Identifier
 import purescala.Expressions.Expr
 
-import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
+import _root_.smtlib.parser.Terms.{Identifier => _, _}
 import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
 import _root_.smtlib.parser.CommandsResponses.GetModelResponseSuccess
-import _root_.smtlib.theories.Core.{Equals => SMTEquals, _}
+import _root_.smtlib.theories.Core.{Equals => _, _}
 
 class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolver(context, program) with SMTLIBZ3Target {
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 657100814d32d67f40979672f94a455a6a63ce02..eac8f47f948f5eceb8c728c900c15d31fc8fd310 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -6,18 +6,15 @@ package smtlib
 
 import purescala.Common._
 import purescala.Expressions._
-import purescala.Extractors._
 import purescala.Constructors._
 import purescala.Types._
 
 import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
 import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
 import _root_.smtlib.interpreters.Z3Interpreter
-import _root_.smtlib.parser.CommandsResponses.GetModelResponseSuccess
 import _root_.smtlib.theories.Core.{Equals => SMTEquals, _}
 import _root_.smtlib.theories.ArraysEx
 
-
 trait SMTLIBZ3Target extends SMTLIBTarget {
 
   def targetName = "z3"