diff --git a/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala b/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala
index 753145736961353b597aa080960bc6760a6eecf0..a6a47106ddc94203c7408734e34f47580d623772 100644
--- a/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala
+++ b/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala
@@ -38,7 +38,7 @@ class InductiveUnrollingSuite extends SolvingTestSuite {
   val append = mkFunDef(appendID)("A") { case Seq(aT) => (
     Seq("l1" :: T(listID)(aT), "l2" :: T(listID)(aT)), T(listID)(aT), { case Seq(l1, l2) =>
       if_ (l1.isInstOf(T(consID)(aT))) {
-        let("c" :: T(listID)(aT), l1.asInstOf(T(consID)(aT))) { c =>
+        let("c" :: T(consID)(aT), l1.asInstOf(T(consID)(aT))) { c =>
           T(consID)(aT)(c.getField(head), E(appendID)(aT)(c.getField(tail), l2))
         }
       } else_ {
diff --git a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
index d9e5836ddbd499e3da88424d2cf046537052256f..8d519087ed52515fd51fcb11b5e5b23c1a6645e8 100644
--- a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
@@ -259,7 +259,6 @@ trait DatatypeTemplates { self: Templates =>
     }
 
     def unroll: Clauses = if (typeInfos.isEmpty) Seq.empty else {
-      println("unrolling datatypes")
       val blockers = typeInfos.filter(_._2._1 <= currentGeneration).toSeq.map(_._1)
 
       val newClauses = new scala.collection.mutable.ListBuffer[Encoded]