diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index f78c4060c48f24b70b332f78468ce9fcd94743b4..49cd236dc40dad92bfdd5622d460c102ce90a794 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -622,6 +622,10 @@ trait SymbolOps { self: TypeOps =>
     liftToLambdas(expr)
   }
 
+  def simplifyFormula(e: Expr): Expr = {
+    simplifyHOFunctions(simplifyByConstructors(simplifyQuantifications(e)))
+  }
+
   // Use this only to debug isValueOfType
   private implicit class BooleanAdder(b: Boolean) {
     @inline def <(msg: => String) = {/*if(!b) println(msg); */b}
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index 2fc373f6586eb0caa5b8f825660bbc4a7456f821..3b01c100ef093dea149a9cccda03cd122b9800d7 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -43,7 +43,7 @@ trait TemplateGenerator { self: Templates =>
       return cache(tfd)
     }
 
-    val lambdaBody : Expr = simplifyHOFunctions(tfd.fullBody)
+    val lambdaBody : Expr = simplifyFormula(tfd.fullBody)
 
     val funDefArgs: Seq[Variable] = tfd.params.map(_.toVariable)
     val lambdaArguments: Seq[Variable] = lambdaArgs(lambdaBody)
diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala
index d2579e9a085270b7c8538b2bcbfab6be23496887..95f9f7b56610aab43efea6e0a76c2de7adb6d211 100644
--- a/src/main/scala/inox/solvers/unrolling/Templates.scala
+++ b/src/main/scala/inox/solvers/unrolling/Templates.scala
@@ -557,7 +557,7 @@ trait Templates extends TemplateGenerator
 
     val tpeClauses = bindings.flatMap { case (v, s) => registerSymbol(encodedStart, s, v.getType) }.toSeq
 
-    val instExpr = simplifyHOFunctions(simplifyQuantifications(expr))
+    val instExpr = simplifyFormula(expr)
     val (condVars, exprVars, condTree, guardedExprs, eqs, lambdas, quants) =
       mkClauses(start, instExpr, bindings + (start -> encodedStart), polarity = Some(true))
 
diff --git a/src/main/scala/inox/tip/Parser.scala b/src/main/scala/inox/tip/Parser.scala
index 0a5af026d2f7aff1d51a42403c4de5e27e1c65e6..422cedd2bf3e2d75f72e78d7158512ce21bcf474 100644
--- a/src/main/scala/inox/tip/Parser.scala
+++ b/src/main/scala/inox/tip/Parser.scala
@@ -43,14 +43,6 @@ class Parser(file: File) {
     (for (cmd <- script.commands) yield cmd match {
       case CheckSat() =>
         val expr: Expr = locals.symbols.andJoin(assertions)
-        for (fd <- locals.symbols.functions.values) {
-          if (fd.fullBody.getType(locals.symbols) == Untyped) {
-            println(locals.symbols.explainTyping(fd.fullBody)(PrinterOptions(printUniqueIds = true, symbols = Some(locals.symbols))))
-          }
-        }
-        if (expr.getType(locals.symbols) == Untyped) {
-          println(locals.symbols.explainTyping(expr)(PrinterOptions(printUniqueIds = true, symbols = Some(locals.symbols))))
-        }
         Some((locals.symbols, expr))
 
       case _ =>