diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index 35423e656e3890d0fa8c20910fbfe52b83872765..f4da2f71a6bbeed344fbcb58ab454a1568574b46 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -46,7 +46,12 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
         }
       }
 
-      ccSubsts.flatten
+      // Direct equivalences:
+      val directEqs = allClauses.collect {
+        case Equals(v1 @ Variable(a1), v2 @ Variable(a2)) if a1 != a2 => (v2, v1)
+      }
+
+      ccSubsts.flatten ++ directEqs
     }
 
 
@@ -78,7 +83,9 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
         _:Expr
       )
       
-      List(decomp(List(sub), forwardMap(subst), "Equivalent Inputs"))
+      val substString = substs.map { case (f, t) => f+" -> "+t }
+
+      List(decomp(List(sub), forwardMap(subst), "Equivalent Inputs ("+substString.mkString(", ")+")"))
     } else {
       Nil
     }