How to prove size of a list in Leon?

Question

I am trying to prove that the size (number of elements) in a list is non-negative, but Leon fails to prove it---it just times out. Is Leon really not capable of proving this property, or am I using it wrongly? My starting point is a function I read in the paper "An Overview of the Leon Verification System".

import leon.lang._
import leon.annotation._

object ListSize {
  sealed abstract class List
  case class Cons(head: Int, tail: List) extends List
  case object Nil extends List

  def size(l: List) : Int = (l match {
    case Nil => 0
    case Cons(_, t) => 1 + size(t)
  }) ensuring(_ >= 0)
}

Answer 1

Previous versions of Leon treated Scala's Int type as mathematical, unbounded, integers. The most recent versions treat values of Int as signed 32-bit vectors, and require the use of BigInt to represent unbounded integers.

In the provided example, Leon times out attempting to build a list of size Int.MaxValue, a counter-example which would demonstrate that the postcondition does not hold for bounded integers.

If you change the return type of size to BigInt, the program verifies as expected.