EquivalentInputs substitutes back during solution reconstruction

src/main/scala/leon/synthesis/Rules.scala

@@ -143,6 +143,12 @@ trait RuleDSL {
   def substAll(what: Map[Identifier, Expr], in: Expr): Expr = replaceFromIDs(what, in)
 
   val forward: List[Solution] => Option[Solution] = { ss => ss.headOption }
+  
+  def forwardMap(f : Expr => Expr) : List[Solution] => Option[Solution] = { 
+    _.headOption map { s =>
+      Solution(f(s.pre), s.defs, f(s.term))
+    }
+  }
 
   def decomp(sub: List[Problem], onSuccess: List[Solution] => Option[Solution], description: String)
             (implicit problem: Problem): RuleInstantiation = {

src/main/scala/leon/synthesis/rules/EquivalentInputs.scala

@@ -19,7 +19,7 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
         case ccio @ CaseClassInstanceOf(cct, s) => ccio
       }
 
-      var clauses = allClauses.filterNot(instanceOfs.toSet)
+      val clauses = allClauses.filterNot(instanceOfs.toSet)
 
       val ccSubsts = for (CaseClassInstanceOf(cct, s) <- instanceOfs) yield {
 
@@ -73,7 +73,12 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
                        pc = simplifier(andJoin(replaceSeq(substs, p.pc) +: postsToInject)),
                        phi = simplifier(replaceSeq(substs, p.phi)))
 
-      List(decomp(List(sub), forward, "Equivalent Inputs"))
+      val subst = replace(
+        substs.map{_.swap}.filter{ case (x,y) => formulaSize(x) > formulaSize(y) }.toMap, 
+        _:Expr
+      )
+      
+      List(decomp(List(sub), forwardMap(subst), "Equivalent Inputs"))
     } else {
       Nil
     }