diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala index 71ff17c26e58970fad14f7b96b36afd3641827e9..c6c6dafc208259d07046a0afec7b42d54dab5a5d 100644 --- a/src/main/scala/leon/ArrayTransformation.scala +++ b/src/main/scala/leon/ArrayTransformation.scala @@ -77,7 +77,7 @@ object ArrayTransformation extends Pass { val length = TupleSelect(ar, 2).setType(Int32Type) IfExpr( And(GreaterEquals(ir, IntLiteral(0)), LessThan(ir, length)), - ArraySelect(TupleSelect(ar, 1), ir).setType(sel.getType).setPosInfo(sel), + ArraySelect(TupleSelect(ar, 1).setType(ArrayType(sel.getType)), ir).setType(sel.getType).setPosInfo(sel), Error("Index out of bound").setType(sel.getType).setPosInfo(sel) ).setType(sel.getType) } diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala index 7983e48b0565afb844ed91b18f79c001c6439600..0410fd11a3c833d5b9cff040bde5fe33fcb6b195 100644 --- a/src/main/scala/leon/purescala/TypeTrees.scala +++ b/src/main/scala/leon/purescala/TypeTrees.scala @@ -100,6 +100,7 @@ object TypeTrees { case UnitType => FiniteSize(1) case Int32Type => InfiniteSize case ListType(_) => InfiniteSize + case ArrayType(_) => InfiniteSize case TupleType(bases) => { val baseSizes = bases.map(domainSize(_)) baseSizes.find(_ == InfiniteSize) match {