diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 7afb63104bc42fdf752f3e653f4a801a15d7f507..7f0e5b0180bd9318cb3b8cd109ae1b01d843b9c1 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -286,11 +286,22 @@ object DefOps {
     }
   }
 
-  private def defaultFiMap(fi: FunctionInvocation, nfd: FunDef): Option[Expr] = (fi, nfd) match {
-    case (FunctionInvocation(old, args), newfd) if old.fd != newfd =>
-      Some(FunctionInvocation(newfd.typed(old.tps), args))
-    case _ =>
-      None
+  def replaceDefsInProgram(p: Program)(fdMap: Map[FunDef, FunDef] = Map.empty,
+                                       cdMap: Map[ClassDef, ClassDef] = Map.empty): Program = {
+    p.copy(units = for (u <- p.units) yield {
+      u.copy(defs = u.defs.map {
+        case m : ModuleDef =>
+          m.copy(defs = for (df <- m.defs) yield {
+            df match {
+              case cd : ClassDef => cdMap.getOrElse(cd, cd)
+              case fd : FunDef => fdMap.getOrElse(fd, fd)
+              case d => d
+            }
+        })
+        case cd: ClassDef => cdMap.getOrElse(cd, cd)
+        case d => d
+      })
+    })
   }
 
   def replaceDefs(p: Program)(fdMapF: FunDef => Option[FunDef],
@@ -365,22 +376,17 @@ object DefOps {
       nfd.fullBody = transformer.transform(fd.fullBody)(bindings)
     }
 
-    val newP = p.copy(units = for (u <- p.units) yield {
-      u.copy(defs = u.defs.map {
-        case m : ModuleDef =>
-          m.copy(defs = for (df <- m.defs) yield {
-            df match {
-              case cd : ClassDef => transformer.transform(cd)
-              case fd : FunDef => transformer.transform(fd)
-              case d => d
-            }
-        })
-        case cd: ClassDef => transformer.transform(cd)
-        case d => d
-      })
-    })
+    val fdsMap = fdMap.toMap
+    val cdsMap = cdMap.toMap
+    val newP = replaceDefsInProgram(p)(fdsMap, cdsMap)
+    (newP, idMap.toMap, fdsMap, cdsMap)
+  }
 
-    (newP, idMap.toMap, fdMap.toMap, cdMap.toMap)
+  private def defaultFiMap(fi: FunctionInvocation, nfd: FunDef): Option[Expr] = (fi, nfd) match {
+    case (FunctionInvocation(old, args), newfd) if old.fd != newfd =>
+      Some(FunctionInvocation(newfd.typed(old.tps), args))
+    case _ =>
+      None
   }
 
   /** Clones the given program by replacing some functions by other functions.
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 95f924a4628055fa855080a035210495ac8f7012..99e1070273b762b824fd0b1543f1ecb035b53c3f 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -91,9 +91,13 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program, theo
 
             for (me <- smodel) me match {
               case DefineFun(SMTFunDef(s, args, kind, e)) if syms(s) =>
-                val id = variables.toA(s)
-                val value = fromSMT(e, id.getType)(Map(), modelFunDefs)
-                model += ids.getAorElse(id, id) -> theories.decode(value)(variablesOf(value).map(id => id -> ids.toA(id)).toMap)
+                try {
+                  val id = variables.toA(s)
+                  val value = fromSMT(e, id.getType)(Map(), modelFunDefs)
+                  model += ids.getAorElse(id, id) -> theories.decode(value)(variablesOf(value).map(id => id -> ids.toA(id)).toMap)
+                } catch {
+                  case _: Unsupported =>
+                }
               case _ =>
             }
 
diff --git a/src/main/scala/leon/solvers/unrolling/DatatypeManager.scala b/src/main/scala/leon/solvers/unrolling/DatatypeManager.scala
index 275621828b84a4e1e1302a5c678a1cd87eff744b..554689830fe4b61442e6272cd658c9212da93da8 100644
--- a/src/main/scala/leon/solvers/unrolling/DatatypeManager.scala
+++ b/src/main/scala/leon/solvers/unrolling/DatatypeManager.scala
@@ -157,6 +157,8 @@ class DatatypeManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(en
         case BooleanType | UnitType | CharType | IntegerType |
              RealType | Int32Type | StringType | (_: TypeParameter) => false
 
+        case at: ArrayType => true
+
         case NAryType(tpes, _) => tpes.exists(requireTypeUnrolling)
       }
 
@@ -205,6 +207,9 @@ class DatatypeManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(en
     case FunctionType(_, _) =>
       FreshFunction(expr)
 
+    case at: ArrayType =>
+      GreaterEquals(ArrayLength(expr), IntLiteral(0))
+
     case _ => scala.sys.error("TODO")
   }
 
diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
index 601aa84eb716d4422e75a7f4d3a23d0ca2a67a68..76f18864b453df290c372af35658707525058224 100644
--- a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
@@ -388,13 +388,9 @@ trait AbstractUnrollingSolver[T]
 
                 if (this.feelingLucky) {
                   // we might have been lucky :D
-                  try {
-                    val extracted = extractModel(model)
-                    val valid = validateModel(extracted, assumptionsSeq, silenceErrors = true)
-                    if (valid) foundAnswer(Some(true), extracted)
-                  } catch {
-                    case u: Unsupported =>
-                  }
+                  val extracted = extractModel(model)
+                  val valid = validateModel(extracted, assumptionsSeq, silenceErrors = true)
+                  if (valid) foundAnswer(Some(true), extracted)
                 }
 
                 if (!foundDefinitiveAnswer) {
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index f1ea90043736d1ea59a5ae0d9747e15905509cd6..0cfc68d50381276e7c3ed5c28c2566086f8cb315 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -55,9 +55,7 @@ object AntiAliasingPhase extends TransformationPhase {
       updateBody(fd, effects, updatedFunctions, varsInScope)(ctx)
     }
 
-    val res = replaceFunDefs(pgm)(fd => updatedFunctions.get(fd), (fi, fd) => None)
-    //println(res._1)
-    res._1
+    replaceDefsInProgram(pgm)(updatedFunctions)
   }
 
   /*