diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 6da84692bb895eccb0fa7e785f2a7fa8839dc8c7..8cb2b732e1cb8f4558d8e3da3e91d0255c1b4fcb 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -4,11 +4,12 @@ package leon
 package purescala
 
 import utils._
+import Expressions.Variable
+import Types._
 import Definitions.Definition
 
 object Common {
-  import Expressions.Variable
-  import Types._
+
 
   abstract class Tree extends Positioned with Serializable {
     def copiedFrom(o: Tree): this.type = {
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index dcca26675e3a723946e4d7f6864a824f66d20151..24f43d7569eb4213fec4f1199a63e0a000d619f2 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -3,13 +3,14 @@
 package leon
 package purescala
 
+import Expressions._
+import ExprOps._
+import Definitions._
+import TypeOps._
+import Common._
+import Types._
+
 object Constructors {
-  import Expressions._
-  import ExprOps._
-  import Definitions._
-  import TypeOps._
-  import Common._
-  import Types._
 
   // If isTuple, the whole expression is returned. This is to avoid a situation
   // like tupleSelect(tupleWrap(Seq(Tuple(x,y))),1) -> x, which is not expected.
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 680e7c0993f50ed7de08d71446b4f53547419c14..e7dd7e202c8ae6e1cc35467497fccafc6acce4af 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -3,15 +3,14 @@
 package leon
 package purescala
 
-import scala.collection.generic.CanBuildFrom
 import utils.Library
+import Common._
+import Expressions._
+import ExprOps._
+import Types._
+import TypeOps._
 
 object Definitions {
-  import Common._
-  import Expressions._
-  import ExprOps._
-  import Types._
-  import TypeOps._
 
   sealed abstract class Definition extends Tree {
     
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 2f7f2ab35a120be39f6bae7216edaae39f48e151..fe049f5af59c74c55f417814ca8eec06517dd283 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -3,21 +3,19 @@
 package leon
 package purescala
 
+import Common._
+import Types._
+import Definitions._
+import Expressions._
+import TypeOps._
+import Extractors._
+import Constructors._
+import DefOps._
 import utils.Simplifiers
-
-import leon.solvers._
-
+import solvers._
 import scala.collection.concurrent.TrieMap
 
 object ExprOps {
-  import Common._
-  import Types._
-  import Definitions._
-  import Expressions._
-  import TypeOps._
-  import Extractors._
-  import Constructors._
-  import DefOps._
 
   /**
    * Core API
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 32e56f1da9d27ec963ac833333ccfba8a0063422..ec4038abc9f392e3ec1372940a9c08e7b1944881 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -3,21 +3,18 @@
 package leon
 package purescala
 
-import utils._
+import Common._
+import Types._
+import TypeOps._
+import Definitions._
+import Extractors._
+import Constructors._
 
 /** AST definitions for Pure Scala. */
 object Expressions {
-  import Common._
-  import Types._
-  import TypeOps._
-  import Definitions._
-  import Extractors._
-  import Constructors._
-
 
   /* EXPRESSIONS */
   abstract class Expr extends Tree with Typed with Serializable {
-    // All Expr's have constant type
     override val getType: TypeTree
   }
 
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 9f705f388974c0fbb087ce37c71cfa129272f59e..8cde59fe888ee25caf203c36da9dd60a8acb88e3 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -4,15 +4,13 @@ package leon
 package purescala
 
 import Expressions._
+import Common._
+import Types._
+import Definitions._
+import Constructors._
+import ExprOps._
 
 object Extractors {
-  import Common._
-  import Types._
-  import TypeOps._
-  import Definitions._
-  import Extractors._
-  import Constructors._
-  import ExprOps._
 
   object UnaryOperator {
     def unapply(expr: Expr) : Option[(Expr,(Expr)=>Expr)] = expr match {
diff --git a/src/main/scala/leon/purescala/RestoreMethods.scala b/src/main/scala/leon/purescala/RestoreMethods.scala
index 353bb8697c8de6eba4746bd9394c5e129f3ac172..64eb74bfada2bfb28a1291d15611f0a9f8ff1ca1 100644
--- a/src/main/scala/leon/purescala/RestoreMethods.scala
+++ b/src/main/scala/leon/purescala/RestoreMethods.scala
@@ -1,12 +1,12 @@
-package leon.purescala
+package leon
+package purescala
 
-import leon._
-import leon.purescala.Definitions._
-import leon.purescala.Common._
-import leon.purescala.Expressions._
-import leon.purescala.ExprOps.{replaceFromIDs,functionCallsOf}
-import leon.purescala.DefOps.{applyOnFunDef,preMapOnFunDef}
-import leon.purescala.Types._
+import Definitions._
+import Common._
+import Expressions._
+import ExprOps.{replaceFromIDs,functionCallsOf}
+import DefOps.{applyOnFunDef,preMapOnFunDef}
+import Types._
 import utils.GraphOps._
 
 object RestoreMethods extends TransformationPhase {
diff --git a/src/main/scala/leon/purescala/Transformer.scala b/src/main/scala/leon/purescala/Transformer.scala
index 46314714fb74038761b6ee96cd81d98b9270a72e..d4a307d99b24d35e22b367779912b417fde67b00 100644
--- a/src/main/scala/leon/purescala/Transformer.scala
+++ b/src/main/scala/leon/purescala/Transformer.scala
@@ -5,7 +5,6 @@ package purescala
 
 import purescala.Expressions._
 
-
 trait Transformer {
   def transform(e: Expr): Expr
 }
diff --git a/src/main/scala/leon/purescala/TreeNormalizations.scala b/src/main/scala/leon/purescala/TreeNormalizations.scala
index 7b80083e498e882cbd899e282c4b444d0dd469d3..755b2c784341658f734a4e08dafec6b1c5c7d78e 100644
--- a/src/main/scala/leon/purescala/TreeNormalizations.scala
+++ b/src/main/scala/leon/purescala/TreeNormalizations.scala
@@ -3,11 +3,12 @@
 package leon
 package purescala
 
+import Common._
+import Types._
+import Expressions._
+import ExprOps._
+
 object TreeNormalizations {
-  import Common._
-  import Types._
-  import Expressions._
-  import ExprOps._
 
   /* TODO: we should add CNF and DNF at least */
 
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 14eba4fe91daca7e24feb94f7692aaf8c538ebe2..2fca2ea893ea15a7efa038199ad8049626a74439 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -3,7 +3,6 @@
 package leon
 package purescala
 
-import ExprOps.postMap
 import Types._
 import Definitions._
 import Common._
diff --git a/src/main/scala/leon/synthesis/rules/CEGLESS.scala b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
index 893657d4cfa45fe2407fcbb30b7f241e2b0b6be7..a746dcfddc3d8ad7d9493daa1b57a62c70d269a5 100644
--- a/src/main/scala/leon/synthesis/rules/CEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Extractors._
 import utils._
 import utils.ExpressionGrammars._
diff --git a/src/main/scala/leon/synthesis/rules/TEGLESS.scala b/src/main/scala/leon/synthesis/rules/TEGLESS.scala
index f182305ac23e504d6d62dc783d020bc954699f4d..c2a4cc4c62d10955032b1c643a64da7eaa4de6bb 100644
--- a/src/main/scala/leon/synthesis/rules/TEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGLESS.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.TypeTrees._
+import purescala.Types._
 import purescala.Extractors._
 import utils._
 import utils.ExpressionGrammars._
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index c849441e092c48cdb66bc76d7d52eec434576fbc..143f6a5cd48aaaa96f4ca71c78d852d99f101c95 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -117,7 +117,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
         reporter.synchronized {
           def title(s : String) = s"   => $s"
           solverResult match {
-            case _ if interruptManager.isInterrupted() =>
+            case _ if interruptManager.isInterrupted =>
               reporter.warning(title("CANCELLED"))
               vcInfo.time = Some(dt)
               false
@@ -158,14 +158,14 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
     
     if (checkInParallel) {
       val allVCsPar = (for {(_, vcs) <- vcs.toSeq; vcInfo <- vcs} yield vcInfo).par
-      for (vc <- allVCsPar if !interruptManager.isInterrupted() && !interrupt) {
+      for (vc <- allVCsPar if !interruptManager.isInterrupted && !interrupt) {
         checkVC(vc)
         interrupt = interruptOn(vc)
       }
     } else {
       for {
         (funDef, vcs) <- vcs.toSeq.sortWith((a,b) => a._1.getPos < b._1.getPos)
-        vc <- vcs if !interruptManager.isInterrupted() && !interrupt
+        vc <- vcs if !interruptManager.isInterrupted && !interrupt
       } {
         checkVC(vc)
         interrupt = interruptOn(vc)
diff --git a/src/test/scala/leon/test/purescala/WithLikelyEq.scala b/src/test/scala/leon/test/purescala/WithLikelyEq.scala
index 7fd0341232eb79a7f3e5ae91fb069388ec700ea2..988247a5986ee4d8200813279e9ef64f3703b388 100644
--- a/src/test/scala/leon/test/purescala/WithLikelyEq.scala
+++ b/src/test/scala/leon/test/purescala/WithLikelyEq.scala
@@ -7,8 +7,8 @@ import leon.test._
 import leon.evaluators._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.TreeOps.replace
-import leon.purescala.Trees._
+import leon.purescala.ExprOps.replace
+import leon.purescala.Expressions._
 
 /*
  * Determine if two expressions over arithmetic variables are likely to be equal.