diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 728b602f9fa343ae8657a2922ca03a3dfe1ada3f..7625eddf86a1656c96b46a9ad7fb3fd2d894dae2 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -161,7 +161,7 @@ object Constructors {
       BooleanLiteral(true)
     }
   }
-  /** $encodingof `... match { ... }` but simplified if possible. Throws an error if no case can match the scrutined expression.
+  /** $encodingof `... match { ... }` but simplified if possible. Simplifies to [[Error]] if no case can match the scrutined expression.
     * @see [[purescala.Expressions.MatchExpr MatchExpr]]
     */
   def matchExpr(scrutinee : Expr, cases : Seq[MatchCase]) : Expr ={
@@ -249,8 +249,8 @@ object Constructors {
   /** $encodingof Simplified `Array(...)` (array length defined at compile-time)
     * @see [[purescala.Expressions.NonemptyArray NonemptyArray]]
     */
-  def finiteArray(els: Seq[Expr]): Expr = {
-    require(els.nonEmpty)
+  def finiteArray(els: Seq[Expr], tpe: TypeTree = Untyped): Expr = {
+    require(els.nonEmpty || tpe != Untyped)
     finiteArray(els, None, Untyped) // Untyped is not correct, but will not be used anyway
   }
   /** $encodingof Simplified `Array[...](...)` (array length and default element defined at run-time) with type information
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index cd57d2187fe0cd59d45e3d88e17b0926e2279412..1337e74d0331775be13e7d1d3311281c630ffdef 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -181,9 +181,14 @@ object Extractors {
           val l = as.length
           nonemptyArray(as.take(l - 2), Some((as(l - 2), as(l - 1))))
         }))
-      case NonemptyArray(elems, None) =>
-        val all = elems.values.toSeq
-        Some((all, finiteArray))
+      case na@NonemptyArray(elems, None) =>
+        val ArrayType(tpe) = na.getType
+        val (indexes, elsOrdered) = elems.toSeq.unzip
+
+        Some((
+          elsOrdered,
+          es => finiteArray(indexes.zip(es).toMap, None, tpe)
+        ))
       case Tuple(args) => Some((args, tupleWrap))
       case IfExpr(cond, thenn, elze) => Some((
         Seq(cond, thenn, elze),