diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index e5b257f077816aea9995a50c0c04195cd6b6c7b6..72b20588b542665295f8b5e6c2e4c9036e31125c 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -95,7 +95,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
 
   def getSynthesizer(passingTests: List[Example], failingTests: List[Example]): Synthesizer = {
     // Create a fresh function
-    val nid = FreshIdentifier(fd.id.name+"_repair").copiedFrom(fd.id)
+    val nid = FreshIdentifier(fd.id.name+"'").copiedFrom(fd.id)
     val nfd = new FunDef(nid, fd.tparams, fd.returnType, fd.params, fd.defType)
     nfd.copyContentFrom(fd)
     nfd.copiedFrom(fd)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index e93aa70893d7fdec87a2dd95c3503bb7b9e50b45..d616c3b933e2abfaab0e7720d1fab97b3250f1e4 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -27,7 +27,7 @@ object Rules {
     InequalitySplit,
     CEGIS,
     TEGIS,
-    BottomUpTEGIS,
+    //BottomUpTEGIS,
     rules.Assert,
     DetupleOutput,
     DetupleInput,
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index 3a0847389eb78b5ae810baf5db408ca31ad6a6f1..6b936d66b5066558194112c90f5b83305311b0b7 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -50,8 +50,15 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
     }
 
 
-    val substs = discoverEquivalences(clauses)
+    // We could discover one equivalence, which could allow us to discover
+    // other equivalences: We do a fixpoint with limit 5.
+    val substs = fixpoint({ (substs: Set[(Expr, Expr)]) =>
+      val newClauses = substs.map{ case(e,v) => Equals(v, e) } // clauses are directed: foo = obj.f
+      substs ++ discoverEquivalences(clauses ++ newClauses)
+    }, 5)(Set()).toSeq
 
+
+    // We are replacing foo(a) with b. We inject postcondition(foo)(a, b).
     val postsToInject = substs.collect {
       case (FunctionInvocation(tfd, args), e) if tfd.hasPostcondition =>
         val Some((id, post)) = tfd.postcondition