Ref equality required between lambdas, otherwise we get wrong

counter-examples

src/main/scala/leon/solvers/templates/LambdaManager.scala

@@ -31,16 +31,29 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) {
     applicationsStack = map :: applicationsStack.tail
   }
 
+  private type FreeMap = Map[TypeTree, Set[T]]
+  private var freeLambdasStack : List[FreeMap] = List(Map.empty.withDefaultValue(Set.empty))
+  private def freeLambdas : FreeMap = freeLambdasStack.head
+  private def freeLambdas_=(map: FreeMap) : Unit = {
+    freeLambdasStack = map :: freeLambdasStack.tail
+  }
+
   def push(): Unit = {
     byIDStack = byID :: byIDStack
     byTypeStack = byType :: byTypeStack
     applicationsStack = applications :: applicationsStack
+    freeLambdasStack = freeLambdas :: freeLambdasStack
   }
 
   def pop(lvl: Int): Unit = {
     byIDStack = byIDStack.drop(lvl)
     byTypeStack = byTypeStack.drop(lvl)
     applicationsStack = applicationsStack.drop(lvl)
+    freeLambdasStack = freeLambdasStack.drop(lvl)
+  }
+
+  def registerFree(lambdas: Seq[(TypeTree, T)]): Unit = {
+    lambdas.foreach(p => freeLambdas += p._1 -> (freeLambdas(p._1) + p._2))
   }
 
   def instantiate(apps: Map[T, Set[App[T]]], lambdas: Map[T, LambdaTemplate[T]]) : (Seq[T], Map[T, Set[TemplateCallInfo[T]]], Map[(T, App[T]), Set[TemplateAppInfo[T]]]) = {
@@ -57,6 +70,9 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) {
     }
 
     for (lambda @ (idT, template) <- lambdas) {
+      // make sure concrete lambdas can't be equal to free lambdas
+      clauses ++= freeLambdas(template.tpe).map(pIdT => encoder.mkNot(encoder.mkEquals(pIdT, idT)))
+
       byID += idT -> template
       byType += template.tpe -> (byType(template.tpe) + (idT -> template))
 

src/main/scala/leon/solvers/templates/Templates.scala

@@ -229,6 +229,11 @@ class FunctionTemplate[T] private(
 
   private lazy val str : String = stringRepr()
   override def toString : String = str
+
+  override def instantiate(aVar: T, args: Seq[T]): (Seq[T], Map[T, Set[TemplateCallInfo[T]]], Map[(T, App[T]), Set[TemplateAppInfo[T]]]) = {
+    if (!isRealFunDef) lambdaManager.registerFree(tfd.params.map(_.tpe) zip args)
+    super.instantiate(aVar, args)
+  }
 }
 
 object LambdaTemplate {

src/test/resources/regression/verification/purescala/valid/Lists.scala → src/test/resources/regression/verification/purescala/valid/Lists1.scala

 import leon.lang._
+import leon.collection._
+import leon.annotation._
 
-object Lists {
-  abstract class List
-  case class Cons(head: Int, tail: List) extends List
-  case class Nil() extends List
+object Lists1 {
 
-  def exists(list: List, f: Int => Boolean): Boolean = list match {
+  def exists[T](list: List[T], f: T => Boolean): Boolean = list match {
     case Cons(head, tail) => f(head) || exists(tail, f)
     case Nil() => false
   }
 
-  def forall(list: List, f: Int => Boolean): Boolean = list match {
+  def forall[T](list: List[T], f: T => Boolean): Boolean = list match {
     case Cons(head, tail) => f(head) && forall(tail, f)
     case Nil() => true
   }
 
-  def exists_lemma(list: List, f: Int => Boolean): Boolean = {
-    exists(list, f) == !forall(list, x => !f(x))
+  def exists_lemma[T](list: List[T], f: T => Boolean): Boolean = {
+    exists(list, f) == !forall(list, (x: T) => !f(x))
   }
 
-  def exists_lemma_induct(list: List, f: Int => Boolean): Boolean = {
+  def exists_lemma_induct[T](list: List[T], f: T => Boolean): Boolean = {
     list match {
       case Nil() => exists_lemma(list, f)
       case Cons(head, tail) => exists_lemma(list, f) && exists_lemma_induct(tail, f)
     }
-  }.holds
+  }.holds 
 
 }
 

src/test/resources/regression/verification/purescala/valid/Sets1.scala

+import leon.lang._
+
+object Sets1 {
+  def set(i: Int): Int => Boolean = x => x == i
+
+  def complement(s: Int => Boolean): Int => Boolean = x => !s(x)
+
+  def union(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) || s2(x)
+
+  def intersection(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) && s2(x)
+
+  def associativity(sa1: Int => Boolean, sa2: Int => Boolean, sa3: Int => Boolean, x: Int): Boolean = {
+    val u1 = union(union(sa1, sa2), sa3)
+    val u2 = union(sa1, union(sa2, sa3))
+    u1(x) == u2(x)
+  }.holds
+
+  def lemma(s1: Int => Boolean, s2: Int => Boolean, x: Int): Boolean = {
+    val u1 = union(s1, s2)
+    val u2 = complement(intersection(complement(s1), complement(s2)))
+    u1(x) == u2(x)
+  }.holds
+}