diff --git a/src/main/scala/inox/transformers/Collector.scala b/src/main/scala/inox/transformers/Collector.scala
new file mode 100644
index 0000000000000000000000000000000000000000..87ac9e52bbee8c35a817b7b05d73e5ece771ff97
--- /dev/null
+++ b/src/main/scala/inox/transformers/Collector.scala
@@ -0,0 +1,31 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package transformers
+
+/** A common trait for objects that collect something from expressions.
+  * The [[Transformer]] environment will also be collected along the way.
+  * This trait is meant to be mixed in with a specific [[Transformer]] to attach collect functionality.
+  */
+trait Collector extends Transformer {
+  /** The type of collected objects */
+  type R
+  type Result = (R, Env)
+  import trees.Expr
+  private var results: List[Result] = Nil
+
+  /** Does one step of collection for the current [[Expr]] and [[Env]] */
+  protected def step(e: Expr, env: Env): List[Result]
+
+  abstract override protected def rec(e: Expr, current: Env): Expr = {
+    results ++= step(e, current)
+    super.rec(e, current)
+  }
+
+  /** Traverses the expression and collects */
+  def collect(e: Expr) = {
+    results = Nil
+    transform(e)
+    results
+  }
+}
diff --git a/src/main/scala/inox/transformers/Transformer.scala b/src/main/scala/inox/transformers/Transformer.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1faa3275561a4657e73450428c8c7437c473697d
--- /dev/null
+++ b/src/main/scala/inox/transformers/Transformer.scala
@@ -0,0 +1,34 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package transformers
+
+import ast._
+
+/** Common trait for expression transformers.
+  * Uses an abstract environment type.
+  */
+trait Transformer {
+  type Env
+  val trees: Trees
+  import trees.{Expr, FunDef}
+
+  /** The default initial [[Env]] */
+  val initEnv: Env
+
+  /** The function that recursively traverses the expression
+    *
+    * @param e The current expression
+    * @param env The current [[Env]]
+    * @return The transformed expression
+    */
+  protected def rec(e: Expr, env: Env): Expr
+
+  /** Transform an [[Expr]] with the specified environment */
+  def transform(e: Expr, init: Env): Expr = rec(e, init)
+  /** Transform an [[Expr]] with the initial environment */
+  def transform(e: Expr): Expr            = transform(e, initEnv)
+  /** Transform the body of a [[FunDef]] */
+  def transform(fd: FunDef): Expr         = transform(fd.fullBody)
+}
+
diff --git a/src/main/scala/inox/transformers/TransformerWithPC.scala b/src/main/scala/inox/transformers/TransformerWithPC.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fd0709898fca22d7a5d4e30c0f97186180c3d4e0
--- /dev/null
+++ b/src/main/scala/inox/transformers/TransformerWithPC.scala
@@ -0,0 +1,100 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package transformers
+
+/** A [[Transformer]] which uses path conditions as environment */
+trait TransformerWithPC extends Transformer {
+  import trees._
+  val symbols: Symbols
+  import symbols._
+  type Env = Path
+  import exprOps.replaceFromSymbols
+
+  protected def rec(e: Expr, path: Path): Expr = e match {
+    case Let(i, v, b) =>
+      val se = rec(v, path)
+      val sb = rec(b, path withBinding (i -> se))
+      Let(i, se, sb).copiedFrom(e)
+
+    case Ensuring(req @ Require(pre, body), lam @ Lambda(Seq(arg), post)) =>
+      val spre = rec(pre, path)
+      val sbody = rec(body, path withCond spre)
+      val spost = rec(post, path withCond spre withBinding (arg -> sbody))
+      Ensuring(
+        Require(spre, sbody).copiedFrom(req),
+        Lambda(Seq(arg), spost).copiedFrom(lam)
+      ).copiedFrom(e)
+
+    case Ensuring(body, lam @ Lambda(Seq(arg), post)) =>
+      val sbody = rec(body, path)
+      val spost = rec(post, path withBinding (arg -> sbody))
+      Ensuring(
+        sbody,
+        Lambda(Seq(arg), spost).copiedFrom(lam)
+      ).copiedFrom(e)
+
+    case Require(pre, body) =>
+      val sp = rec(pre, path)
+      val sb = rec(body, path withCond pre)
+      Require(sp, sb).copiedFrom(e)
+
+    //@mk: TODO Discuss if we should include asserted predicates in the pc
+    //case Assert(pred, err, body) =>
+    //  val sp = rec(pred, path)
+    //  val sb = rec(body, register(sp, path))
+    //  Assert(sp, err, sb).copiedFrom(e)
+
+    case MatchExpr(scrut, cases) =>
+      val rs = rec(scrut, path)
+
+      var soFar = path
+
+      MatchExpr(rs, cases.map { c =>
+        val patternPathPos = conditionForPattern(rs, c.pattern, includeBinders = true)
+        val patternPathNeg = conditionForPattern(rs, c.pattern, includeBinders = false)
+        val map = mapForPattern(rs, c.pattern)
+        val guardOrTrue = c.optGuard.getOrElse(BooleanLiteral(true))
+        val guardMapped = replaceFromSymbols(map, guardOrTrue)
+
+        val subPath = soFar merge (patternPathPos withCond guardOrTrue)
+        soFar = soFar merge (patternPathNeg withCond guardMapped).negate
+
+        MatchCase(c.pattern, c.optGuard, rec(c.rhs, subPath)).copiedFrom(c)
+      }).copiedFrom(e)
+
+    case IfExpr(cond, thenn, elze) =>
+      val rc = rec(cond, path)
+      IfExpr(rc, rec(thenn, path withCond rc), rec(elze, path withCond Not(rc))).copiedFrom(e)
+
+    case And(es) =>
+      var soFar = path
+      andJoin(for(e <- es) yield {
+        val se = rec(e, soFar)
+        soFar = soFar withCond se
+        se
+      }).copiedFrom(e)
+
+    case Or(es) =>
+      var soFar = path
+      orJoin(for(e <- es) yield {
+        val se = rec(e, soFar)
+        soFar = soFar withCond Not(se)
+        se
+      }).copiedFrom(e)
+
+    case i @ Implies(lhs, rhs) =>
+      val rc = rec(lhs, path)
+      Implies(rc, rec(rhs, path withCond rc)).copiedFrom(i)
+
+    case o @ Operator(es, builder) =>
+      builder(es.map(rec(_, path))).copiedFrom(o)
+
+    case _ =>
+      sys.error(s"Expression $e [${e.getClass}] is not extractable")
+  }
+
+}
+
+/** A [[Collector]] that collects path conditions */
+trait CollectorWithPC extends TransformerWithPC with Collector