diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala
index 8c950fd87215da16ebdebc1b13c88dbb78ba66e3..176cb96b1f9fe411be0553afca3a31895d7e962a 100644
--- a/src/main/scala/leon/Analysis.scala
+++ b/src/main/scala/leon/Analysis.scala
@@ -68,6 +68,7 @@ class Analysis(val program : Program, val reporter: Reporter = Settings.reporter
         allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef)
         allVCs ++= tactic.generatePostconditions(funDef)
         allVCs ++= tactic.generateMiscCorrectnessConditions(funDef)
+        allVCs ++= tactic.generateArrayAccessChecks(funDef)
       }
       allVCs = allVCs.sortWith((vc1, vc2) => {
         val id1 = vc1.funDef.id.name
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 06c31189a731514afbf9ee27c74cfea323ae0622..5ff33521d54e023a6c4838051860078f2c483ba1 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -35,7 +35,7 @@ object ArrayTransformation extends Pass {
       IfExpr(
         And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
         ArraySelect(TupleSelect(ar, 1), ir).setType(sel.getType),
-        Error("Array out of bound access").setType(sel.getType)
+        Error("Index out of bound").setType(sel.getType)
       ).setType(sel.getType)
     }
     case ArrayUpdate(a, i, v) => {
@@ -49,7 +49,7 @@ object ArrayTransformation extends Pass {
       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("Array out of bound access").setType(Int32Type)
+        Error("Index out of bound").setType(Int32Type)
       ).setType(Int32Type)
     }
 
diff --git a/src/main/scala/leon/DefaultTactic.scala b/src/main/scala/leon/DefaultTactic.scala
index a01d025431c2ec3c704a1950410334fd322abae9..70ad17f36150a47f846fe67a8bf8db350e03a9bf 100644
--- a/src/main/scala/leon/DefaultTactic.scala
+++ b/src/main/scala/leon/DefaultTactic.scala
@@ -194,6 +194,35 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
       toRet
     }
 
+    def generateArrayAccessChecks(function: FunDef) : Seq[VerificationCondition] = {
+      val toRet = if (function.hasBody) {
+        val cleanBody = matchToIfThenElse(function.body.get)
+
+        val allPathConds = collectWithPathCondition((t => t match {
+          case Error("Index out of bound") => true
+          case _ => false
+        }), cleanBody)
+
+        def withPrecIfDefined(conds: Seq[Expr]) : Expr = if (function.hasPrecondition) {
+          Not(And(mapGetWithChecks(matchToIfThenElse(function.precondition.get)), And(conds)))
+        } else {
+          Not(And(conds))
+        }
+
+        allPathConds.map(pc =>
+          new VerificationCondition(
+            withPrecIfDefined(pc._1),
+            if(function.fromLoop) function.parent.get else function,
+            VCKind.ArrayAccess,
+            this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
+        ).toSeq
+      } else {
+        Seq.empty
+      }
+
+      toRet
+    }
+
     def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition] = {
       generateMapAccessChecks(function)
     }
diff --git a/src/main/scala/leon/Extensions.scala b/src/main/scala/leon/Extensions.scala
index 5905ec99820c7dff51cef6fef88705017a17614d..1ddb97e7c774b029c421c551129d015c880a8062 100644
--- a/src/main/scala/leon/Extensions.scala
+++ b/src/main/scala/leon/Extensions.scala
@@ -46,6 +46,7 @@ object Extensions {
     def generatePreconditions(function: FunDef) : Seq[VerificationCondition]
     def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[VerificationCondition]
     def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition]
+    def generateArrayAccessChecks(function: FunDef) : Seq[VerificationCondition]
   }
 
   // The rest of the code is for dynamically loading extensions
diff --git a/src/main/scala/leon/VerificationCondition.scala b/src/main/scala/leon/VerificationCondition.scala
index 01545bc3e87bd3606591b464f59098a5b0d8dd8c..e5556f1acf52fa3f8472556bcc66d3572c032488 100644
--- a/src/main/scala/leon/VerificationCondition.scala
+++ b/src/main/scala/leon/VerificationCondition.scala
@@ -49,6 +49,7 @@ object VCKind extends Enumeration {
   val Postcondition = Value("postcond.")
   val ExhaustiveMatch = Value("match.")
   val MapAccess = Value("map acc.")
+  val ArrayAccess = Value("arr. acc.")
   val InvariantInit = Value("inv init.")
   val InvariantInd = Value("inv ind.")
   val InvariantPost = Value("inv post.")