diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 9d7369d9995453e62508e37394dd75fd55f0138b..8ec32c5d8d0285a1328a9e1729354a8d5959ec53 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -855,6 +855,7 @@ object TreeOps {
     case SetType(baseType) => FiniteSet(Seq()).setType(tpe)
     case MapType(fromType, toType) => FiniteMap(Seq()).setType(tpe)
     case TupleType(tpes) => Tuple(tpes.map(simplestValue))
+    case ArrayType(tpe) => ArrayFill(IntLiteral(0), simplestValue(tpe))
     case _ => throw new Exception("I can't choose simplest value for type " + tpe)
   }
 
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 0a53b4c908ee4a5b3b7d58654fcb9351e15f7cb8..0b29dd89c122f8728e43799cfa63d39ec44577b6 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -542,6 +542,8 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
 
   protected[leon] def fromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: Option[TypeTree] = None) : Expr = {
     def rec(t: Z3AST, expType: Option[TypeTree] = None) : Expr = expType match {
+      case _ if z3IdToExpr contains t => z3IdToExpr(t)
+
       case Some(MapType(kt,vt)) => 
         model.getArrayValue(t) match {
           case None => throw new CantTranslateException(t)