Fixed generic type subst for free variables in termination chains

src/main/scala/leon/termination/ChainBuilder.scala

@@ -50,14 +50,19 @@ final case class Chain(relations: List[Relation]) {
 
   def loop(initialArgs: Seq[Identifier] = Seq.empty, finalArgs: Seq[Identifier] = Seq.empty): Seq[Expr] = {
     def rec(relations: List[Relation], funDef: TypedFunDef, subst: Map[Identifier, Identifier]): Seq[Expr] = {
+      val Relation(_, path, FunctionInvocation(fitfd, args), _) = relations.head
+      val tfd = TypedFunDef(fitfd.fd, fitfd.tps.map(funDef.translated))
+
       val translate : Expr => Expr = {
-        val map : Map[Expr, Expr] = subst.map(p => p._1.toVariable -> p._2.toVariable)
+        val free : Set[Identifier] = path.flatMap(variablesOf).toSet -- funDef.fd.params.map(_.id)
+        val freeMapping : Map[Identifier,Identifier] = free.map(id => id -> {
+          FreshIdentifier(id.name, funDef.translated(id.getType), true).copiedFrom(id)
+        }).toMap
+
+        val map : Map[Expr, Expr] = (subst ++ freeMapping).map(p => p._1.toVariable -> p._2.toVariable)
         (e: Expr) => replace(map, funDef.translated(e))
       }
 
-      val Relation(_, path, FunctionInvocation(fitfd, args), _) = relations.head
-      val tfd = TypedFunDef(fitfd.fd, fitfd.tps.map(funDef.translated))
-
       lazy val newArgs = args.map(translate)
 
       path.map(translate) ++ (relations.tail match {