diff --git a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
index 9a2f915e35a9397d71f1c87b19daf9ca560ef315..49114239edcd91782ef5cbda85637aabcc9e0afd 100644
--- a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
@@ -138,7 +138,8 @@ trait DatatypeTemplates { self: Templates =>
         guardedExprs += pathVar -> (expr +: prev)
       }
 
-      @inline protected def iff(e1: Expr, e2: Expr): Unit = storeGuarded(pathVar, Equals(e1, e2))
+      private var equations = Seq[Expr]()
+      @inline protected def iff(e1: Expr, e2: Expr): Unit = equations :+= Equals(e1, e2)
 
       private var tpes = Map[Variable, Set[(TypedADTSort, Expr)]]()
       @inline protected def storeType(pathVar: Variable, tsort: TypedADTSort, arg: Expr): Unit = {
@@ -179,6 +180,7 @@ trait DatatypeTemplates { self: Templates =>
                 }
 
                 val vars = tpes.keys.toSet ++ functions.keys ++
+                  guardedExprs.keys ++
                   guardedExprs.flatMap(_._2.flatMap(exprOps.variablesOf))
 
                 if (vars(newBool)) {
@@ -223,6 +225,8 @@ trait DatatypeTemplates { self: Templates =>
           if (callInfos.nonEmpty) calls += encoder(b) -> callInfos
         }
 
+        clauses ++= equations.map(encoder)
+
         val encodedTypes: Map[Encoded, Set[(TypedADTSort, Encoded)]] = tpes.map { case (b, tps) =>
           encoder(b) -> tps.map { case (tadt, expr) => (tadt, encoder(expr)) }
         }
@@ -487,6 +491,11 @@ trait DatatypeTemplates { self: Templates =>
           newClauses ++= template.instantiate(blocker, container, arg)
       }
 
+      ctx.reporter.debug("Unrolling datatypes (" + newClauses.size + ")")
+      for (cl <- newClauses) {
+        ctx.reporter.debug("  . " + cl)
+      }
+
       newClauses.toSeq
     }
   }