diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index 637dbc8e6e4979d859b83334ec7a79da139c7be8..659a94fc883d45b5ab31705102f50a7adeab226e 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -25,8 +25,8 @@ trait Definitions { self: Trees =>
   case class FunctionLookupException(id: Identifier) extends LookupException(id, "function")
   case class ADTLookupException(id: Identifier) extends LookupException(id, "adt")
 
-  case class NotWellFormedException(id: Identifier, s: Symbols)
-    extends Exception(s"$id not well formed in $s")
+  case class NotWellFormedException(d: Definition)
+    extends Exception(s"Not well formed definition $d")
 
   /** Common super-type for [[ValDef]] and [[Expressions.Variable]].
     *
@@ -219,7 +219,7 @@ trait Definitions { self: Trees =>
     def constructors(implicit s: Symbols): Seq[ADTConstructor] = cons
       .map(id => s.getADT(id) match {
         case cons: ADTConstructor => cons
-        case _ => throw NotWellFormedException(id, s)
+        case sort => throw NotWellFormedException(sort)
       })
 
     def isInductive(implicit s: Symbols): Boolean = {
@@ -325,12 +325,12 @@ trait Definitions { self: Trees =>
 
     def toConstructor = this match {
       case tcons: TypedADTConstructor => tcons
-      case _ => throw NotWellFormedException(definition.id, symbols)
+      case _ => throw NotWellFormedException(definition)
     }
 
     def toSort = this match {
       case tsort: TypedADTSort => tsort
-      case _ => throw NotWellFormedException(definition.id, symbols)
+      case _ => throw NotWellFormedException(definition)
     }
   }
 
@@ -355,7 +355,7 @@ trait Definitions { self: Trees =>
 
     lazy val sort: Option[TypedADTSort] = definition.sort.map(id => symbols.getADT(id) match {
       case sort: ADTSort => TypedADTSort(sort, tps)
-      case _ => throw NotWellFormedException(id, symbols)
+      case cons => throw NotWellFormedException(cons)
     })
   }
 
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index bf4ebabd6eb78bdee06b5ee1ee6d5cdc4bc5e6f0..55c8aad2a5e486675e9eb7ef0e9f8ba8d76a4f6d 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -121,8 +121,7 @@ trait Expressions { self: Trees =>
   /** $encodingof  `function(...)` (function invocation) */
   case class FunctionInvocation(id: Identifier, tps: Seq[Type], args: Seq[Expr]) extends Expr with CachingTyped {
     protected def computeType(implicit s: Symbols): Type = s.lookupFunction(id, tps) match {
-      case Some(tfd) =>
-        require(args.size == tfd.params.size)
+      case Some(tfd) if args.size == tfd.params.size =>
         checkParamTypes(args.map(_.getType), tfd.params.map(_.tpe), tfd.returnType)
       case _ => Untyped
     }
diff --git a/src/main/scala/inox/ast/ProgramEncoder.scala b/src/main/scala/inox/ast/ProgramEncoder.scala
index 0d60a6ed6523c0cc4b34c2aba7e3c442d739add5..ec40e5f9e6436df42d1d20a21c09cdca49920dd6 100644
--- a/src/main/scala/inox/ast/ProgramEncoder.scala
+++ b/src/main/scala/inox/ast/ProgramEncoder.scala
@@ -83,5 +83,19 @@ object ProgramEncoder {
     protected object encoder extends p.trees.IdentityTreeTransformer
     protected object decoder extends p.trees.IdentityTreeTransformer
   }
+
+  def apply(p: Program)(tr: SymbolTransformer { val s: p.trees.type; val t: p.trees.type }): ProgramEncoder {
+    val sourceProgram: p.type
+    val t: p.trees.type
+  } = new ProgramEncoder {
+    val sourceProgram: p.type = p
+    val t: p.trees.type = p.trees
+
+    override protected def encodedProgram: Program { val trees: p.trees.type } = p.transform(tr)
+
+    protected object encoder extends p.trees.IdentityTreeTransformer
+    protected object decoder extends p.trees.IdentityTreeTransformer
+  }
+
 }
 
diff --git a/src/main/scala/inox/transformers/Collector.scala b/src/main/scala/inox/transformers/Collector.scala
index 191e3c73ad8bd1e22b85f83a81cfba881beff199..aef262a8a822943cf769cbde0706594ad1653060 100644
--- a/src/main/scala/inox/transformers/Collector.scala
+++ b/src/main/scala/inox/transformers/Collector.scala
@@ -13,11 +13,15 @@ trait Collector extends Transformer {
 
   import trees._
 
+  protected def accumulate(e: Expr, env: Env): Unit = {
+    results ++= step(e, env)
+  }
+
   /** 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)
+    accumulate(e, current)
     super.rec(e, current)
   }