diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 5ff33521d54e023a6c4838051860078f2c483ba1..95e8719b1913c5c22bcc9d3a1108d949d2e4046d 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -52,7 +52,10 @@ object ArrayTransformation extends Pass {
         Error("Index out of bound").setType(Int32Type)
       ).setType(Int32Type)
     }
-
+    case ArrayLength(a) => {
+      val ar = transform(a)
+      TupleSelect(ar, 2).setType(Int32Type)
+    }
     case Let(i, v, b) => {
       val vr = transform(v)
       v.getType match {
@@ -68,7 +71,11 @@ object ArrayTransformation extends Pass {
         }
       }
     }
-    //case LetVar(id, e, b) =>
+    case LetVar(id, e, b) => {
+      val er = transform(e)
+      val br = transform(b)
+      LetVar(id, er, br)
+    }
 
     //case ite@IfExpr(cond, tExpr, eExpr) => 
 
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 1a760f3fe58956546b931a4019d86410c469abc9..61b6f9ee540c4e2dc224c2b88bc02de7540ca4dd 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -805,6 +805,10 @@ trait CodeExtraction extends Extractors {
           val newValueRec = rec(newValue)
           ArrayUpdate(lhsRec, indexRec, newValueRec).setType(newValueRec.getType)
         }
+        case ExArrayLength(t) => {
+          val rt = rec(t)
+          ArrayLength(rt)
+        }
         case ExArrayFill(baseType, length, defaultValue) => {
           val underlying = scalaType2PureScala(unit, silent)(baseType.tpe)
           val lengthRec = rec(length)
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 020cc2537fefc0c5755dc7d3f294ff0fcfa22704..2c5bbeab919d60dc3bd1ecbedc3aca0a65d0ac1b 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -662,6 +662,14 @@ trait Extractors {
       }
     }
 
+    object ExArrayLength {
+      def unapply(tree: Select): Option[Tree] = tree match {
+        case Select(t, n) if (n.toString == "length") => Some(t)
+        case _ => None
+      }
+
+    }
+
     object ExArrayFill {
       def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match {
         case Apply(
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index a82ad435fe461ba4445e42b273745f1b660b8015..848c1dad3fcd565ff222fe6b0b03ca7effd69c3e 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -249,6 +249,10 @@ object PrettyPrinter {
       nsb = ppNary(nsb, Seq(k), "(", ",", ")", lvl)
       nsb
     }
+    case ArrayLength(a) => {
+      pp(a, sb, lvl)
+      sb.append(".length")
+    }
     case fill@ArrayFill(size, v) => {
       sb.append("Array.fill(")
       pp(size, sb, lvl)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 6f103ad8017dc641020d392b4c2f3b7c17800146..b308dbf53073f80667b4d1ffedcf2507a1b5b410 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -386,6 +386,9 @@ object Trees {
   //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 ArrayLength(array: Expr) extends Expr with FixedType {
+    val fixedType = Int32Type
+  }
 
   /* List operations */
   case class NilList(baseType: TypeTree) extends Expr with Terminal
@@ -419,6 +422,7 @@ object Trees {
       case CaseClassInstanceOf(cd, e) => Some((e, CaseClassInstanceOf(cd, _)))
       case Assignment(id, e) => Some((e, Assignment(id, _)))
       case TupleSelect(t, i) => Some((t, TupleSelect(_, i)))
+      case ArrayLength(a) => Some((a, ArrayLength))
       case e@Epsilon(t) => Some((t, (expr: Expr) => Epsilon(expr).setType(e.getType).setPosInfo(e)))
       case _ => None
     }
diff --git a/testcases/regression/valid/Array2.scala b/testcases/regression/valid/Array2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4f149a9305cb4b53a4a9353b82e25468c898bdc8
--- /dev/null
+++ b/testcases/regression/valid/Array2.scala
@@ -0,0 +1,9 @@
+object Array2 {
+
+  def foo(): Int = {
+    val a = Array.fill(5)(0)
+    a(2) = 3
+    a.length
+  } ensuring(_ == 5)
+
+}
diff --git a/testcases/regression/valid/Array3.scala b/testcases/regression/valid/Array3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d51894c3651613ee8c5a79eaa3c99c38c4a72f5f
--- /dev/null
+++ b/testcases/regression/valid/Array3.scala
@@ -0,0 +1,14 @@
+object Array1 {
+
+  def foo(): Int = {
+    val a = Array.fill(5)(0)
+    var i = 0
+    var sum = 0
+    while(i < a.length) {
+      sum = sum + a(i)
+      i = i + 1
+    }
+    sum
+  } ensuring(_ == 0)
+
+}