diff --git a/src/main/scala/inox/ast/DSL.scala b/src/main/scala/inox/ast/DSL.scala
index 46778edfffb4b6a22681436680cb99829085f2d2..f8de46db25c0518034b3144ea0236754223bf96e 100644
--- a/src/main/scala/inox/ast/DSL.scala
+++ b/src/main/scala/inox/ast/DSL.scala
@@ -30,6 +30,7 @@ trait DSL {
     def - = Minus(e, _: Expr)
     def % = Modulo(e, _: Expr)
     def / = Division(e, _: Expr)
+    def unary_- = UMinus(e)
 
     // Comparisons
     def <   = LessThan(e, _: Expr)
diff --git a/src/main/scala/inox/transformers/Collector.scala b/src/main/scala/inox/transformers/Collector.scala
index 5424859c38c9a6f62a2adb0f33236e1f1abe958d..8097214e7078a14420770cbb352a8009176e2ac9 100644
--- a/src/main/scala/inox/transformers/Collector.scala
+++ b/src/main/scala/inox/transformers/Collector.scala
@@ -11,9 +11,10 @@ trait Collector extends Transformer {
   /** The type of collected objects */
   type R
   final type Result = (R, Env)
-  import trees.Expr
   private var results: List[Result] = Nil
 
+  import trees._
+
   /** Does one step of collection for the current [[Expr]] and [[Env]] */
   protected def step(e: Expr, env: Env): List[Result]
 
@@ -23,9 +24,12 @@ trait Collector extends Transformer {
   }
 
   /** Traverses the expression and collects */
-  final def collect(e: Expr) = {
+  final def collect(e: Expr): List[Result] = {
     results = Nil
     transform(e)
     results
   }
+
+  /** Collect the expressions in a [[FunDef]]'s body */
+  final def collect(fd: FunDef): List[Result] = collect(fd.fullBody)
 }
diff --git a/src/main/scala/inox/transformers/CollectorWithPC.scala b/src/main/scala/inox/transformers/CollectorWithPC.scala
index 0681991d3035d4058348ef112ab6eda3b70084f9..823b351960bf3a2945f6e778b19159a146e2e7d4 100644
--- a/src/main/scala/inox/transformers/CollectorWithPC.scala
+++ b/src/main/scala/inox/transformers/CollectorWithPC.scala
@@ -4,18 +4,22 @@ package inox
 package transformers
 
 /** A [[Collector]] that collects path conditions */
-trait CollectorWithPC extends TransformerWithPC with Collector
+trait CollectorWithPC extends TransformerWithPC with Collector {
+  import program.trees._
+  import program.symbols._
+
+  lazy val initEnv: Path = Path.empty
+}
 
 object CollectorWithPC {
-  def apply[T](p: Program)(f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]): CollectorWithPC { type R = T; val program: p.type } = {
+  def apply[T](p: Program)
+              (f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]):
+               CollectorWithPC { type R = T; val program: p.type } = {
     new CollectorWithPC {
-
       type R = T
       val program: p.type = p
-      import program._
-      import symbols._
-      import trees._
-      val initEnv: Path = Path.empty
+      import program.trees._
+      import program.symbols._
 
       private val fLifted = f.lift
 
diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala
index b0bb42569a5611c4288070a99298fe6eb502d924..0bdbfddadc7b30f30a70ee6bc1efa972880f65af 100644
--- a/src/main/scala/inox/transformers/SimplifierWithPC.scala
+++ b/src/main/scala/inox/transformers/SimplifierWithPC.scala
@@ -12,7 +12,7 @@ trait SimplifierWithPC extends TransformerWithPC { self =>
   import trees._
   import symbols._
 
-  protected val sf: SolverFactory{ val program: self.program.type }
+  protected val sf: SolverFactory { val program: self.program.type }
   protected lazy val s = SimpleSolverAPI(sf)
 
   private def querie(e: Expr, path: Path, implied: Boolean) = {