Implement solver support for FiniteArray

src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala

@@ -522,6 +522,14 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
           val res = getLength(ar)
           res
         }
+
+        case arr @ FiniteArray(exprs) => {
+          val ArrayType(innerType) = arr.getType
+          val arrayType = arr.getType
+          val a: Expr = ArrayFill(IntLiteral(exprs.length), simplestValue(innerType)).setType(arrayType)
+          val u = exprs.zipWithIndex.foldLeft(a)((array, expI) => ArrayUpdated(array, IntLiteral(expI._2), expI._1).setType(arrayType))
+          rec(u)
+        }
         case Distinct(exs) => z3.mkDistinct(exs.map(rec(_)): _*)
   
         case _ => {