Stainless crashed with: Error: List() (of class scala.collection.immutable.Nil$).

[NicolasRouquette]

I tried to encode a simple directed graph library and crashed stainless with this error:

https://github.com/NicolasRouquette/stainless-bundle-closure/tree/10366df0c54395dd99bacb9451256c625d3ef5cc#v4-commit

This is with Stainless 0.7.4, sbt 1.3.0, scala 2.12.9 running on ubuntu 20.04

[info] Cache miss: 'adt invariant' VC for next @42:20...
[info]  - Now solving 'adt invariant' VC for next @42:20...
[info] ¬hasNext[V](thiss) || ¬wff[V](thiss.g.adjascent) || {
[info]   val x$1: (V, DFSIterator[V]) = (pop[V](thiss)._1, pop[V](thiss)._2)
[info]   val n: DFSIterator[V] = pop[V](thiss)._2
[info]   val vss: List[V] = ++[V](n.stack, childrenOf[V](n.g, pop[V](thiss)._1))
[info]   wff[V](n.g.adjascent) && includesAll[V](n.g.adjascent, vss) && includesAll[V](n.g.adjascent, n.toVisit) && noDuplicate[V](n.toVisit) && forall[V](vss, (v: V) => contains[V](n.toVisit, v))
[info] }
[info] Solving with: U:smt-z3
[error] Error: List() (of class scala.collection.immutable.Nil$). Trace:
[error] - stainless.verification.VerificationChecker.checkAdtInvariantModel(VerificationChecker.scala:150)
[error] - stainless.verification.VerificationChecker.checkAdtInvariantModel$(VerificationChecker.scala:147)
[error] - stainless.verification.VerificationChecker$Checker$1.checkAdtInvariantModel(VerificationChecker.scala:336)
[error] - stainless.verification.VerificationChecker.checkVC(VerificationChecker.scala:256)
[error] - stainless.verification.VerificationChecker.checkVC$(VerificationChecker.scala:214)
[error] - stainless.verification.VerificationChecker$$anon$1.stainless$verification$VerificationCache$$super$checkVC(VerificationChecker.scala:345)
[error] - stainless.verification.VerificationCache.$anonfun$checkVC$1(VerificationCache.scala:87)
[error] - scala.util.Try$.apply(Try.scala:213)
[error] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)

[jad-hamza]

Thanks for the report!

The error appears to come from there: https://github.com/epfl-lara/stainless/blob/391088ee6ea1154db23e1320d8f637b350c593c0/core/src/main/scala/stainless/verification/VerificationChecker.scala#L150-L152

@romac Any thoughts? What should we do when the invocation cannot be found?

[vkuncak]

@NicolasRouquette the list from Stainless library is invariant in its type parameter. The Scala standard library is not directly supported, but one could try to define a covariant list that more closely the covariant list of Scala, for example along the lines of this sketch: https://github.com/epfl-lara/bolts/tree/master/WIP/ScalaList