diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 8cbbaf2802cac822ed641bee2b144fd6d6a2a4c4..239f0cc629fe6144adb089153a13e81f773951ba 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -642,12 +642,18 @@ trait SymbolOps { self: TypeOps =>
     fold[String]{ (e, se) =>
       e match {
         case FunctionInvocation(id, tps, args) =>
-          val tfd = getFunction(id, tps)
-          s"${e.asString} is of type ${e.getType.asString}" +
-          se.map(child => "\n  " + "\n".r.replaceAllIn(child, "\n  ")).mkString +
-          s" because ${tfd.fd.id.name} was instantiated with " +
-          s"${tfd.fd.tparams.zip(tps).map(k => k._1.asString + ":=" + k._2.asString).mkString(",")} " +
-          s"with type ${tfd.fd.params.map(_.getType.asString).mkString(",")} => ${tfd.fd.returnType.asString}"
+          lookupFunction(id, tps) match {
+            case Some(tfd) =>
+              s"${e.asString} is of type ${e.getType.asString}" +
+              se.map(child => "\n  " + "\n".r.replaceAllIn(child, "\n  ")).mkString +
+              s" because ${tfd.fd.id.name} was instantiated with " +
+              s"${tfd.fd.tparams.zip(tps).map(k => k._1.asString + ":=" + k._2.asString).mkString(",")} " +
+              s"with type ${tfd.fd.params.map(_.getType.asString).mkString(",")} => ${tfd.fd.returnType.asString}"
+            case None =>
+              s"${e.asString} is of type ${e.getType.asString}" +
+              se.map(child => "\n  " + "\n".r.replaceAllIn(child, "\n  ")).mkString +
+              s" but couldn't find function $id"
+          }
         case e =>
           s"${e.asString} is of type ${e.getType.asString}" +
           se.map(child => "\n  " + "\n".r.replaceAllIn(child, "\n  ")).mkString
diff --git a/src/main/scala/inox/transformers/CollectorWithPC.scala b/src/main/scala/inox/transformers/CollectorWithPC.scala
index 0bad6300d08814ed56dee880989f9d5833df6865..dbacecd00d3a904fd21748097acf4207b52ce6a3 100644
--- a/src/main/scala/inox/transformers/CollectorWithPC.scala
+++ b/src/main/scala/inox/transformers/CollectorWithPC.scala
@@ -5,28 +5,32 @@ package transformers
 
 /** A [[Collector]] that collects path conditions */
 trait CollectorWithPC extends TransformerWithPC with Collector {
-  import program.trees._
-  import program.symbols._
-
-  lazy val initEnv: Path = Path.empty
+  lazy val initEnv = symbols.Path.empty
 }
 
 object CollectorWithPC {
-  def apply[T](p: Program)
-              (f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]):
-               CollectorWithPC { type Result = T; val program: p.type } = {
+  def apply[T](t: ast.Trees)
+              (s: t.Symbols)
+              (f: PartialFunction[(t.Expr, s.Path), T]):
+               CollectorWithPC { type Result = T; val trees: t.type; val symbols: s.type } = {
     new CollectorWithPC {
       type Result = T
-      val program: p.type = p
-      import program.trees._
-      import program.symbols._
+      val trees: t.type = t
+      val symbols: s.type = s
 
       private val fLifted = f.lift
 
-      protected def step(e: Expr, env: Path): List[T] = {
+      protected def step(e: t.Expr, env: s.Path): List[T] = {
         fLifted((e, env)).toList
       }
     }
   }
 
+  def apply[T](p: Program)
+              (f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]):
+               CollectorWithPC { type Result = T; val trees: p.trees.type; val symbols: p.symbols.type } = {
+    apply(p.trees)(p.symbols)(f)
+  }
+              
+
 }
diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala
index 0bdbfddadc7b30f30a70ee6bc1efa972880f65af..0cf5581d3bfb443877aaa18597d34000bfe89994 100644
--- a/src/main/scala/inox/transformers/SimplifierWithPC.scala
+++ b/src/main/scala/inox/transformers/SimplifierWithPC.scala
@@ -8,9 +8,13 @@ import inox.solvers.{SimpleSolverAPI, SolverFactory}
 /** Uses solvers to perform PC-aware simplifications */
 trait SimplifierWithPC extends TransformerWithPC { self =>
 
+  val program: Program
+  lazy val trees: program.trees.type = program.trees
+  lazy val symbols: program.symbols.type = program.symbols
+
   import program._
-  import trees._
-  import symbols._
+  import program.trees._
+  import program.symbols._
 
   protected val sf: SolverFactory { val program: self.program.type }
   protected lazy val s = SimpleSolverAPI(sf)
diff --git a/src/main/scala/inox/transformers/TransformerWithPC.scala b/src/main/scala/inox/transformers/TransformerWithPC.scala
index 1714f9d9dd76db139373df42bdf1211b7befb62f..20698ee34213e9449384eb52209277365e6506b8 100644
--- a/src/main/scala/inox/transformers/TransformerWithPC.scala
+++ b/src/main/scala/inox/transformers/TransformerWithPC.scala
@@ -5,11 +5,10 @@ package transformers
 
 /** A [[Transformer]] which uses path conditions as environment */
 trait TransformerWithPC extends Transformer {
-  val program: Program
-  import program._
-  final lazy val trees: program.trees.type = program.trees
+  val symbols: trees.Symbols
   import trees._
   import symbols._
+
   type Env = Path
 
   protected def rec(e: Expr, path: Path): Expr = e match {