Good catch. Leon indeed currently models the `Int` type as mathematical (unbounded) integers. There is a project in the works to correct this semantic differenc

Good catch. Leon indeed currently models the `Int` type as mathematical (unbounded) integers. There is a project in the works to correct this semantic difference with Scala, and have `Int` be signed 32-bit bitvectors and `BigInt` be the mathematical integers. At that stage, Leon will also be able to generate the kind of bound checks you were expecting. For the types of problems we had been looking at, the current state is arguably not a major issue (if you are really building a list of 2^31 elements, you're probably facing other problems), but for the sake of being formal, the semantic mismatch must be addressed.