diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala index 6a2afc155d312409641d0f564d5f37ddb150af5f..71ff17c26e58970fad14f7b96b36afd3641827e9 100644 --- a/src/main/scala/leon/ArrayTransformation.scala +++ b/src/main/scala/leon/ArrayTransformation.scala @@ -90,16 +90,14 @@ object ArrayTransformation extends Pass { val array = TupleSelect(ar, 1).setType(ArrayType(v.getType)) IfExpr( And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)), - Block(Seq( - Assignment( - id, - Tuple(Seq( - ArrayUpdated(array, ir, vr).setType(array.getType).setPosInfo(up), - length) - ).setType(TupleType(Seq(array.getType, Int32Type))))), - IntLiteral(0)), - Error("Index out of bound").setType(Int32Type).setPosInfo(up) - ).setType(Int32Type) + Assignment( + id, + Tuple(Seq( + ArrayUpdated(array, ir, vr).setType(array.getType).setPosInfo(up), + length) + ).setType(TupleType(Seq(array.getType, Int32Type)))), + Error("Index out of bound").setType(UnitType).setPosInfo(up) + ).setType(UnitType) } case ArrayLength(a) => { val ar = transform(a)