Add array support in simplestValue, fix for certain array models

Z3 may return an id->id model for array kinds, leading to an assertion
error caused by the expectation of getting an array literal. We
shortcircuit with z3IdToExpr to catch such cases for all kinds.

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)
   }
 

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)