New tests for function canBeHomomorphic + corrected implementation.

src/main/scala/leon/purescala/ExprOps.scala

@@ -1537,6 +1537,9 @@ object ExprOps {
   
   /** Checks whether two expressions can be homomorphic and returns the corresponding mapping */
   def canBeHomomorphic(t1: Expr, t2: Expr): Option[Map[Identifier, Identifier]] = {
+    val freeT1Variables = ExprOps.variablesOf(t1)
+    val freeT2Variables = ExprOps.variablesOf(t2)
+    
     def mergeContexts(a: Option[Map[Identifier, Identifier]], b: =>Option[Map[Identifier, Identifier]]) = a match {
       case Some(m) =>
         b match {
@@ -1570,7 +1573,7 @@ object ExprOps {
 
 
     def idHomo(i1: Identifier, i2: Identifier): Option[Map[Identifier, Identifier]] = {
-      Some(Map(i1 -> i2))
+      if(!(freeT1Variables(i1) || freeT2Variables(i2)) || i1 == i2) Some(Map(i1 -> i2)) else None
     }
 
     def fdHomo(fd1: FunDef, fd2: FunDef): Option[Map[Identifier, Identifier]] = {

src/test/scala/leon/integration/purescala/ExprOpsSuite.scala

@@ -101,5 +101,17 @@ class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL
     assert(isSubtypeOf(simplestValue(act).getType, act))
     assert(simplestValue(cct).getType == cct)
   }
+  
+  test("canBeHomomorphic") { implicit fix =>
+    import leon.purescala.ExprOps.canBeHomomorphic
+    import leon.purescala.Types._
+    import leon.purescala.Definitions._
+    val d = FreshIdentifier("x", IntegerType)
+    val e = FreshIdentifier("y", IntegerType)
+    assert(canBeHomomorphic(Variable(d), Variable(e)).isEmpty)
+    val l1 = Lambda(Seq(ValDef(d)), Variable(d))
+    val l2 = Lambda(Seq(ValDef(e)), Variable(e))
+    assert(canBeHomomorphic(l1, l2).nonEmpty)
+  }
 
 }