diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index 5c1d651e81bdc829948cb3e38763e3889f6bff43..fa43474eadd42e50c5463fe78e39e73494ba0a42 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -168,7 +168,7 @@ trait QuantificationTemplates { self: Templates =>
           val inst: Variable = Variable(FreshIdentifier("inst", true), BooleanType)
           val insts = inst -> encodeSymbol(inst)
           val extraClause = mkImplies(pathVar._2, mkEquals(insts._2, pT))
-          (Some(inst), Negative(insts), Seq(extraClause), Map.empty)
+          (Some(inst), Negative(insts), Seq(extraClause), Map.empty[Variable, Encoded])
 
         case None =>
           val q: Variable = Variable(FreshIdentifier("q", true), BooleanType)