diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index d25965ede6a34f8de6206ec1b38cb0e6381b3d41..294bc4fefbf2ec0fb5f47d11bc8f7d3f5b5d4b04 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -73,11 +73,11 @@ object ArrayTransformation extends Pass {
       val length = TupleSelect(ar, 2).setType(Int32Type)
       IfExpr(
         And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
-        ArraySelect(TupleSelect(ar, 1), ir).setType(sel.getType),
-        Error("Index out of bound").setType(sel.getType)
+        ArraySelect(TupleSelect(ar, 1), ir).setType(sel.getType).setPosInfo(sel),
+        Error("Index out of bound").setType(sel.getType).setPosInfo(sel)
       ).setType(sel.getType)
     }
-    case ArrayUpdate(a, i, v) => {
+    case up@ArrayUpdate(a, i, v) => {
       val ar = transform(a)
       val ir = transform(i)
       val vr = transform(v)
@@ -87,8 +87,15 @@ object ArrayTransformation extends Pass {
       //val Tuple(Seq(Variable(id), length)) = ar
       IfExpr(
         And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
-        Block(Seq(Assignment(id, Tuple(Seq(ArrayUpdated(array, i, v).setType(array.getType), length)).setType(TupleType(Seq(array.getType, Int32Type))))), IntLiteral(0)),
-        Error("Index out of bound").setType(Int32Type)
+        Block(Seq(
+          Assignment(
+            id, 
+            Tuple(Seq(
+              ArrayUpdated(array, i, v).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)
     }
     case ArrayLength(a) => {
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 61b6f9ee540c4e2dc224c2b88bc02de7540ca4dd..3a3cfc305c8292e82966c0b0b759989b4cab3c69 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -790,7 +790,7 @@ trait CodeExtraction extends Extractors {
             }
             case ArrayType(bt) => {
               assert(rargs.size == 1)
-              ArraySelect(rlhs, rargs.head).setType(bt)
+              ArraySelect(rlhs, rargs.head).setType(bt).setPosInfo(app.pos.line, app.pos.column)
             }
             case _ => {
               if (!silent) unit.error(tree.pos, "apply on unexpected type")
@@ -799,11 +799,11 @@ trait CodeExtraction extends Extractors {
           }
         }
         // for now update only happens with array. later it might have to be distinguish in function of the lhs
-        case ExUpdate(lhs, index, newValue) => { 
+        case update@ExUpdate(lhs, index, newValue) => { 
           val lhsRec = rec(lhs)
           val indexRec = rec(index)
           val newValueRec = rec(newValue)
-          ArrayUpdate(lhsRec, indexRec, newValueRec).setType(newValueRec.getType)
+          ArrayUpdate(lhsRec, indexRec, newValueRec).setType(newValueRec.getType).setPosInfo(update.pos.line, update.pos.column)
         }
         case ExArrayLength(t) => {
           val rt = rec(t)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 030845358b5efe100e15ef31215f820031c3cd98..93bf6fd97268f1e95cdca875edc7e39c58040eb0 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -382,11 +382,11 @@ object Trees {
   /* Array operations */
   case class ArrayFill(length: Expr, defaultValue: Expr) extends Expr
   case class ArrayMake(defaultValue: Expr) extends Expr
-  case class ArraySelect(array: Expr, index: Expr) extends Expr
+  case class ArraySelect(array: Expr, index: Expr) extends Expr with ScalacPositional
   //the difference between ArrayUpdate and ArrayUpdated is that the former has a side effect while the latter is the function variant
   //ArrayUpdate should be eliminated soon in the analysis while ArrayUpdated is keep all the way to the backend
-  case class ArrayUpdate(array: Expr, index: Expr, newValue: Expr) extends Expr
-  case class ArrayUpdated(array: Expr, index: Expr, newValue: Expr) extends Expr 
+  case class ArrayUpdate(array: Expr, index: Expr, newValue: Expr) extends Expr with ScalacPositional
+  case class ArrayUpdated(array: Expr, index: Expr, newValue: Expr) extends Expr with ScalacPositional
   case class ArrayLength(array: Expr) extends Expr with FixedType {
     val fixedType = Int32Type
   }