Fix bug in EquivalentInputs where pc got simplified under itself

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

@@ -9,15 +9,12 @@ import purescala.Path
 import purescala.Common._
 import purescala.Expressions._
 import purescala.ExprOps._
-import purescala.Extractors._
 import purescala.Constructors._
 import purescala.Types.CaseClassType
 
 case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
 
-    val simplifier = Simplifiers.bestEffort(hctx, hctx.program)(_:Expr, p.pc)
-
     var subst = Map.empty[Identifier, Expr]
     var reverseSubst = Map.empty[Identifier, Expr]
 
@@ -57,12 +54,12 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
       obsolete ++= equivalences.map(_._1)
       free ++= unbound
 
-      def replace(e: Expr) = simplifier(replaceFromIDs(equivalences.toMap, e))
+      def replace(e: Expr) = replaceFromIDs(equivalences.toMap, e)
       subst = subst.mapValues(replace) ++ equivalences
 
       val reverse = equivalences.toMap.flatMap { case (id, CaseClass(cct, fields)) =>
         (cct.classDef.fields zip fields).map { case (vid, Variable(fieldId)) =>
-          fieldId -> CaseClassSelector(cct, AsInstanceOf(Variable(id), cct), vid.id)
+          fieldId -> caseClassSelector(cct, asInstOf(Variable(id), cct), vid.id)
         }
       }
 
@@ -73,7 +70,7 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
 
     // We could discover one equivalence, which could allow us to discover
     // other equivalences: We do a fixpoint with limit 5.
-    val simplifiedPath = fixpoint({ (path: Path) => discoverEquivalences(path) }, 5)(p.pc)
+    val newPC = fixpoint({ (path: Path) => discoverEquivalences(path) }, 5)(p.pc)
 
     if (subst.nonEmpty) {
       // XXX: must take place in this order!! obsolete & free is typically non-empty
@@ -88,10 +85,12 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
         })
       }
 
+      val simplifier = Simplifiers.bestEffort(hctx, hctx.program)(_:Expr, newPC)
+
       val sub = p.copy(
         as = newAs,
         ws = replaceFromIDs(subst, p.ws),
-        pc = simplifiedPath,
+        pc = newPC,
         phi = simplifier(replaceFromIDs(subst, p.phi)),
         eb = newBank
       )