NonEmptyArray is required to be nonempty
Allow arbitrary expression as length in CodeGeneration
Handle FiniteArray in valueToJVM
Add integration tests
finiteArray makes EmptyArray for arrays of size 0
Fail when z3 returns negative size array