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

object BigArray {

  def big(a: Array[Int]): Int = {
    require(a.length >= 10 && a(7) == 42)
    a.length
  } ensuring(_ <= 1000000000)

}

Refactor FiniteArray to an implicit representation
Refactor FiniteArray to an implicit representation

FiniteArray now takes an Expr for the length, a default
Expr, and a Map of defined Expr for some of its elements.
Adapt the rest of Leon to the new trees.

The PrettyPrinter tries to be a little bit smart about
how to print the array, only printing a few elements when the
array gets too big. The regression test produces an
huge array counter-example that used to lead to a crash of
Leon with the previous implementation of Array (fully represented
in memory).
