Counterexample does not violate precondition of lambda passed to HOF

[samuelgruetter]

In this example

import leon.collection._

object Test {

  def id(x: BigInt): BigInt = {
    require(x >= 2)
    x
  }

  def go(start: BigInt): List[BigInt] = {
    require(start >= 2)
    Cons(start, Nil()).map(id)
  }

  // let's --eval this:
  def c1 = go(2)
}

Leon says it found a counter-example:

[  Info  ]  - Now considering 'precond. (call id(x))' VC for go @15:28...
[ Error  ]  => INVALID
[ Error  ] Found counter-example:
[ Error  ]   start -> 2
[ Error  ]   x     -> 0
[  Info  ]  - Now considering 'precond. (call go(2))' VC for c1 @19:12...
[  Info  ]  => VALID
[  Info  ]   ┌──────────────────────┐
[  Info  ] ╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └──────────────────────┘                                                                   ║
[  Info  ] ║ c1    precond. (call go(2))                   19:12      valid          Z3-f         0.004 ║
[  Info  ] ║ go    precond. (call id(x))                   15:28      invalid        Z3-f         0.023 ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 2      valid: 1      invalid: 1      unknown 0                                0.027 ║
[  Info  ] ╚════════════════════════════════════════════════════════════════════════════════════════════╝

If I understand correctly, it says that the call to id in Cons(start, Nil()).map(id) does not respect the precondition of id. But it does, because start is required to be >= 2.

[samarion]

Yes, this is a known issue. Currently, we cannot handle functions with preconditions inside of lambdas (id is desugared to x => id(x)). I'm currently working on finding a nice way of dealing with this limitation but I'm afraid this might require some form of universal quantification.