Counter-example not well typed in presence of lambdas

[jad-hamza]

Sorry for the long file, but it is hard to reproduce the problem.when removing lines in the code.
When running with --solvers=smt-cvc4 or --solvers=smt-z3, we obtain a counter-example

[Warning ] net -> VerifiedNetwork(MMap[BigInt, BigInt](VerifiedNetwork%28MMap[BigInt, BigInt]%28%28x$399 : BigInt%29 => None[BigInt]%28%29%29%29))

which is not well-typed (VerifiedNetwork is not recursive, and MMap should take a lambda as a parameter, not a VerifiedNetwork)

Note that there are quantifiers in "instantiate".

import leon.lang._
import leon.collection._
import leon.proof._
import leon.annotation._

import scala.language.postfixOps


object Networking {

  case class MMap[A,B](f: A => Option[B]) {

    def contains(k: A): Boolean = f(k) != None[B]()


    def getOrElse(k: A, v: B) = {
      if (contains(k)) f(k).get
      else v
    }
  }
  case class VerifiedNetwork(states: MMap[BigInt,BigInt]) 

  abstract class ActorId
  case class UID(uid: BigInt) extends ActorId


  abstract class Message
  case class Elected(i: BigInt) extends Message


  abstract class Actor {
    val myId: ActorId

  }
  case class PP(myId: ActorId) extends Actor


  def instantiate(n: BigInt, p: BigInt => Boolean): Boolean = {
    require(forall ((i: BigInt) => p(i)))

    true
  }


  def receivePre(n: BigInt, a: Actor, m: Message, net: VerifiedNetwork) = {

    val UID(myuid) = a.myId

    myuid < n && {
      val dummyVar = 0

      (instantiate(n, (i: BigInt) => net.states.contains(i)))  && (
        m match {
          case Elected(uid) => false
        })
    }
  }




  def applyMessage(
    messages: MMap[(ActorId,ActorId), List[Message]], 
    param: BigInt, 
    getActor: Actor, 
    sender: ActorId, 
    receiver: ActorId, 
    m: Message, 
    net: VerifiedNetwork): Boolean = {

    val sms = messages.getOrElse((sender,receiver), Nil())

    sms match {
      case Cons(x, xs) if (x == m) => 
        check(receivePre(param, getActor,m, net))

      case _ => 
        false
    }

  }

}

[samarion]

Fixed in 05ed414