convert array to pair of array and length

src/main/scala/leon/ArrayTransformation.scala

@@ -48,9 +48,9 @@ object ArrayTransformation extends Pass {
       //val Tuple(Seq(Variable(id), length)) = ar
       IfExpr(
         And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
-        Assignment(id, Tuple(Seq(ArrayUpdated(array, i, v), length)).setType(TupleType(Seq(array.getType, Int32Type)))),
-        Error("Array out of bound access").setType(UnitType)
-      ).setType(UnitType)
+        Block(Seq(Assignment(id, Tuple(Seq(ArrayUpdated(array, i, v), length)).setType(TupleType(Seq(array.getType, Int32Type))))), IntLiteral(0)),
+        Error("Array out of bound access").setType(Int32Type)
+      ).setType(Int32Type)
     }
 
     case Let(i, v, b) => {

src/main/scala/leon/FairZ3Solver.scala

@@ -59,6 +59,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
     fallbackSorts = Map.empty
 
     mapSorts = Map.empty
+    arraySorts = Map.empty
     funSorts = Map.empty
     funDomainConstructors = Map.empty
     funDomainSelectors = Map.empty
@@ -97,6 +98,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
   private var boolSort: Z3Sort = null
   private var setSorts: Map[TypeTree, Z3Sort] = Map.empty
   private var mapSorts: Map[TypeTree, Z3Sort] = Map.empty
+  private var arraySorts: Map[TypeTree, Z3Sort] = Map.empty
 
   protected[leon] var funSorts: Map[TypeTree, Z3Sort] = Map.empty
   protected[leon] var funDomainConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
@@ -386,6 +388,16 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
         ms
       }
     }
+    case at @ ArrayType(base) => arraySorts.get(at) match {
+      case Some(s) => s
+      case None => {
+        val fromSort = typeToSort(Int32Type)
+        val toSort = typeToSort(base)
+        val as = z3.mkArraySort(fromSort, toSort)
+        arraySorts += (at -> as)
+        as
+      }
+    }
     case ft @ FunctionType(fts, tt) => funSorts.get(ft) match {
       case Some(s) => s
       case None => {
@@ -1043,6 +1055,16 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
           case MapType(ft, tt) => z3.mkDistinct(z3.mkSelect(rec(m), rec(k)), mapRangeNoneConstructors(tt)())
           case errorType => scala.sys.error("Unexpected type for map: " + (ex, errorType))
         }
+        case fill@ArrayFill(length, default) => {
+          val ArrayType(base) = fill.getType
+          z3.mkConstArray(typeToSort(base), rec(default))
+        }
+        case ArraySelect(ar, index) => {
+          z3.mkSelect(rec(ar), rec(index))
+        }
+        case ArrayUpdated(ar, index, newVal) => {
+          z3.mkStore(rec(ar), rec(index), rec(newVal))
+        }
         case AnonymousFunctionInvocation(id, args) => id.getType match {
           case ft @ FunctionType(fts, tt) => {
             val consFD = funDomainConstructors(ft)

src/main/scala/leon/ImperativeCodeElimination.scala

@@ -15,11 +15,9 @@ object ImperativeCodeElimination extends Pass {
   def apply(pgm: Program): Program = {
     val allFuns = pgm.definedFunctions
     allFuns.foreach(fd => fd.body.map(body => {
-      Logger.debug("Transforming to functional code the following function:\n" + fd, 5, "imperative")
       parent = fd
       val (res, scope, _) = toFunction(body)
       fd.body = Some(scope(res))
-      Logger.debug("Resulting functional code is:\n" + fd, 5, "imperative")
     }))
     pgm
   }