diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 512cb6ebf8ed5ad1135edd159888108a973d6b21..42cc07526982d45e56c034ea7b9b14f4c4c72e44 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -10,18 +10,18 @@ import Constructors._
 
 object Extractors {
 
-  /** Operator Extractor to extract any Expression in a consistent way
+  /** Operator Extractor to extract any Expression in a consistent way.
     *
     * You can match on any Leon Expr, and then get both a Seq[Expr] of
-    * subterms and a builder fonction that take a Seq of subterm (os same
+    * subterms and a builder fonction that takes a Seq of subterms (of same
     * length) and rebuild the original node.
     *
     * Those extractors do not perform any syntactic simplifications. They
-    * rebuild the node using the case class (not the constructor that perform
-    * simplifications). The rationals behind this decision is to have core
+    * rebuild the node using the case class (not the constructor, that performs
+    * simplifications). The rational behind this decision is to have core
     * tools for performing tree transformations that are very predictable, if
     * one need to simplify the tree, it is easy to write/call a simplification
-    * function that would simply apply the constructor for each node.
+    * function that would simply apply the corresponding constructor for each node.
     */
   object Operator extends TreeExtractor[Expr] {
     def unapply(expr: Expr): Option[(Seq[Expr], (Seq[Expr]) => Expr)] = expr match {
diff --git a/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala b/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
index c1c29acbbe91243f68315a94e6ba60cedc11b3a2..3c0376039ce33972deac9e3210d81757c6c6126e 100644
--- a/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
+++ b/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
@@ -49,6 +49,10 @@ import leon.test.helpers.ExpressionsDSLVariables
 import leon.purescala.Extractors._
 
 class InputCoverageSuite extends LeonTestSuiteWithProgram with Matchers with ScalaFutures with ExpressionsDSLProgram with ExpressionsDSLVariables {
+
+  //override a because it comes from both Matchers and ExpressionsDSLVariables
+  override val a = null
+
   val sources = List("""
     |import leon.lang._
     |import leon.collection._
@@ -315,4 +319,4 @@ class InputCoverageSuite extends LeonTestSuiteWithProgram with Matchers with Sca
       }
     }
   }
-}
\ No newline at end of file
+}
diff --git a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala b/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
index 7c6de266e523f46f94281a556dda2f2d691e783a..7a760143cfe733f989164bc4320960f129788de1 100644
--- a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
+++ b/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
@@ -9,9 +9,7 @@ import leon.purescala.Common._
 import leon.purescala.Types._
 import leon.purescala.Expressions._
 
-trait ExpressionsDSLVariables_a {
-  val a = FreshIdentifier("a", Int32Type).toVariable
-}
+import scala.language.implicitConversions
 
 trait ExpressionsDSLVariables {
   val F = BooleanLiteral(false)
@@ -22,6 +20,7 @@ trait ExpressionsDSLVariables {
   def i(x: Int)     = IntLiteral(x)
   def r(n: BigInt, d: BigInt)  = FractionalLiteral(n, d)
 
+  val a = FreshIdentifier("a", Int32Type).toVariable
   val b = FreshIdentifier("b", Int32Type).toVariable
   val c = FreshIdentifier("c", Int32Type).toVariable
 
@@ -100,10 +99,10 @@ self: Assertions =>
   }
 }
 
-trait ExpressionsDSL extends ExpressionsDSLVariables with ExpressionsDSLProgram with ExpressionsDSLVariables_a {
+trait ExpressionsDSL extends ExpressionsDSLVariables with ExpressionsDSLProgram {
   self: Assertions =>
-  
-  
+ 
+ 
   implicit def int2IntLit(i: Int): IntLiteral = IntLiteral(i)
   implicit def bigInt2IntegerLit(i: BigInt): InfiniteIntegerLiteral = InfiniteIntegerLiteral(i)
 
diff --git a/src/test/scala/leon/unit/purescala/DefinitionTransformerSuite.scala b/src/test/scala/leon/unit/purescala/DefinitionTransformerSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..88e9aea53c295baa1190eda284a323c471a89c2b
--- /dev/null
+++ b/src/test/scala/leon/unit/purescala/DefinitionTransformerSuite.scala
@@ -0,0 +1,33 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.unit.purescala
+
+import org.scalatest._
+
+import leon.test.helpers.ExpressionsDSL
+import leon.purescala.Common._
+import leon.purescala.Expressions._
+import leon.purescala.Extractors._
+import leon.purescala.DefinitionTransformer
+import leon.purescala.Definitions._
+import leon.purescala.Types._
+
+class DefinitionTransformerSuite extends FunSuite with ExpressionsDSL {
+
+  private val fd1 = new FunDef(FreshIdentifier("f1"), Seq(), Seq(ValDef(x.id)), IntegerType)
+  fd1.body = Some(x)
+
+  private val fd2 = new FunDef(FreshIdentifier("f1"), Seq(), Seq(ValDef(x.id)), IntegerType)
+  fd2.body = Some(Plus(x, bi(1)))
+
+  private val fd3 = new FunDef(FreshIdentifier("f1"), Seq(), Seq(ValDef(x.id)), IntegerType)
+  fd3.body = Some(Times(x, bi(1)))
+
+  test("transformation with no rewriting should not change FunDef") {
+    val tr1 = new DefinitionTransformer
+    assert(tr1.transform(fd1) === fd1)
+    assert(tr1.transform(fd2) === fd2)
+    assert(tr1.transform(fd3) === fd3)
+  }
+
+}
diff --git a/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala b/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala
index c09c39fe48a6e649a526e7401c3dbdc641a90da8..4e7c7d40ab4234bf0ae909271153823385badbc5 100644
--- a/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala
+++ b/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon.unit.xlang
+package leon.unit.purescala
 
 import org.scalatest._