diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 6f9c3101defff497d48fe92493544501f35928f5..dd71afeec907abd4ed1b0df0a507750a857d544a 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -310,8 +310,8 @@ trait CodeExtraction extends Extractors {
       throw new ImpureCodeEncounteredException(null)
     }
     def unsupported(tr: Tree, msg: String): Nothing = {
-      reporter.error(tr.pos, tr.toString)
       reporter.error(tr.pos, msg)
+      reporter.error(tr.pos, tr.toString)
       throw new ImpureCodeEncounteredException(tr)
     }
 
@@ -390,15 +390,18 @@ trait CodeExtraction extends Extractors {
       var rest = tmpRest
 
       val res = current match {
+        case ExArrayLiteral(tpe, args) =>
+          FiniteArray(args.map(extractTree)).setType(ArrayType(extractType(tpe)))
+
         case ExCaseObject(sym) =>
           classesToClasses.get(sym) match {
             case Some(ccd: CaseClassDef) =>
               CaseClass(ccd, Seq())
-
             case _ =>
-              unsupported(tr, "Unknown case class "+sym.name)
+              unsupported(tr, "Unknown case object "+sym.name)
           }
 
+
         case ExParameterlessMethodCall(t,n) if extractTree(t).getType.isInstanceOf[CaseClassType] =>
           val selector = extractTree(t)
           val selType = selector.getType
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 00da888f67181eecb21e62118b263e8ec326c6f3..8735654d7813bf2e86777a5964400638977a4f1c 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -310,6 +310,23 @@ trait Extractors {
       }
     }
 
+    object ExArrayLiteral {
+      def unapply(tree: Apply): Option[(Type, Seq[Tree])] = tree match {
+        case Apply(ExSelected("scala", "Array", "apply"), args) =>
+          tree.tpe match {
+            case TypeRef(_, _, List(t1)) =>
+              Some((t1, args))
+            case _ =>
+              None
+          }
+        case Apply(Apply(TypeApply(ExSelected("scala", "Array", "apply"), List(tpt)), args), ctags) =>
+          Some((tpt.tpe, args))
+
+        case _ =>
+          None
+      }
+    }
+
     object ExTuple {
       def unapply(tree: Apply): Option[(Seq[Type], Seq[Tree])] = tree match {
         case Apply(
diff --git a/src/test/resources/regression/verification/purescala/valid/ArrayLiterals.scala b/src/test/resources/regression/verification/purescala/valid/ArrayLiterals.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2ce0669e612100ca51bd542808a5a28517f11054
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/ArrayLiterals.scala
@@ -0,0 +1,8 @@
+import leon.Utils._
+object Numerals {
+  def foo(): Int = {
+    val b : Array[Int] = Array[Int](1,2,3)
+    val a : Array[Int] = Array(1,2,3)
+    a.length
+  } ensuring { _ > 0 }
+}