diff --git a/build.sbt b/build.sbt
index b649370c0ba2a6ea63d052958b82dccfd2107587..372c4cb07a8a429a2405ab61be47060b457fa63b 100644
--- a/build.sbt
+++ b/build.sbt
@@ -40,17 +40,13 @@ resolvers ++= Seq(
   "Sonatype OSS Releases" at "https://oss.sonatype.org/content/repositories/releases"
 )
 
-val libisabelleVer = "0.3.1"
-
 libraryDependencies ++= Seq(
   "org.scala-lang" % "scala-compiler" % scalaVer,
-  "org.scalatest" %% "scalatest" % "2.2.4" % "test",
+  "org.scalatest" %% "scalatest" % "2.2.4" % "test;it",
   "com.typesafe.akka" %% "akka-actor" % "2.3.4",
-  "info.hupel" %% "libisabelle" % libisabelleVer,
-  "info.hupel" %% "libisabelle-setup" % libisabelleVer,
-  "info.hupel" %% "slf4j-impl-helper" % "0.1" % "optional",
   "org.ow2.asm" % "asm-all" % "5.0.4",
-  "com.fasterxml.jackson.module" %% "jackson-module-scala" % "2.6.0-rc2"//,
+  "com.fasterxml.jackson.module" %% "jackson-module-scala" % "2.6.0-rc2",
+  "org.apache.commons" % "commons-lang3" % "3.4"
   //"com.regblanc" %% "scala-smtlib" % "0.2"
 )
 
@@ -133,14 +129,9 @@ def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${versi
 lazy val bonsai      = ghProject("git://github.com/colder/bonsai.git",     "10eaaee4ea0ff6567f4f866922cb871bae2da0ac")
 lazy val scalaSmtlib = ghProject("git://github.com/regb/scala-smtlib.git", "88835c02ca2528e888b06bc48e4e93e52dc5f4b5")
 
-lazy val root = (project in file(".")).
-  configs(IntegrationTest).
-  configs(RegressionTest, NativeZ3RegressionTest, IsabelleTest).
-  dependsOn(bonsai).
-  dependsOn(scalaSmtlib).
-  settings(inConfig(NativeZ3RegressionTest)(Defaults.testTasks ++ testSettings): _*).
-  settings(inConfig(RegressionTest)(Defaults.testTasks ++ testSettings): _*).
-  //settings(inConfig(IntegrTest)(Defaults.testTasks ++ testSettings): _*).
-  settings(inConfig(IsabelleTest)(Defaults.testTasks ++ testSettings): _*).
-  settings(inConfig(Test)(Defaults.testTasks ++ testSettings): _*)
+lazy val root = (project in file("."))
+  .configs(IntegrationTest)
+  .settings(Defaults.itSettings : _*)
+  .dependsOn(bonsai)
+  .dependsOn(scalaSmtlib)
 
diff --git a/src/it/InoxTestSuite.scala b/src/it/scala/inox/InoxTestSuite.scala
similarity index 100%
rename from src/it/InoxTestSuite.scala
rename to src/it/scala/inox/InoxTestSuite.scala
diff --git a/src/it/SolvingTestSuite.scala b/src/it/scala/inox/SolvingTestSuite.scala
similarity index 69%
rename from src/it/SolvingTestSuite.scala
rename to src/it/scala/inox/SolvingTestSuite.scala
index a522214ef896964737ff111e69bd58c255a84027..348906f82f787e3a6c0c11448c11b80691d802ae 100644
--- a/src/it/SolvingTestSuite.scala
+++ b/src/it/scala/inox/SolvingTestSuite.scala
@@ -7,14 +7,15 @@ trait SolvingTestSuite extends InoxTestSuite {
 
   override val configurations = for {
     solverName        <- Seq("nativez3", "unrollz3", "smt-z3", "smt-cvc4")
-    checkModels       <- Seq(true, false)
-    feelingLucky      <- Seq(true, false)
-    unrollAssumptions <- Seq(true, false)
+    checkModels       <- Seq(false, true)
+    feelingLucky      <- Seq(false, true)
+    unrollAssumptions <- Seq(false, true)
   } yield Seq(
     InoxOption(InoxOptions.optSelectedSolvers)(Set(solverName)),
     InoxOption(optCheckModels)(checkModels),
     InoxOption(unrolling.optFeelingLucky)(feelingLucky),
     InoxOption(unrolling.optUnrollAssumptions)(unrollAssumptions),
-    InoxOption(InoxOptions.optTimeout)(300)
+    InoxOption(InoxOptions.optTimeout)(300),
+    InoxOption(ast.optPrintUniqueIds)(true)
   )
 }
diff --git a/src/it/TestSilentReporter.scala b/src/it/scala/inox/TestSilentReporter.scala
similarity index 82%
rename from src/it/TestSilentReporter.scala
rename to src/it/scala/inox/TestSilentReporter.scala
index a42ec27a4736bcd699afdbe5a3654a519d8ef09d..178262039cd630af9a5b13dfc7adfe01ffd5c413 100644
--- a/src/it/TestSilentReporter.scala
+++ b/src/it/scala/inox/TestSilentReporter.scala
@@ -10,6 +10,10 @@ class TestSilentReporter extends DefaultReporter(Set()) {
     case Message(this.FATAL, _, msg) => lastErrors ++= List(msg.toString)
     case _ =>
   }
+
+  override def debug(pos: utils.Position, msg: => Any)(implicit section: DebugSection): Unit = {
+    println(msg)
+  }
 }
 
 class TestErrorReporter extends DefaultReporter(Set()) {
diff --git a/src/it/regression/SimpleQuantifiersSuite.scala b/src/it/scala/inox/regression/SimpleQuantifiersSuite.scala
similarity index 76%
rename from src/it/regression/SimpleQuantifiersSuite.scala
rename to src/it/scala/inox/regression/SimpleQuantifiersSuite.scala
index db43db66a36a1fc6f51b3fe37fe0f4d440bab9a8..a21b07ef51c3049f3164395c0c0b592bfcdddcee 100644
--- a/src/it/regression/SimpleQuantifiersSuite.scala
+++ b/src/it/scala/inox/regression/SimpleQuantifiersSuite.scala
@@ -11,21 +11,21 @@ class SimpleQuantifiersSuite extends SolvingTestSuite {
 
   val isAssociativeID = FreshIdentifier("isAssociative")
   val isAssociative = mkFunDef(isAssociativeID)("A") { case Seq(aT) => (
-    Seq("f" :: (T(aT, aT) =>: aT)), BooleanType, { case Seq(f) =>
+    Seq("f" :: ((aT, aT) =>: aT)), BooleanType, { case Seq(f) =>
       forall("x" :: aT, "y" :: aT, "z" :: aT)((x,y,z) => f(f(x,y),z) === f(x,f(y,z)))
     })
   }
 
   val isCommutativeID = FreshIdentifier("isCommutative")
   val isCommutative = mkFunDef(isCommutativeID)("A") { case Seq(aT) => (
-    Seq("f" :: (T(aT, aT) =>: aT)), BooleanType, { case Seq(f) =>
+    Seq("f" :: ((aT, aT) =>: aT)), BooleanType, { case Seq(f) =>
       forall("x" :: aT, "y" :: aT)((x,y) => f(x,y) === f(y,x))
     })
   }
 
   val isRotateID = FreshIdentifier("isRotate")
   val isRotate = mkFunDef(isRotateID)("A") { case Seq(aT) => (
-    Seq("f" :: (T(aT, aT) =>: aT)), BooleanType, { case Seq(f) =>
+    Seq("f" :: ((aT, aT) =>: aT)), BooleanType, { case Seq(f) =>
       forall("x" :: aT, "y" :: aT, "z" :: aT)((x,y,z) => f(f(x,y),z) === f(f(y,z),x))
     })
   }
@@ -40,60 +40,60 @@ class SimpleQuantifiersSuite extends SolvingTestSuite {
     val program = InoxProgram(ctx, symbols)
 
     val (aT,bT) = (T("A"), T("B"))
-    val Seq(f1,f2) = Seq("f1" :: (T(aT, aT) =>: aT), "f2" :: (T(bT, bT) =>: bT)).map(_.toVariable)
+    val Seq(f1,f2) = Seq("f1" :: ((aT, aT) =>: aT), "f2" :: ((bT, bT) =>: bT)).map(_.toVariable)
     val clause = isAssociative(aT)(f1) && isAssociative(bT)(f2) && !isAssociative(T(aT,bT)) {
       \("p1" :: T(aT,bT), "p2" :: T(aT, bT))((p1,p2) => E(f1(p1._1,p2._1), f2(p1._2,p2._2)))
     }
 
     val sf = SolverFactory.default(program)
     val api = SimpleSolverAPI(sf)
-    api.solveVALID(clause) should be (Some(false))
+    assert(api.solveSAT(clause).isUNSAT)
   }
 
   test("Commutative and rotate ==> associative") { ctx =>
     val program = InoxProgram(ctx, symbols)
 
     val aT = T("A")
-    val f = ("f" :: (T(aT, aT) =>: aT)).toVariable
+    val f = ("f" :: ((aT, aT) =>: aT)).toVariable
     val clause = isCommutative(aT)(f) && isRotate(aT)(f) && !isAssociative(aT)(f)
 
     val sf = SolverFactory.default(program)
     val api = SimpleSolverAPI(sf)
-    api.solveVALID(clause) should be (Some(false))
+    assert(api.solveSAT(clause).isUNSAT)
   }
 
   test("Commutative and rotate ==> associative (integer type)") { ctx =>
     val program = InoxProgram(ctx, symbols)
 
-    val f = ("f" :: (T(IntegerType, IntegerType) =>: IntegerType)).toVariable
+    val f = ("f" :: ((IntegerType, IntegerType) =>: IntegerType)).toVariable
     val clause = isCommutative(IntegerType)(f) && isRotate(IntegerType)(f) && !isAssociative(IntegerType)(f)
 
     val sf = SolverFactory.default(program)
     val api = SimpleSolverAPI(sf)
-    api.solveVALID(clause) should be (Some(false))
+    assert(api.solveSAT(clause).isUNSAT)
   }
 
   test("Associatve =!=> commutative") { ctx =>
     val program = InoxProgram(ctx, symbols)
 
     val aT = T("A")
-    val f = ("f" :: (T(aT, aT) =>: aT)).toVariable
+    val f = ("f" :: ((aT, aT) =>: aT)).toVariable
     val clause = isAssociative(aT)(f) && !isCommutative(aT)(f)
 
     val sf = SolverFactory.default(program)
     val api = SimpleSolverAPI(sf)
-    api.solveVALID(clause) should be (Some(true))
+    assert(api.solveSAT(clause).isSAT)
   }
 
   test("Commutative =!=> associative") { ctx =>
     val program = InoxProgram(ctx, symbols)
 
     val aT = T("A")
-    val f = ("f" :: (T(aT, aT) =>: aT)).toVariable
+    val f = ("f" :: ((aT, aT) =>: aT)).toVariable
     val clause = isCommutative(aT)(f) && !isAssociative(aT)(f)
 
     val sf = SolverFactory.default(program)
     val api = SimpleSolverAPI(sf)
-    api.solveVALID(clause) should be (Some(true))
+    assert(api.solveSAT(clause).isSAT)
   }
 }
diff --git a/src/it/regression/SimpleSolversSuite.scala b/src/it/scala/inox/regression/SimpleSolversSuite.scala
similarity index 100%
rename from src/it/regression/SimpleSolversSuite.scala
rename to src/it/scala/inox/regression/SimpleSolversSuite.scala
diff --git a/src/main/scala/inox/ast/CallGraph.scala b/src/main/scala/inox/ast/CallGraph.scala
index e4498f7af9d420915b0a228c12321fdde5b3ba63..ec749fcef3485f707f6e8801ae9ca9957e5cf741 100644
--- a/src/main/scala/inox/ast/CallGraph.scala
+++ b/src/main/scala/inox/ast/CallGraph.scala
@@ -19,7 +19,7 @@ trait CallGraph {
   lazy val graph: DiGraph[FunDef, SimpleEdge[FunDef]] = {
     var g = DiGraph[FunDef, SimpleEdge[FunDef]]()
 
-    for ((_, fd) <- symbols.functions; body <- fd.body; c <- collect(collectCalls(fd))(body)) {
+    for ((_, fd) <- symbols.functions; c <- collect(collectCalls(fd))(fd.fullBody)) {
       g += SimpleEdge(c._1, c._2)
     }
 
diff --git a/src/main/scala/inox/ast/DSL.scala b/src/main/scala/inox/ast/DSL.scala
index cc50665036714da651d1b8e25fec4d449164bc68..08bdff350c56aba311e404175b16b6e643584f0e 100644
--- a/src/main/scala/inox/ast/DSL.scala
+++ b/src/main/scala/inox/ast/DSL.scala
@@ -242,7 +242,7 @@ trait DSL {
     val (params, retType, bodyBuilder) = builder(tParams)
     val body = bodyBuilder(params map (_.toVariable))
 
-    new FunDef(id, tParamDefs, params, retType, Some(body), Set())
+    new FunDef(id, tParamDefs, params, retType, body, Set())
   }
 
   def mkAbstractClass(id: Identifier)
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index fda6fb737c635180f3d9e9febf0f4b45cd4a27f3..a63f639e8d41ff207129864eb9294bdeb0d70e76 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -333,12 +333,10 @@ trait Definitions { self: Trees =>
     val tparams: Seq[TypeParameterDef],
     val params: Seq[ValDef],
     val returnType: Type,
-    val body: Option[Expr],
+    val fullBody: Expr,
     val flags: Set[FunctionFlag]
   ) extends Definition {
 
-    def hasBody = body.isDefined
-
     def annotations: Set[String] = extAnnotations.keySet
     def extAnnotations: Map[String, Seq[Option[Any]]] = flags.collect {
       case Annotation(s, args) => s -> args
@@ -430,7 +428,6 @@ trait Definitions { self: Trees =>
     lazy val returnType: Type = instantiate(fd.returnType)
 
     /** The body of the respective [[FunDef]] instantiated with the real type parameters */
-    lazy val body = fd.body map instantiate
-    def hasBody   = body.isDefined
+    lazy val fullBody = instantiate(fd.fullBody)
   }
 }
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index e97cf4082924c6757e278d137942ca7533fbb1f1..bd4766373748d195660355797b85f924a0b0cb3f 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -121,13 +121,19 @@ trait Expressions { self: Trees =>
 
   /** $encodingof  `function(...)` (function invocation) */
   case class FunctionInvocation(id: Identifier, tps: Seq[Type], args: Seq[Expr]) extends Expr with CachingTyped {
-    protected def computeType(implicit s: Symbols): Type = s.lookupFunction(id) match {
-      case Some(fd) =>
-        val tfd = fd.typed(tps)
+    protected def computeType(implicit s: Symbols): Type = s.lookupFunction(id, tps) match {
+      case Some(tfd) =>
         require(args.size == tfd.params.size)
         checkParamTypes(args.map(_.getType), tfd.params.map(_.getType), tfd.returnType)
       case _ => Untyped
     }
+
+    def tfd(implicit s: Symbols): TypedFunDef = s.getFunction(id, tps)
+
+    def inlined(implicit s: Symbols): Expr = {
+      val tfd = this.tfd
+      tfd.withParamSubst(args, tfd.fullBody)
+    }
   }
 
   /** $encodingof `if(...) ... else ...` */
diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index ffc708f585ca3bab32db116003a3f64737aee34d..37152452c8616e2a47c36b0d49c12f14dddb0e5c 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/src/main/scala/inox/ast/Extractors.scala
@@ -28,16 +28,12 @@ trait TreeDeconstructor {
       (Seq(e), Seq(ct), (es, tps) => t.AsInstanceOf(es.head, tps.head.asInstanceOf[t.ClassType]))
     case s.TupleSelect(e, i) =>
       (Seq(e), Seq(), (es, tps) => t.TupleSelect(es.head, i))
-    case s.Lambda(args, body) =>
-      (
-        Seq(body), args.map(_.tpe),
-        (es, tps) => t.Lambda(args.zip(tps).map(p => t.ValDef(p._1.id, p._2)), es.head)
-      )
-    case s.Forall(args, body) =>
-      (
-        Seq(body), args.map(_.tpe),
-        (es, tps) => t.Forall(args.zip(tps).map(p => t.ValDef(p._1.id, p._2)), es.head)
-      )
+    case s.Lambda(args, body) => (
+      Seq(body), args.map(_.tpe),
+      (es, tps) => t.Lambda(args.zip(tps).map(p => t.ValDef(p._1.id, p._2)), es.head))
+    case s.Forall(args, body) => (
+      Seq(body), args.map(_.tpe),
+      (es, tps) => t.Forall(args.zip(tps).map(p => t.ValDef(p._1.id, p._2)), es.head))
     case s.Choose(res, pred) =>
       (Seq(pred), Seq(res.tpe), (es, tps) => t.Choose(t.ValDef(res.id, tps.head), es.head))
 
@@ -147,8 +143,7 @@ trait TreeDeconstructor {
     case s.Tuple(args) => (args, Seq(), (es, _) => t.Tuple(es))
     case s.IfExpr(cond, thenn, elze) => (
       Seq(cond, thenn, elze), Seq(),
-      (es, _) => t.IfExpr(es(0), es(1), es(2))
-      )
+      (es, _) => t.IfExpr(es(0), es(1), es(2)))
 
     case s.Variable(id, tp) =>
       (Seq(), Seq(tp), (_, tps) => t.Variable(id, tps.head))
@@ -176,11 +171,6 @@ trait TreeDeconstructor {
 
     case s.UnitLiteral() =>
       (Seq(), Seq(), (_, _) => t.UnitLiteral())
-
-    /* Expr's not handled here should implement this trait */
-   // case e: Extractable =>
-    //  e.extract
-
   }
 
   def deconstruct(tp: s.Type): (Seq[s.Type], Seq[t.Type] => t.Type) = tp match {
@@ -205,28 +195,52 @@ trait TreeDeconstructor {
 
   def translate(e: s.Expr): t.Expr = {
     val (es, tps, builder) = deconstruct(e)
-    builder(es map translate, tps map translate)
+
+    var changed = false
+    val newEs = for (e <- es) yield {
+      val newE = translate(e)
+      if (e ne newE) changed = true
+      newE
+    }
+
+    val newTps = for (tp <- tps) yield {
+      val newTp = translate(tp)
+      if (tp ne newTp) changed = true
+      newTp
+    }
+
+    if (changed || (s ne t)) {
+      builder(newEs, newTps).copiedFrom(e)
+    } else {
+      e.asInstanceOf[t.Expr]
+    }
   }
 
   def translate(tp: s.Type): t.Type = {
     val (tps, builder) = deconstruct(tp)
-    builder(tps map translate)
-  }
-
-}
 
-trait ExprDeconstructor extends TreeExtractor with TreeDeconstructor {
-  type Source = s.Expr
-  type Target = t.Expr
+    var changed = false
+    val newTps = for (tp <- tps) yield {
+      val newTp = translate(tp)
+      if (tp ne newTp) changed = true
+      newTp
+    }
 
-  def unapply(e: Source): Option[(Seq[Source], (Seq[Target]) => Target)] = {
-    val (es, tps, builder) = deconstruct(e)
-    Some(es, ess => builder(ess, tps map translate))
+    if (changed || (s ne t)) {
+      builder(newTps).copiedFrom(tp)
+    } else {
+      tp.asInstanceOf[t.Type]
+    }
   }
 }
 
 trait Extractors { self: Trees =>
 
+  val deconstructor: TreeDeconstructor {
+    val s: self.type
+    val t: self.type
+  }
+
   /** Operator Extractor to extract any Expression in a consistent way.
     *
     * You can match on any Leon Expr, and then get both a Seq[Expr] of
@@ -239,23 +253,18 @@ trait Extractors { self: Trees =>
     * tools for performing tree transformations that are very predictable, if
     * one need to simplify the tree, it is easy to write/call a simplification
     * function that would simply apply the corresponding constructor for each node.
-    *
-    * XXX: ideally, we would want [[Operator]] to be defined as
-    * {{{
-    *   val Operator: ExprDeconstructor {
-    *     val s: self.type
-    *     val t: self.type
-    *   }
-    * }}}
-    * however the Scala compiler seems to have some bug with this and reports
-    * wrong errors when we define it this way...
-    * @see https://issues.scala-lang.org/browse/SI-9247
     */
-  val Operator: TreeExtractor {
-    val s: self.type
-    val t: self.type
-    type Source = self.Expr
-    type Target = self.Expr
+  object Operator extends {
+    protected val s: self.type = self
+    protected val t: self.type = self
+  } with TreeExtractor {
+    type Source = Expr
+    type Target = Expr
+
+    def unapply(e: Expr): Option[(Seq[Expr], Seq[Expr] => Expr)] = {
+      val (es, tps, builder) = deconstructor.deconstruct(e)
+      Some(es, ess => builder(ess, tps))
+    }
   }
 
   object TopLevelOrs { // expr1 OR (expr2 OR (expr3 OR ..)) => List(expr1, expr2, expr3)
diff --git a/src/main/scala/inox/ast/GenTreeOps.scala b/src/main/scala/inox/ast/GenTreeOps.scala
index 6584e5a43e172e49c3e21fef82cbe246567449f3..1ff1bc8b43f93f5a9c1b4b0172566a6a862d8086 100644
--- a/src/main/scala/inox/ast/GenTreeOps.scala
+++ b/src/main/scala/inox/ast/GenTreeOps.scala
@@ -16,7 +16,7 @@ trait TreeExtractor {
 
   type Source <: s.Tree
   type Target <: t.Tree
-  def unapply(e: Source): Option[(Seq[Source], (Seq[Target]) => Target)]
+  def unapply(e: Source): Option[(Seq[Source], Seq[Target] => Target)]
 }
 
 /** Generic tree traversals based on a deconstructor of a specific tree type
@@ -388,11 +388,12 @@ trait GenTreeOps { self =>
   }
 
   object Same {
-    def unapply(tt: (Source, Target))(implicit ev1: Source =:= Target, ev2: Target =:= Source): Option[(Source, Target)] = {
+    def unapply(tt: (Source, Target))
+               (implicit ev1: Source =:= Target, ev2: Target =:= Source): Option[(Source, Target)] = {
       val Deconstructor(es1, recons1) = tt._1
       val Deconstructor(es2, recons2) = ev2(tt._2)
 
-      if (es1.size == es2.size && scala.util.Try(recons2(es1.map(ev1))).toOption == Some(tt._1)) {
+      if (es1.size == es2.size && scala.util.Try(recons2(es1.map(ev1))).toOption == Some(ev2(tt._1))) {
         Some(tt)
       } else {
         None
diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index aaec515fa045ab52cb2b6c1a7ea3a5f8a44246ed..513443fb02784554a9067a2f7b43807da5e81584 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/src/main/scala/inox/ast/Printers.scala
@@ -7,29 +7,27 @@ import utils._
 import org.apache.commons.lang3.StringEscapeUtils
 import scala.language.implicitConversions
 
-object optPrintPositions extends InoxFlagOptionDef("printPositions", "Attach positions to trees when printing", false)
-object optPrintUniqueIds extends InoxFlagOptionDef("printIds",       "Always print unique ids",                 false)
-object optPrintTypes     extends InoxFlagOptionDef("printPositions", "Attach types to trees when printing",     false)
+object optPrintPositions extends InoxFlagOptionDef("printpositions", "Attach positions to trees when printing", false)
+object optPrintUniqueIds extends InoxFlagOptionDef("printids",       "Always print unique ids",                 false)
+object optPrintTypes     extends InoxFlagOptionDef("printtypes",     "Attach types to trees when printing",     false)
 
 trait Printers {
   self: Trees =>
 
-  case class PrinterContext(
-                             current: Tree,
-                             parents: List[Tree],
-                             lvl: Int,
-                             printer: PrettyPrinter) {
+  case class PrinterContext(current: Tree,
+                            parents: List[Tree],
+                            lvl: Int,
+                            printer: PrettyPrinter) {
 
     def parent = parents.headOption
   }
 
-  case class PrinterOptions(
-                             baseIndent: Int = 0,
-                             printPositions: Boolean = false,
-                             printUniqueIds: Boolean = false,
-                             printTypes: Boolean = false,
-                             symbols: Option[Symbols] = None
-                           ) {
+  case class PrinterOptions(baseIndent: Int = 0,
+                            printPositions: Boolean = false,
+                            printUniqueIds: Boolean = false,
+                            printTypes: Boolean = false,
+                            symbols: Option[Symbols] = None) {
+
     require(
       !printTypes || symbols.isDefined,
       "Can't print types without an available symbol table"
@@ -315,11 +313,7 @@ trait Printers {
           }
 
           p"${fd.returnType} = "
-
-          fd.body match {
-            case Some(body) => p"$body"
-            case None => p"???"
-          }
+          p"${fd.fullBody}"
 
         case (tree: PrettyPrintable) => tree.printWith(ctx)
 
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index da2698aa6a7fdf602b6cf14d80b5f013e4e54185..c45a91102740ba3cd59a0468e7309da5fb7bfef7 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -184,6 +184,30 @@ trait SymbolOps { self: TypeOps =>
     (Forall(args, body), subst)
   }
 
+  /** Pre-processing for solvers that handle universal quantification
+    * in order to increase the precision of polarity analysis for
+    * quantification instantiations.
+    */
+  def simplifyQuantifications(e: Expr): Expr = {
+    val fds = functionCallsOf(e).flatMap { fi =>
+      val fd = fi.tfd.fd
+      transitiveCallees(fd) + fd
+    }
+
+    val fdsToInline = fds
+      .filterNot(fd => transitivelyCalls(fd, fd))
+      .filter(fd => exists { case _: Forall => true case _ => false }(fd.fullBody))
+    
+    def inline(e: Expr): Expr = {
+      val subst = functionCallsOf(e)
+        .filter(fi => fdsToInline(fi.tfd.fd))
+        .map(fi => fi -> fi.inlined)
+      replace(subst.toMap, e)
+    }
+
+    fixpoint(inline)(e)
+  }
+
   /** Fully expands all let expressions. */
   def expandLets(expr: Expr): Expr = {
     def rec(ex: Expr, s: Map[Variable,Expr]) : Expr = ex match {
@@ -585,16 +609,21 @@ trait SymbolOps { self: TypeOps =>
 
   /** Returns true if expr is a value. Stronger than isGround */
   def isValue(e: Expr) = isValueOfType(e, e.getType)
-  
+
   /** Returns a nested string explaining why this expression is typed the way it is.*/
-  def explainTyping(e: Expr): String = {
+  def explainTyping(e: Expr)(implicit opts: PrinterOptions): String = {
     fold[String]{ (e, se) =>
       e match {
         case FunctionInvocation(id, tps, args) =>
           val tfd = getFunction(id, tps)
-          s"$e is of type ${e.getType}" + se.map(child => "\n  " + "\n".r.replaceAllIn(child, "\n  ")).mkString + s" because ${tfd.fd.id.name} was instantiated with ${tfd.fd.tparams.zip(args).map(k => k._1 +":="+k._2).mkString(",")} with type ${tfd.fd.params.map(_.getType).mkString(",")} => ${tfd.fd.returnType}"
+          s"${e.asString} is of type ${e.getType.asString}" +
+          se.map(child => "\n  " + "\n".r.replaceAllIn(child, "\n  ")).mkString +
+          s" because ${tfd.fd.id.name} was instantiated with " +
+          s"${tfd.fd.tparams.zip(tps).map(k => k._1.asString + ":=" + k._2.asString).mkString(",")} " +
+          s"with type ${tfd.fd.params.map(_.getType.asString).mkString(",")} => ${tfd.fd.returnType.asString}"
         case e =>
-          s"$e is of type ${e.getType}" + se.map(child => "\n  " + "\n".r.replaceAllIn(child, "\n  ")).mkString
+          s"${e.asString} is of type ${e.getType.asString}" +
+          se.map(child => "\n  " + "\n".r.replaceAllIn(child, "\n  ")).mkString
       }
     }(e)
   }
@@ -606,8 +635,8 @@ trait SymbolOps { self: TypeOps =>
   // Helpers for instantiateType
   class TypeInstantiator(tps: Map[TypeParameter, Type]) extends TreeTransformer {
     override def transform(tpe: Type): Type = tpe match {
-      case tp: TypeParameter => tps.getOrElse(tp, tpe)
-      case _ => tpe
+      case tp: TypeParameter => tps.getOrElse(tp, super.transform(tpe))
+      case _ => super.transform(tpe)
     }
   }
 
diff --git a/src/main/scala/inox/ast/TreeOps.scala b/src/main/scala/inox/ast/TreeOps.scala
index 2e5a44c4df6fbd49f532dea73cf6d62692741a85..a43920d698bef423b3c821b70814d8ef3a6daeba 100644
--- a/src/main/scala/inox/ast/TreeOps.scala
+++ b/src/main/scala/inox/ast/TreeOps.scala
@@ -25,249 +25,61 @@ trait TreeOps { self: Trees =>
       }
     }
 
-    @inline
-    private def transformValDefs(vds: Seq[ValDef]): (Seq[ValDef], Boolean) = {
-      var changed = false
-      val newVds = vds.map { vd =>
-        val newVd = transform(vd)
-        if (vd ne newVd) changed = true
-        newVd
-      }
-
-      (newVds, changed)
-    }
+    def transform(e: Expr): Expr = {
+      val (es, tps, builder) = deconstructor.deconstruct(e)
 
-    @inline
-    private def transformExprs(args: Seq[Expr]): (Seq[Expr], Boolean) = {
       var changed = false
-      val newArgs = args.map { arg =>
-        val newArg = transform(arg)
-        if (arg ne newArg) changed = true
-        newArg
+      val newEs = for (e <- es) yield {
+        val newE = transform(e)
+        if (e ne newE) changed = true
+        newE
       }
 
-      (newArgs, changed)
-    }
-
-    @inline
-    private def transformTypes(tps: Seq[Type]): (Seq[Type], Boolean) = {
-      var changed = false
-      val newTps = tps.map { tp =>
+      val newTps = for (tp <- tps) yield {
         val newTp = transform(tp)
         if (tp ne newTp) changed = true
         newTp
       }
 
-      (newTps, changed)
+      if (changed) {
+        builder(newEs, newTps).copiedFrom(e)
+      } else {
+        e
+      }
     }
 
-    def transform(e: Expr): Expr = e match {
-      case v: Variable => transform(v)
-
-      case Lambda(args, body) =>
-        val (newArgs, changedArgs) = transformValDefs(args)
-        val newBody = transform(body)
-        if (changedArgs || (body ne newBody)) {
-          Lambda(newArgs, newBody).copiedFrom(e)
-        } else {
-          e
-        }
-
-      case Forall(args, body) =>
-        val (newArgs, changedArgs) = transformValDefs(args)
-        val newBody = transform(body)
-        if (changedArgs || (body ne newBody)) {
-          Forall(newArgs, newBody).copiedFrom(e)
-        } else {
-          e
-        }
-
-      case Choose(res, pred) =>
-        val newRes = transform(res)
-        val newPred = transform(pred)
-        if ((res ne newRes) || (pred ne newPred)) {
-          Choose(newRes, newPred).copiedFrom(e)
-        } else {
-          e
-        }
-
-      case Let(vd, expr, body) =>
-        val newVd = transform(vd)
-        val newExpr = transform(expr)
-        val newBody = transform(body)
-        if ((vd ne newVd) || (expr ne newExpr) || (body ne newBody)) {
-          Let(newVd, newExpr, newBody).copiedFrom(e)
-        } else {
-          e
-        }
-
-      case CaseClass(ct, args) =>
-        val newCt = transform(ct)
-        val (newArgs, changedArgs) = transformExprs(args)
-        if ((ct ne newCt) || changedArgs) {
-          CaseClass(newCt.asInstanceOf[ClassType], newArgs).copiedFrom(e)
-        } else {
-          e
-        }
-
-      case CaseClassSelector(cc, selector) =>
-        val newCc = transform(cc)
-        if (cc ne newCc) {
-          CaseClassSelector(cc, selector).copiedFrom(e)
-        } else {
-          e
-        }
-
-      case FunctionInvocation(id, tps, args) =>
-        val (newTps, changedTps) = transformTypes(tps)
-        val (newArgs, changedArgs) = transformExprs(args)
-        if (changedTps || changedArgs) {
-          FunctionInvocation(id, newTps, newArgs).copiedFrom(e)
-        } else {
-          e
-        }
-
-      case IsInstanceOf(expr, ct) =>
-        val newExpr = transform(expr)
-        val newCt = transform(ct)
-        if ((expr ne newExpr) || (ct ne newCt)) {
-          IsInstanceOf(newExpr, newCt.asInstanceOf[ClassType]).copiedFrom(e)
-        } else {
-          e
-        }
-
-      case AsInstanceOf(expr, ct) => 
-        val newExpr = transform(expr)
-        val newCt = transform(ct)
-        if ((expr ne newExpr) || (ct ne newCt)) {
-          AsInstanceOf(newExpr, newCt.asInstanceOf[ClassType]).copiedFrom(e)
-        } else {
-          e
-        }
-
-      case FiniteSet(es, tpe) =>
-        val (newArgs, changed) = transformExprs(es)
-        val newTpe = transform(tpe)
-        if (changed || (tpe ne newTpe)) {
-          FiniteSet(newArgs, newTpe).copiedFrom(e)
-        } else {
-          e
-        }
-
-      case FiniteBag(es, tpe) =>
-        var changed = false
-        val newEs = es.map { case (k, v) =>
-          val newK = transform(k)
-          if (k ne newK) changed = true
-          newK -> v
-        }
-        val newTpe = transform(tpe)
-        if (changed || (tpe ne newTpe)) {
-          FiniteBag(newEs, newTpe).copiedFrom(e)
-        } else {
-          e
-        }
-
-      case FiniteMap(pairs, from, to) =>
-        var changed = false
-        val newPairs = pairs.map { case (k, v) =>
-          val newK = transform(k)
-          val newV = transform(v)
-          if ((k ne newK) || (v ne newV)) changed = true
-          newK -> newV
-        }
-        val newFrom = transform(from)
-        val newTo = transform(to)
-        if (changed || (from ne newFrom) || (to ne newTo)) {
-          FiniteMap(newPairs, newFrom, newTo).copiedFrom(e)
-        } else {
-          e
-        }
+    def transform(t: Type): Type = {
+      val (tps, builder) = deconstructor.deconstruct(t)
 
-      case Operator(es, builder) =>
-        val newEs = es map transform
-        if ((newEs zip es).exists { case (bef, aft) => aft ne bef }) {
-          builder(newEs).copiedFrom(e)
-        } else {
-          e
-        }
-
-      case e => e
-    }
+      var changed = false
+      val newTps = for (tp <- tps) yield {
+        val newTp = transform(tp)
+        if (tp ne newTp) changed = true
+        newTp
+      }
 
-    def transform(tpe: Type): Type = tpe match {
-      case NAryType(ts, builder) =>
-        val newTs = ts map transform
-        if ((newTs zip ts).exists { case (bef, aft) => aft ne bef }) {
-          builder(ts map transform).copiedFrom(tpe)
-        } else {
-          tpe
-        }
+      if (changed) {
+        builder(newTps).copiedFrom(t)
+      } else {
+        t
+      }
     }
   }
 
   trait TreeTraverser {
-    def traverse(e: Expr): Unit = e match {
-      case Variable(_, tpe) =>
-        traverse(tpe)
-
-      case Lambda(args, body) =>
-        args foreach (vd => traverse(vd.tpe))
-        traverse(body)
-
-      case Forall(args, body) =>
-        args foreach (vd => traverse(vd.tpe))
-        traverse(body)
-
-      case Choose(res, pred) =>
-        traverse(res.tpe)
-        traverse(pred)
-
-      case Let(a, expr, body) =>
-        traverse(expr)
-        traverse(body)
-
-      case CaseClass(cct, args) =>
-        traverse(cct)
-        args foreach traverse
-
-      case CaseClassSelector(caseClass, selector) =>
-        traverse(caseClass)
-
-      case FunctionInvocation(id, tps, args) =>
-        tps foreach traverse
-        args foreach traverse
-
-      case IsInstanceOf(expr, ct) =>
-        traverse(expr)
-        traverse(ct)
-
-      case AsInstanceOf(expr, ct) => 
-        traverse(expr)
-        traverse(ct)
-
-      case FiniteSet(es, tpe) =>
-        es foreach traverse
-        traverse(tpe)
-
-      case FiniteBag(es, tpe) =>
-        es foreach { case (k, _) => traverse(k) }
-        traverse(tpe)
-
-      case FiniteMap(pairs, from, to) =>
-        pairs foreach { case (k, v) => traverse(k); traverse(v) }
-        traverse(from)
-        traverse(to)
+    def traverse(vd: ValDef): Unit = traverse(vd.tpe)
 
-      case Operator(es, builder) =>
-        es foreach traverse
+    def traverse(v: Variable): Unit = traverse(v.tpe)
 
-      case e =>
+    def traverse(e: Expr): Unit = {
+      val (es, tps, _) = deconstructor.deconstruct(e)
+      es.foreach(traverse)
+      tps.foreach(traverse)
     }
 
-    def traverse(tpe: Type): Unit = tpe match {
-      case NAryType(ts, builder) =>
-        ts foreach traverse
+    def traverse(tpe: Type): Unit = {
+      val (tps, _) = deconstructor.deconstruct(tpe)
+      tps.foreach(traverse)
     }
   }
 }
diff --git a/src/main/scala/inox/ast/Types.scala b/src/main/scala/inox/ast/Types.scala
index e1433d64218d0337c4b57610ef99ca1a8d564186..f6c59d18267d48c181ea7172d951f4d0baaecc67 100644
--- a/src/main/scala/inox/ast/Types.scala
+++ b/src/main/scala/inox/ast/Types.scala
@@ -47,7 +47,6 @@ trait Types { self: Trees =>
   case object StringType  extends Type
 
   case class BVType(size: Int) extends Type
-  //TODO: not sure about the interaction between BVType(32) and Int32Type
   object Int32Type extends BVType(32) {
     override def toString = "Int32Type"
   }
@@ -90,11 +89,16 @@ trait Types { self: Trees =>
     *
     * @see [[Extractors.Operator]] about why we can't have nice(r) things
     */
-  val NAryType: TreeExtractor {
-    val s: self.type
-    val t: self.type
-    type Source = self.Type
-    type Target = self.Type
+  object NAryType extends {
+    protected val s: self.type = self
+    protected val t: self.type = self
+  } with TreeExtractor {
+    type Source = Type
+    type Target = Type
+
+    def unapply(t: Type): Option[(Seq[Type], Seq[Type] => Type)] = {
+      Some(deconstructor.deconstruct(t))
+    }
   }
 
   object FirstOrderFunctionType {
diff --git a/src/main/scala/inox/datagen/SolverDataGen.scala b/src/main/scala/inox/datagen/SolverDataGen.scala
index 9a530c88bff663ba5ff4fe5086159db301bae540..18b8a39636525b244b75bcf945acecba9b20bcfd 100644
--- a/src/main/scala/inox/datagen/SolverDataGen.scala
+++ b/src/main/scala/inox/datagen/SolverDataGen.scala
@@ -46,7 +46,7 @@ trait SolverDataGen extends DataGenerator { self =>
               }
 
             val x = Variable(FreshIdentifier("x", true), tcd.root.toType)
-            fds +:= new FunDef(id, tparams, Seq(x.toVal), IntegerType, Some(root match {
+            fds +:= new FunDef(id, tparams, Seq(x.toVal), IntegerType, root match {
               case acd: AbstractClassDef =>
                 val (child +: rest) = acd.descendants
                 def sizeOf(ccd: CaseClassDef) = sizeOfCaseClass(ccd, x.asInstOf(typed(ccd).toType))
@@ -56,7 +56,7 @@ trait SolverDataGen extends DataGenerator { self =>
 
               case ccd: CaseClassDef =>
                 sizeOfCaseClass(ccd, x)
-            }), Set.empty)
+            }, Set.empty)
 
             id
           })
diff --git a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
index d310e98b8715c3a727774fd27e95fd190a26628b..59a0eee042710090766fcc669657f6800e04fc04 100644
--- a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
@@ -26,7 +26,7 @@ trait RecursiveEvaluator
     case v: Variable =>
       rctx.mappings.get(v.toVal) match {
         case Some(v) => v
-        case None => throw EvalError("No value for variable " + v.asString + " in mapping " + rctx.mappings)
+        case None => throw EvalError("No value for variable " + v + " in mapping " + rctx.mappings)
       }
 
     case Application(caller, args) =>
@@ -84,14 +84,7 @@ trait RecursiveEvaluator
       }
       */
 
-      val callResult: Expr = tfd.body match {
-        case Some(body) => e(body)(frame, gctx)
-        case None =>
-          // @nv TODO: this isn't right...
-          throw RuntimeError("Cannot evaluate bodyless function")
-      }
-
-      callResult
+      e(tfd.fullBody)(frame, gctx)
 
     case And(Seq(e1, e2)) =>
       (e(e1), e(e2)) match {
@@ -495,9 +488,13 @@ trait RecursiveEvaluator
       val mapping = variablesOf(l).map(v => v -> e(v)).toMap
       replaceFromSymbols(mapping, l).asInstanceOf[Lambda]
 
-    case f: Forall => onForallInvocation(f)
+    case f: Forall => onForallInvocation {
+      replaceFromSymbols(variablesOf(f).map(v => v -> e(v)).toMap, f).asInstanceOf[Forall]
+    }
 
-    case c: Choose => onChooseInvocation(c)
+    case c: Choose => onChooseInvocation {
+      replaceFromSymbols(variablesOf(c).map(v => v -> e(v)).toMap, c).asInstanceOf[Choose]
+    }
 
     case f @ FiniteMap(ss, dflt, vT) =>
       // we use toMap.toSeq to reduce dupplicate keys
diff --git a/src/main/scala/inox/evaluators/SolvingEvaluator.scala b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
index 9b17eae6bc69d5df2e30e416efba8e33e9ca5604..7e5ab5c7d0c3a4729278967b182707e38284bb1c 100644
--- a/src/main/scala/inox/evaluators/SolvingEvaluator.scala
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -48,10 +48,8 @@ trait SolvingEvaluator extends Evaluator {
   })
 
   def onForallInvocation(forall: Forall): Expr = {
-    val cache = options.findOption(optForallCache).getOrElse {
-      throw new RuntimeException("Couldn't find evaluator's forall cache")
-    }
-    
+    val cache = options.findOptionOrDefault(optForallCache)
+
     BooleanLiteral(cache.getOrElse(forall, {
       val timer = ctx.timers.evaluators.forall.start()
 
diff --git a/src/main/scala/inox/package.scala b/src/main/scala/inox/package.scala
index 6f67768b00045081c126b54ea4b6c7ca172eae55..649f8d2d1461e4e4bfad0875d34f43e3563b815d 100644
--- a/src/main/scala/inox/package.scala
+++ b/src/main/scala/inox/package.scala
@@ -43,15 +43,10 @@ package object inox {
 
   object trees extends ast.Trees {
 
-    object Operator extends {
+    object deconstructor extends {
       protected val s: trees.type = trees
       protected val t: trees.type = trees
-    } with ast.ExprDeconstructor
-
-    object NAryType extends {
-      protected val s: trees.type = trees
-      protected val t: trees.type = trees
-    } with ast.TypeDeconstructor
+    } with ast.TreeDeconstructor
 
     class Symbols(
       val functions: Map[Identifier, FunDef],
@@ -64,7 +59,7 @@ package object inox {
           fd.tparams, // type parameters can't be transformed!
           fd.params.map(vd => t.transform(vd)),
           t.transform(fd.returnType),
-          fd.body.map(t.transform),
+          t.transform(fd.fullBody),
           fd.flags)),
         classes.mapValues {
           case acd: AbstractClassDef => acd
diff --git a/src/main/scala/inox/solvers/SolverResponses.scala b/src/main/scala/inox/solvers/SolverResponses.scala
index 94f375cf69c28af14e9c5b393e7f79cfe7114bd1..5c31b4415d8ec7955bafb569e37d6ef2a120d6ee 100644
--- a/src/main/scala/inox/solvers/SolverResponses.scala
+++ b/src/main/scala/inox/solvers/SolverResponses.scala
@@ -7,10 +7,21 @@ import scala.language.higherKinds
 import scala.language.implicitConversions
 
 object SolverResponses {
-  sealed trait SolverResponse[+Model,+Assumptions]
+  sealed trait SolverResponse[+Model,+Assumptions] {
+    def isSAT: Boolean
+    def isUNSAT: Boolean
+  }
+
+  sealed trait Satisfiable {
+    def isSAT: Boolean = true
+    def isUNSAT: Boolean = false
+  }
+
+  sealed trait Unsatisfiable {
+    def isSAT: Boolean = false
+    def isUNSAT: Boolean = true
+  }
 
-  sealed trait Satisfiable
-  sealed trait Unsatisfiable
   sealed trait CheckResponse
 
   sealed trait SimpleResponse extends SolverResponse[Nothing, Nothing] with CheckResponse
@@ -37,7 +48,10 @@ object SolverResponses {
   case object Unknown extends SimpleResponse
     with ResponseWithModel[Nothing]
     with ResponseWithUnsatAssumptions[Nothing]
-    with ResponseWithModelAndAssumptions[Nothing, Nothing]
+    with ResponseWithModelAndAssumptions[Nothing, Nothing] {
+      def isSAT: Boolean = false
+      def isUNSAT: Boolean = false
+    }
 
   object Check {
     def unapply[Model,Assumptions](resp: SolverResponse[Model,Assumptions]): Option[Boolean] = resp match {
diff --git a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
index db0a91287975a3992d8d30c12548b73b0d77ae65..f739a0f4034803f9075a8d594ec90422eebb8428 100644
--- a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
@@ -29,41 +29,42 @@ trait DatatypeTemplates { self: Templates =>
     mkTemplate(tpe).instantiate(start, sym)
   }
 
-  object DatatypeTemplate {
+  private val requireChecking: MutableSet[TypedClassDef] = MutableSet.empty
+  private val requireCache: MutableMap[Type, Boolean] = MutableMap.empty
+
+  def requiresUnrolling(tpe: Type): Boolean = requireCache.get(tpe) match {
+    case Some(res) => res
+    case None =>
+      val res = tpe match {
+        case ft: FunctionType => true
+
+        case ct: ClassType => ct.tcd match {
+          case tccd: TypedCaseClassDef => tccd.parent.isDefined
+          case tcd if requireChecking(tcd.root) => false
+          case tcd =>
+            requireChecking += tcd.root
+            val classTypes = tcd.root +: (tcd.root match {
+              case (tacd: TypedAbstractClassDef) => tacd.descendants
+              case _ => Seq.empty
+            })
+
+            classTypes.exists(ct => ct.hasInvariant || (ct match {
+              case tccd: TypedCaseClassDef => tccd.fieldsTypes.exists(requiresUnrolling)
+              case _ => false
+            }))
+        }
 
-    private val requireChecking: MutableSet[TypedClassDef] = MutableSet.empty
-    private val requireCache: MutableMap[Type, Boolean] = MutableMap.empty
-
-    private def requireTypeUnrolling(tpe: Type): Boolean = requireCache.get(tpe) match {
-      case Some(res) => res
-      case None =>
-        val res = tpe match {
-          case ft: FunctionType => true
-          case ct: ClassType => ct.tcd match {
-            case tccd: TypedCaseClassDef => tccd.parent.isDefined
-            case tcd if requireChecking(tcd.root) => false
-            case tcd =>
-              requireChecking += tcd.root
-              val classTypes = tcd.root +: (tcd.root match {
-                case (tacd: TypedAbstractClassDef) => tacd.descendants
-                case _ => Seq.empty
-              })
-
-              classTypes.exists(ct => ct.hasInvariant || (ct match {
-                case tccd: TypedCaseClassDef => tccd.fieldsTypes.exists(requireTypeUnrolling)
-                case _ => false
-              }))
-          }
+        case BooleanType | UnitType | CharType | IntegerType |
+             RealType | StringType | (_: BVType) | (_: TypeParameter) => false
 
-          case BooleanType | UnitType | CharType | IntegerType |
-               RealType | StringType | (_: BVType) | (_: TypeParameter) => false
+        case NAryType(tpes, _) => tpes.exists(requiresUnrolling)
+      }
 
-          case NAryType(tpes, _) => tpes.exists(requireTypeUnrolling)
-        }
+      requireCache += tpe -> res
+      res
+  }
 
-        requireCache += tpe -> res
-        res
-    }
+  object DatatypeTemplate {
 
     def apply(tpe: Type): DatatypeTemplate = {
       val v = Variable(FreshIdentifier("x", true), tpe)
@@ -95,7 +96,7 @@ trait DatatypeTemplates { self: Templates =>
       }
 
       def rec(pathVar: Variable, expr: Expr): Unit = expr.getType match {
-        case tpe if !requireTypeUnrolling(tpe) =>
+        case tpe if !requiresUnrolling(tpe) =>
           // nothing to do here!
 
         case ct: ClassType =>
@@ -123,7 +124,7 @@ trait DatatypeTemplates { self: Templates =>
             for (tccd <- matchers) {
               val tpe = tccd.toType
 
-              if (requireTypeUnrolling(tpe)) {
+              if (requiresUnrolling(tpe)) {
                 val newBool: Variable = Variable(FreshIdentifier("b", true), BooleanType)
                 storeCond(pathVar, newBool)
 
diff --git a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
index 98f9c9be6afcb3c1f5a2d7c19db515956ea72eb7..942fa17da1e4cebf6f5d819a0e2e8e9527d27dd5 100644
--- a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
@@ -259,34 +259,38 @@ trait LambdaTemplates { self: Templates =>
     neqClauses ++ extClauses
   }
 
-  private def typeUnroller(blocker: Encoded, app: App): Clauses = typeBlockers.get(app.encoded) match {
-    case Some(typeBlocker) =>
-      Seq(mkImplies(blocker, typeBlocker))
+  private def typeUnroller(blocker: Encoded, app: App): Clauses = {
+    val App(caller, tpe @ FirstOrderFunctionType(_, to), args, value) = app
+    if (!requiresUnrolling(to)) {
+      Seq.empty
+    } else typeBlockers.get(value) match {
+      case Some(typeBlocker) =>
+        Seq(mkImplies(blocker, typeBlocker))
 
-    case None =>
-      val App(caller, tpe @ FirstOrderFunctionType(_, to), args, value) = app
-      val typeBlocker = encodeSymbol(Variable(FreshIdentifier("t"), BooleanType))
-      typeBlockers += value -> typeBlocker
+      case None =>
+        val typeBlocker = encodeSymbol(Variable(FreshIdentifier("t"), BooleanType))
+        typeBlockers += value -> typeBlocker
 
-      val clauses = registerSymbol(typeBlocker, value, to)
+        val clauses = registerSymbol(typeBlocker, value, to)
 
-      val (b, extClauses) = if (knownFree(tpe) contains caller) {
-        (blocker, Seq.empty)
-      } else {
-        val firstB = encodeSymbol(Variable(FreshIdentifier("b_free", true), BooleanType))
-        typeEnablers += firstB
+        val (b, extClauses) = if (knownFree(tpe) contains caller) {
+          (blocker, Seq.empty)
+        } else {
+          val firstB = encodeSymbol(Variable(FreshIdentifier("b_free", true), BooleanType))
+          typeEnablers += firstB
 
-        val nextB  = encodeSymbol(Variable(FreshIdentifier("b_or", true), BooleanType))
-        freeBlockers += tpe -> (freeBlockers(tpe) + (nextB -> caller))
+          val nextB  = encodeSymbol(Variable(FreshIdentifier("b_or", true), BooleanType))
+          freeBlockers += tpe -> (freeBlockers(tpe) + (nextB -> caller))
 
-        val clause = mkEquals(firstB, mkAnd(blocker, mkOr(
-          knownFree(tpe).map(idT => mkEquals(caller, idT)).toSeq ++
-          maybeFree(tpe).map { case (b, idT) => mkAnd(b, mkEquals(caller, idT)) } :+
-          nextB : _*)))
-        (firstB, Seq(clause))
-      }
+          val clause = mkEquals(firstB, mkAnd(blocker, mkOr(
+            knownFree(tpe).map(idT => mkEquals(caller, idT)).toSeq ++
+            maybeFree(tpe).map { case (b, idT) => mkAnd(b, mkEquals(caller, idT)) } :+
+            nextB : _*)))
+          (firstB, Seq(clause))
+        }
 
-      clauses ++ extClauses :+ mkImplies(b, typeBlocker)
+        clauses ++ extClauses :+ mkImplies(b, typeBlocker)
+    }
   }
 
   private def registerAppBlocker(gen: Int, key: (Encoded, App), template: Either[LambdaTemplate, Encoded], equals: Encoded, args: Seq[Arg]): Unit = {
@@ -347,28 +351,30 @@ trait LambdaTemplates { self: Templates =>
 
       if (knownFree(tpe) contains caller) {
         clauses
-      } else if (byID contains caller) {
-        // we register this app at the CURRENT generation to increase the performance
-        // of fold-style higher-order functions (the first-class function will be
-        // dispatched immediately after the fold-style function unrolling)
-        registerAppBlocker(currentGeneration, key, Left(byID(caller)), trueT, args)
-        clauses
       } else {
         val freshAppClause = if (appBlockers.isDefinedAt(key)) None else {
           val firstB = encodeSymbol(Variable(FreshIdentifier("b_lambda", true), BooleanType))
           val clause = mkImplies(mkNot(firstB), mkNot(blocker))
 
+          // blockerToApps will be updated by the following registerAppBlocker call
           appBlockers += key -> firstB
           Some(clause)
         }
 
-        lazy val gen = nextGeneration(currentGeneration)
-        for (template <- byType(tpe).values) {
-          val equals = mkEquals(template.ids._2, caller)
-          registerAppBlocker(gen, key, Left(template), equals, args)
-        }
+        if (byID contains caller) {
+          /* We register this app at the CURRENT generation to increase the performance
+           * of fold-style higher-order functions (the first-class function will be
+           * dispatched immediately after the fold-style function unrolling). */
+          registerAppBlocker(currentGeneration, key, Left(byID(caller)), trueT, args)
+        } else {
+          lazy val gen = nextGeneration(currentGeneration)
+          for (template <- byType(tpe).values) {
+            val equals = mkEquals(template.ids._2, caller)
+            registerAppBlocker(gen, key, Left(template), equals, args)
+          }
 
-        applications += tpe -> (applications(tpe) + key)
+          applications += tpe -> (applications(tpe) + key)
+        }
 
         clauses ++ freshAppClause
       }
@@ -460,6 +466,8 @@ trait LambdaTemplates { self: Templates =>
         val clause = mkEquals(appBlockers(app), extension)
 
         appBlockers += app -> nextB
+        blockerToApps -= appBlockers(app)
+        blockerToApps += nextB -> app
 
         ctx.reporter.debug(" -> extending lambda blocker: " + clause)
         newClauses += clause
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index a46423abfcedf671f6605c39b443746ee986808b..d50c5feff0e729011e162372e55ab1a02b358ef5 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -414,7 +414,7 @@ trait QuantificationTemplates { self: Templates =>
 
     private def instantiateSubsts(substs: Seq[(Set[Encoded], Map[Encoded, Arg])]): Clauses = {
       val instantiation = new scala.collection.mutable.ListBuffer[Encoded]
-      for (p @ (bs, subst) <- substs if !handledSubsts(this)(p)) {
+      for (p @ (bs, subst) <- substs if !handledSubsts.get(this).exists(_ contains p)) {
         if (subst.values.exists(_.isRight)) {
           ignoredSubsts += this -> (ignoredSubsts.getOrElse(this, Set.empty) + ((currentGeneration + 3, bs, subst)))
         } else {
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index 4c8b36e895428218f9d95db6db62c958a7f1d370..24339f73fdf43eb2c58ebe3505e6430833598053 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -40,18 +40,14 @@ trait TemplateGenerator { self: Templates =>
       return cache(tfd)
     }
 
-    val lambdaBody : Option[Expr] = tfd.body.map(simplifyHOFunctions)
+    val lambdaBody : Expr = simplifyHOFunctions(tfd.fullBody)
 
     val funDefArgs: Seq[Variable] = tfd.params.map(_.toVariable)
-    val lambdaArguments: Seq[Variable] = lambdaBody.map(lambdaArgs).toSeq.flatten
+    val lambdaArguments: Seq[Variable] = lambdaArgs(lambdaBody)
     val invocation : Expr = tfd.applied(funDefArgs)
 
-    val invocationEqualsBody : Seq[Expr] = lambdaBody match {
-      case Some(body) =>
-        liftedEquals(invocation, body, lambdaArguments) :+ Equals(invocation, body)
-      case _ =>
-        Seq.empty
-    }
+    val invocationEqualsBody : Seq[Expr] =
+      liftedEquals(invocation, lambdaBody, lambdaArguments) :+ Equals(invocation, lambdaBody)
 
     val start : Variable = Variable(FreshIdentifier("start", true), BooleanType)
     val pathVar : (Variable, Encoded) = start -> encodeSymbol(start)
@@ -174,7 +170,7 @@ trait TemplateGenerator { self: Templates =>
           implies(rec(pathVar, lhs, None), rec(pathVar, rhs, None))
         }
 
-      case a @ And(parts) if a.getType == BooleanType =>
+      case a @ And(parts) =>
         val partitions = SeqUtils.groupWhile(parts)(exprOps.isSimple)
         partitions.map(andJoin) match {
           case Seq(e) => e
@@ -203,7 +199,7 @@ trait TemplateGenerator { self: Templates =>
             newExpr
         }
 
-      case o @ Or(parts) if o.getType == BooleanType =>
+      case o @ Or(parts) =>
         val partitions = SeqUtils.groupWhile(parts)(exprOps.isSimple)
         partitions.map(orJoin) match {
           case Seq(e) => e
@@ -242,7 +238,6 @@ trait TemplateGenerator { self: Templates =>
 
           storeCond(pathVar, newBool1)
           storeCond(pathVar, newBool2)
-
           storeExpr(newExpr)
 
           val crec = rec(pathVar, cond, None)
diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala
index 2b80190248574f86db0a0c6e5450dc7e4fbec157..696b3596bb73eeeaeb30fbe3338abeb10ebd2cc0 100644
--- a/src/main/scala/inox/solvers/unrolling/Templates.scala
+++ b/src/main/scala/inox/solvers/unrolling/Templates.scala
@@ -517,8 +517,9 @@ trait Templates extends TemplateGenerator
 
     val tpeClauses = bindings.flatMap { case (v, s) => registerSymbol(encodedStart, s, v.getType) }.toSeq
 
+    val instExpr = simplifyHOFunctions(simplifyQuantifications(expr))
     val (condVars, exprVars, condTree, guardedExprs, lambdas, quants) =
-      mkClauses(start, expr, bindings + (start -> encodedStart))
+      mkClauses(start, instExpr, bindings + (start -> encodedStart), polarity = Some(true))
 
     val (clauses, calls, apps, matchers, _) = Template.encode(
       start -> encodedStart, bindings.toSeq, condVars, exprVars, guardedExprs, lambdas, quants)
@@ -526,7 +527,13 @@ trait Templates extends TemplateGenerator
     val (substMap, substClauses) = Template.substitution(
       condVars, exprVars, condTree, lambdas, quants, Map.empty, start, encodedStart)
 
-    val templateClauses = Template.instantiate(clauses, calls, apps, matchers, Map.empty)
-    tpeClauses ++ substClauses ++ templateClauses
+    val templateClauses = Template.instantiate(clauses, calls, apps, matchers, substMap)
+    val allClauses = encodedStart +: (tpeClauses ++ substClauses ++ templateClauses)
+
+    for (cl <- allClauses) {
+      ctx.reporter.debug("  . " + cl)
+    }
+
+    allClauses
   }
 }
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index fa3816fd147764c7c16ab2579ccb78c1b2cfcd21..dbe6ba29b30e75fa5a5b39e579b1299e73fd9311 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -104,7 +104,7 @@ trait AbstractUnrollingSolver
   protected def wrapModel(model: underlying.Model): ModelWrapper
 
   trait ModelWrapper {
-    def modelEval(elem: Encoded, tpe: Type): Option[Expr]
+    protected def modelEval(elem: Encoded, tpe: Type): Option[Expr]
 
     def eval(elem: Encoded, tpe: Type): Option[Expr] = modelEval(elem, theories.encode(tpe)).flatMap {
       expr => try {
@@ -114,7 +114,7 @@ trait AbstractUnrollingSolver
       }
     }
 
-    def get(v: Variable): Option[Expr] = eval(freeVars(v), theories.encode(v.getType)).filter {
+    def get(v: Variable): Option[Expr] = eval(freeVars(v), v.getType).filter {
       case v: Variable => false
       case _ => true
     }
@@ -213,7 +213,7 @@ trait AbstractUnrollingSolver
                 None
               }
             }
-          }
+          }.distinct
 
           val default = if (allImages.isEmpty) {
             def rec(e: Expr): Expr = e match {
@@ -256,7 +256,6 @@ trait AbstractUnrollingSolver
   }
 
   def checkAssumptions(config: Configuration)(assumptions: Set[Expr]): config.Response[Model, Assumptions] = {
-
     val assumptionsSeq       : Seq[Expr]          = assumptions.toSeq
     val encodedAssumptions   : Seq[Encoded]       = assumptionsSeq.map { expr =>
       val vars = exprOps.variablesOf(expr)
@@ -476,10 +475,9 @@ trait UnrollingSolver extends AbstractUnrollingSolver {
     underlying.free()
   }
 
-  val printable = (e: Expr) => e
-
-  val templates = new Templates {
+  object templates extends {
     val program: theories.targetProgram.type = theories.targetProgram
+  } with Templates {
     type Encoded = Expr
 
     def asString(expr: Expr): String = expr.asString
diff --git a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
index cda80fdbe99c30665d8c3b8ff76b7e4fafc4cf5e..08f82c01cf02e3bfcc6af1323b24a433ba6eb6f5 100644
--- a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
@@ -156,7 +156,7 @@ trait AbstractZ3Solver
 
   def declareStructuralSort(t: Type): Z3Sort = {
     adtManager.declareADTs(t, declareDatatypes)
-    sorts(bestRealType(t))
+    sorts(t)
   }
 
   def declareDatatypes(adts: Seq[(Type, DataType)]): Unit = {
diff --git a/src/main/scala/inox/transformers/Transformer.scala b/src/main/scala/inox/transformers/Transformer.scala
index d8b0c8832d83d646b3e0bfd310f7891255db72ab..36510801613d000571707f61acc5c9630fe0ac6f 100644
--- a/src/main/scala/inox/transformers/Transformer.scala
+++ b/src/main/scala/inox/transformers/Transformer.scala
@@ -29,6 +29,6 @@ trait Transformer {
   /** Transform an [[Expr]] with the initial environment */
   final def transform(e: Expr): Expr            = transform(e, initEnv)
   /** Transform the body of a [[FunDef]] */
-  final def transform(fd: FunDef): Option[Expr] = fd.body.map(transform)
+  final def transform(fd: FunDef): Expr         = transform(fd.fullBody)
 }