From 0c62931b9a1433d3997bcd4fa29e861d3607171d Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Wed, 27 Feb 2013 17:52:35 +0100
Subject: [PATCH] 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           | 1 +
 src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 9d7369d99..8ec32c5d8 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 0a53b4c90..0b29dd89c 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)
-- 
GitLab