diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 0b29dd89c122f8728e43799cfa63d39ec44577b6..1a94e295fb9669242bde48a8e0b7b8550578e1ff 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/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 _ => {