fix extractors for Arrays

src/main/scala/leon/purescala/Extractors.scala

@@ -228,10 +228,12 @@ object Extractors {
         (as: Seq[Expr]) => ArrayUpdated(as(0), as(1), as(2))
       ))
       case NonemptyArray(elems, Some((default, length))) =>
-        val all = elems.values.toSeq :+ default :+ length
+        val elemsSeq: Seq[(Int, Expr)] = elems.toSeq
+        val all = elemsSeq.map(_._2) :+ default :+ length
         Some((all, as => {
           val l = as.length
-          nonemptyArray(as.take(l - 2), Some((as(l - 2), as(l - 1))))
+          NonemptyArray(elemsSeq.map(_._1).zip(as.take(l - 2)).toMap, 
+                        Some((as(l - 2), as(l - 1))))
         }))
       case na @ NonemptyArray(elems, None) =>
         val ArrayType(tpe) = na.getType
@@ -239,7 +241,7 @@ object Extractors {
 
         Some((
           elsOrdered,
-          es => finiteArray(indexes.zip(es).toMap, None, tpe)
+          es => NonemptyArray(indexes.zip(es).toMap, None)
         ))
       case Tuple(args) => Some((args, es => Tuple(es)))
       case IfExpr(cond, thenn, elze) => Some((

src/test/scala/leon/unit/purescala/ExtractorsSuite.scala

@@ -25,17 +25,24 @@ class ExtractorsSuite extends FunSuite with ExpressionsDSL {
     assert(e3 === e4)
   }
 
-  ignore("Extractors of NonemptyArray with sparse elements") {
+  test("Extractors of NonemptyArray with sparse elements") {
     val a1 = NonemptyArray(Map(0 -> x, 3 -> y, 5 -> z), Some((BigInt(0), BigInt(10))))
-
     val a2 = a1 match {
       case Operator(es, builder) => {
         assert(es === Seq(x, y, z, InfiniteIntegerLiteral(0), InfiniteIntegerLiteral(10)))
         builder(es)
       }
     }
-
     assert(a2 === a1)
+
+    val a3 = NonemptyArray(Map(0 -> x, 1 -> y, 2 -> z), None)
+    val a4 = a3 match {
+      case Operator(es, builder) => {
+        assert(es === Seq(x, y, z))
+        builder(es)
+      }
+    }
+    assert(a3 === a4)
   }
 
 }