diff --git a/src/main/java/leon/codegen/runtime/FiniteLambda.java b/src/main/java/leon/codegen/runtime/FiniteLambda.java
index d249392384c1cf99cf6ebc5ae0677a4a41c73819..fcdb340191923fe3f408484333171c242a946196 100644
--- a/src/main/java/leon/codegen/runtime/FiniteLambda.java
+++ b/src/main/java/leon/codegen/runtime/FiniteLambda.java
@@ -5,8 +5,8 @@ package leon.codegen.runtime;
 import java.util.HashMap;
 
 public final class FiniteLambda extends Lambda {
-  final HashMap<Tuple, Object> mapping = new HashMap<Tuple, Object>();
-  private final Object dflt;
+  public final HashMap<Tuple, Object> mapping = new HashMap<Tuple, Object>();
+  public final Object dflt;
 
   public FiniteLambda(Object dflt) {
     super();
@@ -41,10 +41,4 @@ public final class FiniteLambda extends Lambda {
   public int hashCode() {
     return 63 + 11 * mapping.hashCode() + (dflt == null ? 0 : dflt.hashCode());
   }
-
-  @Override
-  public void checkForall(boolean[] quantified) {}
-
-  @Override
-  public void checkAxiom() {}
 }
diff --git a/src/main/java/leon/codegen/runtime/Forall.java b/src/main/java/leon/codegen/runtime/Forall.java
deleted file mode 100644
index f6877b604bcd069af6c2ce20d78a17d82d434dbe..0000000000000000000000000000000000000000
--- a/src/main/java/leon/codegen/runtime/Forall.java
+++ /dev/null
@@ -1,35 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.codegen.runtime;
-
-import java.util.HashMap;
-
-public abstract class Forall {
-  private static final HashMap<Tuple, Boolean> cache = new HashMap<Tuple, Boolean>();
-
-  protected final LeonCodeGenRuntimeHenkinMonitor monitor;
-  protected final Tuple closures;
-  protected final boolean check;
-
-  public Forall(LeonCodeGenRuntimeMonitor monitor, Tuple closures) throws LeonCodeGenEvaluationException {
-    if (!(monitor instanceof LeonCodeGenRuntimeHenkinMonitor))
-      throw new LeonCodeGenEvaluationException("Can't evaluate foralls without domain");
-
-    this.monitor = (LeonCodeGenRuntimeHenkinMonitor) monitor;
-    this.closures = closures;
-    this.check = (boolean) closures.get(closures.getArity() - 1);
-  }
-
-  public boolean check() {
-    Tuple key = new Tuple(new Object[] { getClass(), monitor, closures }); // check is in the closures
-    if (cache.containsKey(key)) {
-      return cache.get(key);
-    } else {
-      boolean res = checkForall();
-      cache.put(key, res);
-      return res;
-    }
-  }
-
-  public abstract boolean checkForall();
-}
diff --git a/src/main/java/leon/codegen/runtime/Lambda.java b/src/main/java/leon/codegen/runtime/Lambda.java
index af255726311655efaeddea545c5e6e44afc15b8e..a6abbef37edbe8f87f480a21a6200e32a9e0206b 100644
--- a/src/main/java/leon/codegen/runtime/Lambda.java
+++ b/src/main/java/leon/codegen/runtime/Lambda.java
@@ -4,6 +4,4 @@ package leon.codegen.runtime;
 
 public abstract class Lambda {
   public abstract Object apply(Object[] args) throws LeonCodeGenRuntimeException;
-  public abstract void checkForall(boolean[] quantified);
-  public abstract void checkAxiom();
 }
diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenQuantificationException.java b/src/main/java/leon/codegen/runtime/LeonCodeGenQuantificationException.java
deleted file mode 100644
index f172316a2548a52c6b294f70101a15ebbb8ce98a..0000000000000000000000000000000000000000
--- a/src/main/java/leon/codegen/runtime/LeonCodeGenQuantificationException.java
+++ /dev/null
@@ -1,14 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.codegen.runtime;
-
-/** Such exceptions are thrown when the evaluator encounters a forall
- *  expression whose shape is not supported in Leon. */
-public class LeonCodeGenQuantificationException extends Exception {
-  
-    private static final long serialVersionUID = -1824885321497473916L;
-
-    public LeonCodeGenQuantificationException(String msg) {
-        super(msg);
-    }
-}
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index d703c736d6c3442ae8ea23710287ba148389d876..e832dd0532601f858d6e91db97e2f8050a3aada8 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -27,9 +27,10 @@ trait CodeGeneration {
    *  isStatic signifies if the current method is static (a function, in Leon terms)
    */
   class Locals private[codegen] (
-    vars   : Map[Identifier, Int],
-    args   : Map[Identifier, Int],
-    fields : Map[Identifier, (String,String,String)]
+    vars    : Map[Identifier, Int],
+    args    : Map[Identifier, Int],
+    fields  : Map[Identifier, (String,String,String)],
+    val tps : Seq[TypeParameter]
   ) {
     /** Fetches the offset of a local variable/ parameter from its identifier */
     def varToLocal(v: Identifier): Option[Int] = vars.get(v)
@@ -39,21 +40,24 @@ trait CodeGeneration {
     def varToField(v: Identifier): Option[(String,String,String)] = fields.get(v)
 
     /** Adds some extra variables to the mapping */
-    def withVars(newVars: Map[Identifier, Int]) = new Locals(vars ++ newVars, args, fields)
+    def withVars(newVars: Map[Identifier, Int]) = new Locals(vars ++ newVars, args, fields, tps)
 
     /** Adds an extra variable to the mapping */
-    def withVar(nv: (Identifier, Int)) = new Locals(vars + nv, args, fields)
+    def withVar(nv: (Identifier, Int)) = new Locals(vars + nv, args, fields, tps)
 
-    def withArgs(newArgs: Map[Identifier, Int]) = new Locals(vars, args ++ newArgs, fields)
+    def withArgs(newArgs: Map[Identifier, Int]) = new Locals(vars, args ++ newArgs, fields, tps)
 
-    def withFields(newFields: Map[Identifier,(String,String,String)]) = new Locals(vars, args, fields ++ newFields)
+    def withFields(newFields: Map[Identifier,(String,String,String)]) = new Locals(vars, args, fields ++ newFields, tps)
 
-    override def toString = "Locals("+vars + ", " + args + ", " + fields + ")"
+    def withTypes(newTps: Seq[TypeParameter]) = new Locals(vars, args, fields, tps ++ newTps)
+
+    override def toString = "Locals("+vars + ", " + args + ", " + fields + ", " + tps + ")"
   }
 
-  object NoLocals extends Locals(Map.empty, Map.empty, Map.empty)
+  object NoLocals extends Locals(Map.empty, Map.empty, Map.empty, Seq.empty)
 
   lazy val monitorID = FreshIdentifier("__$monitor")
+  lazy val tpsID     = FreshIdentifier("__$tps")
 
   private[codegen] val ObjectClass               = "java/lang/Object"
   private[codegen] val BoxedIntClass             = "java/lang/Integer"
@@ -73,10 +77,8 @@ trait CodeGeneration {
   private[codegen] val RationalClass             = "leon/codegen/runtime/Rational"
   private[codegen] val CaseClassClass            = "leon/codegen/runtime/CaseClass"
   private[codegen] val LambdaClass               = "leon/codegen/runtime/Lambda"
-  private[codegen] val ForallClass               = "leon/codegen/runtime/Forall"
   private[codegen] val FiniteLambdaClass         = "leon/codegen/runtime/FiniteLambda"
   private[codegen] val ErrorClass                = "leon/codegen/runtime/LeonCodeGenRuntimeException"
-  private[codegen] val InvalidForallClass        = "leon/codegen/runtime/LeonCodeGenQuantificationException"
   private[codegen] val ImpossibleEvaluationClass = "leon/codegen/runtime/LeonCodeGenEvaluationException"
   private[codegen] val BadQuantificationClass    = "leon/codegen/runtime/LeonCodeGenQuantificationException"
   private[codegen] val HashingClass              = "leon/codegen/runtime/LeonCodeGenRuntimeHashing"
@@ -166,7 +168,8 @@ trait CodeGeneration {
     val cf = classes(owner)
     val (_,mn,_) = leonFunDefToJVMInfo(funDef).get
 
-    val realParams = ("L" + MonitorClass + ";") +: funDef.params.map(a => typeToJVM(a.getType))
+    val tpeParam = if (funDef.tparams.isEmpty) Seq() else Seq("[I")
+    val realParams = ("L" + MonitorClass + ";") +: (tpeParam ++ funDef.params.map(a => typeToJVM(a.getType)))
 
     val m = cf.addMethod(
       typeToJVM(funDef.returnType),
@@ -188,9 +191,12 @@ trait CodeGeneration {
 
     // An offset we introduce to the parameters:
     // 1 if this is a method, so we need "this" in position 0 of the stack
-    // 1 if we are monitoring
-    val idParams = monitorID +: funDef.paramIds
-    val newMapping = idParams.zipWithIndex.toMap.mapValues(_ + (if (!isStatic) 1 else 0))
+    // 1 the method is type parametric and we need to keep track of types
+    val receiverOffset = if (isStatic) 0 else 1
+    val paramIds = Seq(monitorID) ++ 
+      (if (funDef.tparams.nonEmpty) Seq(tpsID) else Seq.empty) ++
+      funDef.paramIds
+    val newMapping = paramIds.zipWithIndex.toMap.mapValues(_ + receiverOffset)
 
     val body = if (params.checkContracts) {
       funDef.fullBody
@@ -198,7 +204,7 @@ trait CodeGeneration {
       funDef.body.getOrElse(throw CompilationException("Can't compile a FunDef without body: "+funDef.id.name))
     }
 
-    val locals = NoLocals.withVars(newMapping)
+    val locals = NoLocals.withVars(newMapping).withTypes(funDef.tparams.map(_.tp))
 
     if (params.recordInvocations) {
       load(monitorID, ch)(locals)
@@ -218,17 +224,30 @@ trait CodeGeneration {
     ch.freeze
   }
 
+  private def typeParameters(expr: Expr): Seq[TypeParameter] = {
+    var tparams: Set[TypeParameter] = Set.empty
+    def extractParameters(tpe: TypeTree): Unit = tpe match {
+      case tp: TypeParameter => tparams += tp
+      case NAryType(tps, _) => tps.foreach(extractParameters)
+    }
+    preTraversal(e => extractParameters(e.getType))(expr)
+    tparams.toSeq.sortBy(_.id.uniqueName)
+  }
+
   private[codegen] val lambdaToClass = scala.collection.mutable.Map.empty[Lambda, String]
   private[codegen] val classToLambda = scala.collection.mutable.Map.empty[String, Lambda]
 
-  protected def compileLambda(l: Lambda): (String, Seq[(Identifier, String)], String) = {
+  protected def compileLambda(l: Lambda): (String, Seq[(Identifier, String)], Seq[TypeParameter], String) = {
     val (normalized, structSubst) = purescala.ExprOps.normalizeStructure(matchToIfThenElse(l))
     val reverseSubst = structSubst.map(p => p._2 -> p._1)
     val nl = normalized.asInstanceOf[Lambda]
 
-    val closureIDs = purescala.ExprOps.variablesOf(nl).toSeq.sortBy(_.uniqueName)
-    val closuresWithoutMonitor = closureIDs.map(id => id -> typeToJVM(id.getType))
-    val closures = (monitorID -> s"L$MonitorClass;") +: closuresWithoutMonitor
+    val tparams: Seq[TypeParameter] = typeParameters(nl)
+
+    val closedVars = purescala.ExprOps.variablesOf(nl).toSeq.sortBy(_.uniqueName)
+    val closuresWithoutMonitor = closedVars.map(id => id -> typeToJVM(id.getType))
+    val closures = (monitorID -> s"L$MonitorClass;") +:
+      ((if (tparams.nonEmpty) Seq(tpsID -> "[I") else Seq.empty) ++ closuresWithoutMonitor)
 
     val afName = lambdaToClass.getOrElse(nl, {
       val afName = "Leon$CodeGen$Lambda$" + lambdaCounter.nextGlobal
@@ -276,7 +295,7 @@ trait CodeGeneration {
 
       val argMapping = nl.args.map(_.id).zipWithIndex.toMap
       val closureMapping = closures.map { case (id, jvmt) => id -> (afName, id.uniqueName, jvmt) }.toMap
-      val newLocals = NoLocals.withArgs(argMapping).withFields(closureMapping)
+      val newLocals = NoLocals.withArgs(argMapping).withFields(closureMapping).withTypes(tparams)
 
       locally {
         val apm = cf.addMethod(s"L$ObjectClass;", "apply", s"[L$ObjectClass;")
@@ -370,396 +389,14 @@ trait CodeGeneration {
         hch.freeze
       }
 
-      locally {
-        val vmh = cf.addMethod("V", "checkForall", "[Z")
-        vmh.setFlags((
-          METHOD_ACC_PUBLIC |
-          METHOD_ACC_FINAL
-        ).asInstanceOf[U2])
-
-        val vch = vmh.codeHandler
-
-        vch << ALoad(1) // load argument array
-        def rec(args: Seq[Identifier], idx: Int, quantified: Set[Identifier]): Unit = args match {
-          case x :: xs =>
-            val notQuantLabel = vch.getFreshLabel("notQuant")
-            vch << DUP << Ldc(idx) << BALOAD << IfEq(notQuantLabel)
-            rec(xs, idx + 1, quantified + x)
-            vch << Label(notQuantLabel)
-            rec(xs, idx + 1, quantified)
-
-          case Nil =>
-            if (quantified.nonEmpty) {
-              checkQuantified(quantified, nl.body, vch)(newLocals)
-              vch << ALoad(0) << InvokeVirtual(LambdaClass, "checkAxiom", "()V")
-            }
-            vch << POP << RETURN
-        }
-
-        if (requireQuantification) {
-          rec(nl.args.map(_.id), 0, Set.empty)
-        } else {
-          vch << POP << RETURN
-        }
-
-        vch.freeze
-      }
-
-      locally {
-        val vmh = cf.addMethod("V", "checkAxiom")
-        vmh.setFlags((
-          METHOD_ACC_PUBLIC |
-          METHOD_ACC_FINAL
-        ).asInstanceOf[U2])
-
-        val vch = vmh.codeHandler
-
-        if (requireQuantification) {
-          val thisVar = FreshIdentifier("this", l.getType)
-          val axiom = Equals(Application(Variable(thisVar), nl.args.map(_.toVariable)), nl.body)
-          val axiomLocals = NoLocals.withFields(closureMapping).withVar(thisVar -> 0)
-
-          mkForall(nl.args.map(_.id).toSet, axiom, vch, check = false)(axiomLocals)
-
-          val skip = vch.getFreshLabel("skip")
-          vch << IfNe(skip)
-          vch << New(InvalidForallClass) << DUP
-          vch << Ldc("Unaxiomatic lambda " + l)
-          vch << InvokeSpecial(InvalidForallClass, constructorName, "(Ljava/lang/String;)V")
-          vch << ATHROW
-          vch << Label(skip)
-        }
-
-        vch << RETURN
-        vch.freeze
-      }
-
       loader.register(cf)
 
       afName
     })
 
     (afName, closures.map { case p @ (id, jvmt) =>
-      if (id == monitorID) p else (reverseSubst(id) -> jvmt)
-    }, "(" + closures.map(_._2).mkString("") + ")V")
-  }
-
-  private def checkQuantified(quantified: Set[Identifier], body: Expr, ch: CodeHandler)(implicit locals: Locals): Unit = {
-    val skipCheck = ch.getFreshLabel("skipCheck")
-
-    load(monitorID, ch)
-    ch << CheckCast(HenkinClass) << GetField(HenkinClass, "checkForalls", "Z")
-    ch << IfEq(skipCheck)
-
-    checkForall(quantified, body)(ctx) match {
-      case status: ForallInvalid =>
-        ch << New(InvalidForallClass) << DUP
-        ch << Ldc("Invalid forall: " + status.getMessage)
-        ch << InvokeSpecial(InvalidForallClass, constructorName, "(Ljava/lang/String;)V")
-        ch << ATHROW
-
-      case ForallValid =>
-        // expand match case expressions and lets so that caller can be compiled given
-        // the current locals (lets and matches introduce new locals)
-        val cleanBody = purescala.ExprOps.expandLets(purescala.ExprOps.matchToIfThenElse(body))
-
-        val calls = new CollectorWithPaths[(Expr, Seq[Expr], Seq[Expr])] {
-          def collect(e: Expr, path: Seq[Expr]): Option[(Expr, Seq[Expr], Seq[Expr])] = e match {
-            case QuantificationMatcher(IsTyped(caller, _: FunctionType), args) => Some((caller, args, path))
-            case _ => None
-          }
-
-          override def rec(e: Expr, path: Seq[Expr]): Expr = e match {
-            case l : Lambda => l
-            case _ => super.rec(e, path)
-          }
-        }.traverse(cleanBody)
-
-        for ((caller, args, paths) <- calls) {
-          if ((variablesOf(caller) & quantified).isEmpty) {
-            val enabler = andJoin(paths.filter(expr => (variablesOf(expr) & quantified).isEmpty))
-            val skipCall = ch.getFreshLabel("skipCall")
-            mkExpr(enabler, ch)
-            ch << IfEq(skipCall)
-
-            mkExpr(caller, ch)
-            ch << Ldc(args.size) << NewArray.primitive("T_BOOLEAN")
-            for ((arg, idx) <- args.zipWithIndex) {
-              ch << DUP << Ldc(idx) << Ldc(arg match {
-                case Variable(id) if quantified(id) => 1
-                case _ => 0
-              }) << BASTORE
-            }
-
-            ch << InvokeVirtual(LambdaClass, "checkForall", "([Z)V")
-
-            ch << Label(skipCall)
-          }
-        }
-    }
-
-    ch << Label(skipCheck)
-  }
-
-  private val typeIdCache = scala.collection.mutable.Map.empty[TypeTree, Int]
-  private[codegen] def typeId(tpe: TypeTree): Int = typeIdCache.get(tpe) match {
-    case Some(id) => id
-    case None =>
-      val id = typeIdCache.size
-      typeIdCache += tpe -> id
-      id
-  }
-
-  private[codegen] val forallToClass = scala.collection.mutable.Map.empty[Expr, String]
-
-  private def mkForall(quants: Set[Identifier], body: Expr, ch: CodeHandler, check: Boolean = true)(implicit locals: Locals): Unit = {
-    val (afName, closures, consSig) = compileForall(quants, body)
-    ch << New(afName) << DUP
-    load(monitorID, ch)
-    mkTuple(closures.map(_.toVariable) :+ BooleanLiteral(check), ch)
-    ch << InvokeSpecial(afName, constructorName, consSig)
-    ch << InvokeVirtual(ForallClass, "check", "()Z")
-  }
-
-  private def compileForall(quants: Set[Identifier], body: Expr): (String, Seq[Identifier], String) = {
-    val (nl, structSubst) = purescala.ExprOps.normalizeStructure(matchToIfThenElse(body))
-    val reverseSubst = structSubst.map(p => p._2 -> p._1)
-    val nquants = quants.flatMap(structSubst.get)
-
-    val closures = (purescala.ExprOps.variablesOf(nl) -- nquants).toSeq.sortBy(_.uniqueName)
-
-    val afName = forallToClass.getOrElse(nl, {
-      val afName = "Leon$CodeGen$Forall$" + forallCounter.nextGlobal
-      forallToClass += nl -> afName
-
-      val cf = new ClassFile(afName, Some(ForallClass))
-
-      cf.setFlags((
-        CLASS_ACC_SUPER |
-        CLASS_ACC_PUBLIC |
-        CLASS_ACC_FINAL
-      ).asInstanceOf[U2])
-
-      locally {
-        val cch = cf.addConstructor(s"L$MonitorClass;", s"L$TupleClass;").codeHandler
-
-        cch << ALoad(0) << ALoad(1) << ALoad(2)
-        cch << InvokeSpecial(ForallClass, constructorName, s"(L$MonitorClass;L$TupleClass;)V")
-        cch << RETURN
-        cch.freeze
-      }
-
-      locally {
-        val cfm = cf.addMethod("Z", "checkForall")
-
-        cfm.setFlags((
-          METHOD_ACC_PUBLIC |
-          METHOD_ACC_FINAL
-        ).asInstanceOf[U2])
-
-        val cfch = cfm.codeHandler
-
-        cfch << ALoad(0) << GetField(ForallClass, "closures", s"L$TupleClass;")
-
-        val closureVars = (for ((id, idx) <- closures.zipWithIndex) yield {
-          val slot = cfch.getFreshVar
-          cfch << DUP << Ldc(idx) << InvokeVirtual(TupleClass, "get", s"(I)L$ObjectClass;")
-          mkUnbox(id.getType, cfch)
-          cfch << (id.getType match {
-            case ValueType() => IStore(slot)
-            case _ => AStore(slot)
-          })
-          id -> slot
-        }).toMap
-
-        cfch << POP
-
-        val monitorSlot = cfch.getFreshVar
-        cfch << ALoad(0) << GetField(ForallClass, "monitor", s"L$HenkinClass;")
-        cfch << AStore(monitorSlot)
-
-        implicit val locals = NoLocals.withVars(closureVars).withVar(monitorID -> monitorSlot)
-
-        val skipCheck = cfch.getFreshLabel("skipCheck")
-        cfch << ALoad(0) << GetField(ForallClass, "check", "Z")
-        cfch << IfEq(skipCheck)
-        checkQuantified(nquants, nl, cfch)
-        cfch << Label(skipCheck)
-
-        val TopLevelAnds(conjuncts) = nl
-        val endLabel = cfch.getFreshLabel("forallEnd")
-
-        for (conj <- conjuncts) {
-          val vars = purescala.ExprOps.variablesOf(conj)
-          val quantified = nquants.filter(vars)
-
-          val matchQuorums = extractQuorums(conj, quantified)
-
-          var allSlots: List[Int] = Nil
-          var freeSlots: List[Int] = Nil
-          def getSlot(): Int = freeSlots match {
-            case x :: xs =>
-              freeSlots = xs
-              x
-            case Nil =>
-              val slot = cfch.getFreshVar
-              allSlots = allSlots :+ slot
-              slot
-          }
-
-          for ((qrm, others) <- matchQuorums) {
-            val quorum = qrm.toList
-
-            def rec(mis: List[(Expr, Expr, Seq[Expr], Int)], locs: Map[Identifier, Int], pointers: Map[(Int, Int), Identifier]): Unit = mis match {
-              case (TopLevelAnds(paths), expr, args, qidx) :: rest =>
-                load(monitorID, cfch)
-                cfch << CheckCast(HenkinClass)
-
-                mkExpr(expr, cfch)
-                cfch << Ldc(typeId(expr.getType))
-                cfch << InvokeVirtual(HenkinClass, "domain", s"(L$ObjectClass;I)L$JavaListClass;")
-                cfch << InvokeInterface(JavaListClass, "iterator", s"()L$JavaIteratorClass;")
-
-                val loop = cfch.getFreshLabel("loop")
-                val out = cfch.getFreshLabel("out")
-                cfch << Label(loop)
-                // it
-                cfch << DUP
-                // it, it
-                cfch << InvokeInterface(JavaIteratorClass, "hasNext", "()Z")
-                // it, hasNext
-                cfch << IfEq(out) << DUP
-                // it, it
-                cfch << InvokeInterface(JavaIteratorClass, "next", s"()L$ObjectClass;")
-                // it, elem
-                cfch << CheckCast(TupleClass)
-
-                val (newLoc, newPtr) = (for ((arg, aidx) <- args.zipWithIndex) yield {
-                  val id = FreshIdentifier("q", arg.getType, true)
-                  val slot = getSlot()
-
-                  cfch << DUP << Ldc(aidx) << InvokeVirtual(TupleClass, "get", s"(I)L$ObjectClass;")
-                  mkUnbox(arg.getType, cfch)
-                  cfch << (typeToJVM(arg.getType) match {
-                    case "I" | "Z" => IStore(slot)
-                    case _ => AStore(slot)
-                  })
-
-                  (id -> slot, (qidx -> aidx) -> id)
-                }).unzip
-
-                cfch << POP
-                // it
-
-                rec(rest, locs ++ newLoc, pointers ++ newPtr)
-
-                cfch << Goto(loop)
-                cfch << Label(out) << POP
-
-              case Nil =>
-                val okLabel = cfch.getFreshLabel("assignmentOk")
-
-                var mappings: Seq[(Identifier, Int, Int)] = Seq.empty
-                var constraints: Seq[(Expr, Int, Int)] = Seq.empty
-                var equalities: Seq[((Int, Int), (Int, Int))] = Seq.empty
-
-                for ((q @ (_, expr, args), qidx) <- quorum.zipWithIndex) {
-                  val (qmappings, qconstraints) = args.zipWithIndex.partition {
-                    case (Variable(id), aidx) => quantified(id)
-                    case _ => false
-                  }
-
-                  mappings ++= qmappings.map(p => (p._1.asInstanceOf[Variable].id, qidx, p._2))
-                  constraints ++= qconstraints.map(p => (p._1, qidx, p._2))
-                }
-
-                val mapping = for ((id, es) <- mappings.groupBy(_._1)) yield {
-                  val base :: others = es.toList.map(p => (p._2, p._3))
-                  equalities ++= others.map(p => base -> p)
-                  (id -> base)
-                }
-
-                val enabler = andJoin(constraints.map {
-                  case (e, qidx, aidx) => Equals(e, pointers(qidx -> aidx).toVariable)
-                } ++ equalities.map {
-                  case (k1, k2) => Equals(pointers(k1).toVariable, pointers(k2).toVariable)
-                })
-
-                val varsMap = quantified.map(id => id -> locs(pointers(mapping(id)))).toMap
-                val varLocals = locals.withVars(varsMap)
-
-                mkExpr(enabler, cfch)(varLocals.withVars(locs))
-                cfch << IfEq(okLabel)
-
-                val checkOk = cfch.getFreshLabel("checkOk")
-                load(monitorID, cfch)
-                cfch << GetField(HenkinClass, "checkForalls", "Z")
-                cfch << IfEq(checkOk)
-
-                var nextLabel: Option[String] = None
-                for ((b,caller,args) <- others) {
-                  nextLabel.foreach(label => cfch << Label(label))
-                  nextLabel = Some(cfch.getFreshLabel("next"))
-
-                  mkExpr(b, cfch)(varLocals)
-                  cfch << IfEq(nextLabel.get)
-
-                  load(monitorID, cfch)
-                  cfch << CheckCast(HenkinClass)
-                  mkExpr(caller, cfch)(varLocals)
-                  cfch << Ldc(typeId(caller.getType))
-                  cfch << InvokeVirtual(HenkinClass, "domain", s"(L$ObjectClass;I)L$JavaListClass;")
-                  mkTuple(args, cfch)(varLocals)
-                  cfch << InvokeInterface(JavaListClass, "contains", s"(L$ObjectClass;)Z")
-                  cfch << IfNe(nextLabel.get)
-
-                  cfch << New(InvalidForallClass) << DUP
-                  cfch << Ldc("Unhandled transitive implication in " + conj)
-                  cfch << InvokeSpecial(InvalidForallClass, constructorName, "(Ljava/lang/String;)V")
-                  cfch << ATHROW
-                }
-                nextLabel.foreach(label => cfch << Label(label))
-
-                cfch << Label(checkOk)
-                mkExpr(conj, cfch)(varLocals)
-                cfch << IfNe(okLabel)
-
-                // -- Forall is false! --
-                // POP all the iterators...
-                for (_ <- List.range(0, quorum.size)) cfch << POP
-
-                // ... and return false
-                cfch << Ldc(0) << Goto(endLabel)
-                cfch << Label(okLabel)
-            }
-
-            val skipQuorum = cfch.getFreshLabel("skipQuorum")
-            for ((TopLevelAnds(paths), _, _) <- quorum) {
-              val p = andJoin(paths.filter(path => (variablesOf(path) & quantified).isEmpty))
-              mkExpr(p, cfch)
-              cfch << IfEq(skipQuorum)
-            }
-
-            val mis = quorum.zipWithIndex.map { case ((p, e, as), idx) => (p, e, as, idx) }
-            rec(mis, Map.empty, Map.empty)
-            freeSlots = allSlots
-
-            cfch << Label(skipQuorum)
-          }
-        }
-
-        cfch << Ldc(1) << Label(endLabel)
-        cfch << IRETURN
-
-        cfch.freeze
-      }
-
-      loader.register(cf)
-
-      afName
-    })
-
-    (afName, closures.map(reverseSubst), s"(L$MonitorClass;L$TupleClass;)V")
+      if (id == monitorID || id == tpsID) p else (reverseSubst(id) -> jvmt)
+    }, tparams, "(" + closures.map(_._2).mkString("") + ")V")
   }
 
   // also makes tuples with 0/1 args
@@ -776,6 +413,31 @@ trait CodeGeneration {
     ch << InvokeSpecial(TupleClass, constructorName, s"([L$ObjectClass;)V")
   }
 
+  private def loadTypes(tps: Seq[TypeTree], ch: CodeHandler)(implicit locals: Locals): Unit = {
+    if (tps.nonEmpty) {
+      ch << Ldc(tps.size)
+      ch << NewArray.primitive("T_INT")
+      for ((tpe,idx) <- tps.zipWithIndex) {
+        ch << DUP << Ldc(idx) << Ldc(registerType(tpe)) << IASTORE
+      }
+
+      if (locals.tps.nonEmpty) {
+        load(monitorID, ch)
+        ch << SWAP
+
+        ch << Ldc(locals.tps.size)
+        ch << NewArray.primitive("T_INT")
+        for ((tpe,idx) <- locals.tps.zipWithIndex) {
+          ch << DUP << Ldc(idx) << Ldc(registerType(tpe)) << IASTORE
+        }
+
+        ch << SWAP
+        load(tpsID, ch)
+        ch << InvokeVirtual(MonitorClass, "typeParams", s"([I[I[I)[I")
+      }
+    }
+  }
+
   private[codegen] def mkExpr(e: Expr, ch: CodeHandler, canDelegateToMkBranch: Boolean = true)(implicit locals: Locals) {
     e match {
       case Variable(id) =>
@@ -1042,11 +704,10 @@ trait CodeGeneration {
           ch << AASTORE
         }
 
-        ch << InvokeVirtual(MonitorClass, "onAbstractInvocation", s"(I[L$ObjectClass;)L$ObjectClass;")
+        ch << InvokeVirtual(MonitorClass, "onAbstractInvocation", s"(I[I[L$ObjectClass;)L$ObjectClass;")
 
         mkUnbox(tfd.returnType, ch)
 
-
       // Static lazy fields/ functions
       case fi @ FunctionInvocation(tfd, as) =>
         val (cn, mn, ms) = leonFunDefToJVMInfo(tfd.fd).getOrElse {
@@ -1054,6 +715,7 @@ trait CodeGeneration {
         }
 
         load(monitorID, ch)
+        loadTypes(tfd.tps, ch)
 
         for((a, vd) <- as zip tfd.fd.params) {
           vd.getType match {
@@ -1102,6 +764,7 @@ trait CodeGeneration {
         mkExpr(rec, ch)
 
         load(monitorID, ch)
+        loadTypes(tfd.tps, ch)
 
         for((a, vd) <- as zip tfd.fd.params) {
           vd.getType match {
@@ -1146,21 +809,18 @@ trait CodeGeneration {
         }
 
       case l @ Lambda(args, body) =>
-        val (afName, closures, consSig) = compileLambda(l)
+        val (afName, closures, tparams, consSig) = compileLambda(l)
 
         ch << New(afName) << DUP
         for ((id,jvmt) <- closures) {
-          if (id == monitorID) {
-            load(monitorID, ch)
+          if (id == tpsID) {
+            loadTypes(tparams, ch)
           } else {
             mkExpr(Variable(id), ch)
           }
         }
         ch << InvokeSpecial(afName, constructorName, consSig)
 
-      case f @ Forall(args, body) =>
-        mkForall(args.map(_.id).toSet, body, ch)
-
       // String processing =>
       case StringConcat(l, r) =>
         mkExpr(l, ch)
@@ -1403,15 +1063,42 @@ trait CodeGeneration {
         ch << ATHROW
 
       case forall @ Forall(fargs, body) =>
+        val id = registerForall(forall, locals.tps)
+        val args = variablesOf(forall).toSeq.sortBy(_.uniqueName)
+
+        load(monitorID, ch)
+        ch << Ldc(id)
+        if (locals.tps.nonEmpty) {
+          load(tpsID, ch)
+        } else {
+          ch << Ldc(0) << NewArray.primitive("T_INT")
+        }
+
+        ch << Ldc(args.size)
+        ch << NewArray(ObjectClass)
+
+        for ((id, i) <- args.zipWithIndex) {
+          ch << DUP
+          ch << Ldc(i)
+          mkExpr(Variable(id), ch)
+          mkBox(id.getType, ch)
+          ch << AASTORE
+        }
+
+        ch << InvokeVirtual(MonitorClass, "onForallInvocation", s"(I[I[L$ObjectClass;)Z")
 
       case choose: Choose =>
         val prob = synthesis.Problem.fromSpec(choose.pred)
 
-        val id = registerProblem(prob)
+        val id = registerProblem(prob, locals.tps)
 
         load(monitorID, ch)
-
         ch << Ldc(id)
+        if (locals.tps.nonEmpty) {
+          load(tpsID, ch)
+        } else {
+          ch << Ldc(0) << NewArray.primitive("T_INT")
+        }
 
         ch << Ldc(prob.as.size)
         ch << NewArray(ObjectClass)
@@ -1424,7 +1111,7 @@ trait CodeGeneration {
           ch << AASTORE
         }
 
-        ch << InvokeVirtual(MonitorClass, "onChooseInvocation", s"(I[L$ObjectClass;)L$ObjectClass;")
+        ch << InvokeVirtual(MonitorClass, "onChooseInvocation", s"(I[I[L$ObjectClass;)L$ObjectClass;")
 
         mkUnbox(choose.getType, ch)
 
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 6af6aa9e50686244581de931f793f00c34c94ed9..ff3c4af1039cf682fe41f3be62eee97e441cf474 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -44,11 +44,30 @@ class CompilationUnit(val ctx: LeonContext,
 
   val runtimeCounter = new UniqueCounter[Unit]
 
-  var runtimeProblemMap  = Map[Int, Problem]()
+  var runtimeTypeToIdMap = Map[TypeTree, Int]()
+  var runtimeIdToTypeMap = Map[Int, TypeTree]()
+  def registerType(tpe: TypeTree): Int = runtimeTypeToIdMap.get(tpe) match {
+    case Some(id) => id
+    case None =>
+      val id = runtimeCounter.nextGlobal
+      runtimeTypeToIdMap += tpe -> id
+      runtimeIdToTypeMap += id -> tpe
+      id
+  }
+
+  var runtimeProblemMap  = Map[Int, (Seq[TypeParameter], Problem)]()
 
-  def registerProblem(p: Problem): Int = {
+  def registerProblem(p: Problem, tps: Seq[TypeParameter]): Int = {
     val id = runtimeCounter.nextGlobal
-    runtimeProblemMap += id -> p
+    runtimeProblemMap += id -> (tps, p)
+    id
+  }
+
+  var runtimeForallMap = Map[Int, (Seq[TypeParameter], Forall)]()
+
+  def registerForall(f: Forall, tps: Seq[TypeParameter]): Int = {
+    val id = runtimeCounter.nextGlobal
+    runtimeForallMap += id -> (tps, f)
     id
   }
 
@@ -103,7 +122,9 @@ class CompilationUnit(val ctx: LeonContext,
    */
   def leonFunDefToJVMInfo(fd: FunDef): Option[(String, String, String)] = {
     funDefInfo.get(fd).orElse {
-      val sig = "(L"+MonitorClass+";" + fd.params.map(a => typeToJVM(a.getType)).mkString("") + ")" + typeToJVM(fd.returnType)
+      val sig = "(L"+MonitorClass+";" +
+        (if (fd.tparams.nonEmpty) "[I" else "") +
+        fd.params.map(a => typeToJVM(a.getType)).mkString("") + ")" + typeToJVM(fd.returnType)
 
       defToModuleOrClass.get(fd).flatMap(m => classes.get(m)) match {
         case Some(cf) =>
@@ -144,36 +165,15 @@ class CompilationUnit(val ctx: LeonContext,
     conss.last
   }
 
-  def getMonitor(model: solvers.Model, maxInvocations: Int, check: Boolean): Monitor = {
+  def getMonitor(model: solvers.Model, maxInvocations: Int): Monitor = {
     val bodies = model.toSeq.filter { case (id, v) => abstractFunDefs(id) }.toMap
+    val domains = model match {
+      case hm: solvers.HenkinModel => Some(hm.doms)
+      case _ => None
+    }
 
-    new StdMonitor(this, maxInvocations, bodies)
+    new StdMonitor(this, maxInvocations, bodies, domains)
   }
-  //  model match {
-  //  case hModel: solvers.HenkinModel =>
-  //    val lhm = new LeonCodeGenRuntimeHenkinMonitor(maxInvocations, check)
-  //    for ((lambda, domain) <- hModel.doms.lambdas) {
-  //      val (afName, _, _) = compileLambda(lambda)
-  //      val lc = loader.loadClass(afName)
-
-  //      for (args <- domain) {
-  //        // note here that it doesn't matter that `lhm` doesn't yet have its domains
-  //        // filled since all values in `args` should be grounded
-  //        val inputJvm = tupleConstructor.newInstance(args.map(valueToJVM(_)(lhm)).toArray).asInstanceOf[leon.codegen.runtime.Tuple]
-  //        lhm.add(lc, inputJvm)
-  //      }
-  //    }
-
-  //    for ((tpe, domain) <- hModel.doms.tpes; args <- domain) {
-  //      val tpeId = typeId(tpe)
-  //      // same remark as above about valueToJVM(_)(lhm)
-  //      val inputJvm = tupleConstructor.newInstance(args.map(valueToJVM(_)(lhm)).toArray).asInstanceOf[leon.codegen.runtime.Tuple]
-  //      lhm.add(tpeId, inputJvm)
-  //    }
-  //    lhm
-  //  case _ =>
-  //    new LeonCodeGenRuntimeMonitor(maxInvocations)
-  //}
 
   /** Translates Leon values (not generic expressions) to JVM compatible objects.
     *
@@ -238,7 +238,7 @@ class CompilationUnit(val ctx: LeonContext,
       m
 
     case f @ FiniteLambda(mapping, dflt, _) =>
-      val l = new leon.codegen.runtime.FiniteLambda(dflt)
+      val l = new leon.codegen.runtime.FiniteLambda(valueToJVM(dflt))
 
       for ((ks,v) <- mapping) {
         // Force tuple even with 1/0 elems.
@@ -354,6 +354,15 @@ class CompilationUnit(val ctx: LeonContext,
       }.toMap
       FiniteMap(pairs, from, to)
 
+    case (lambda: runtime.FiniteLambda, ft @ FunctionType(from, to)) =>
+      val mapping = lambda.mapping.asScala.map { entry =>
+        val k = jvmToValue(entry._1, tupleTypeWrap(from))
+        val v = jvmToValue(entry._2, to)
+        unwrapTuple(k, from.size) -> v
+      }
+      val dflt = jvmToValue(lambda.dflt, to)
+      FiniteLambda(mapping.toSeq, dflt, ft)
+
     case (lambda: runtime.Lambda, _: FunctionType) =>
       val cls = lambda.getClass
 
diff --git a/src/main/scala/leon/codegen/CompiledExpression.scala b/src/main/scala/leon/codegen/CompiledExpression.scala
index 8ce2cb269546ef69f6edb1eefecd0d53123fd15b..6467a2068cf56227f26d01df6bec2287d515d48d 100644
--- a/src/main/scala/leon/codegen/CompiledExpression.scala
+++ b/src/main/scala/leon/codegen/CompiledExpression.scala
@@ -43,9 +43,9 @@ class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression: Expr,
     }
   }
 
-  def eval(model: solvers.Model, check: Boolean = false) : Expr = {
+  def eval(model: solvers.Model) : Expr = {
     try {
-      val monitor = unit.getMonitor(model, params.maxFunctionInvocations, check)
+      val monitor = unit.getMonitor(model, params.maxFunctionInvocations)
 
       evalFromJVM(argsToJVM(argsDecl.map(model), monitor), monitor)
     } catch {
diff --git a/src/main/scala/leon/codegen/runtime/Monitor.scala b/src/main/scala/leon/codegen/runtime/Monitor.scala
index a4fcbe8158d2b727a865969f36f19194fdfef56b..ac88c35be2cecc8bec3451354d79bdefb382a4e5 100644
--- a/src/main/scala/leon/codegen/runtime/Monitor.scala
+++ b/src/main/scala/leon/codegen/runtime/Monitor.scala
@@ -6,8 +6,12 @@ package codegen.runtime
 import utils._
 import purescala.Expressions._
 import purescala.Constructors._
+import purescala.Definitions._
 import purescala.Common._
-import purescala.ExprOps.valuateWithModel
+import purescala.Types._
+import purescala.TypeOps._
+import purescala.ExprOps.{valuateWithModel, replaceFromIDs, variablesOf}
+import purescala.Quantification.{extractQuorums, HenkinDomains}
 
 import codegen.CompilationUnit
 
@@ -17,30 +21,41 @@ import scala.concurrent.duration._
 
 import solvers.SolverFactory
 
-
 import synthesis._
 
 abstract class Monitor {
   def onInvocation(): Unit
 
-  def onAbstractInvocation(id: Int, args: Array[AnyRef]): AnyRef
+  def typeParams(params: Array[Int], tps: Array[Int], newTps: Array[Int]): Array[Int]
+
+  def onAbstractInvocation(id: Int, tps: Array[Int], args: Array[AnyRef]): AnyRef
+
+  def onChooseInvocation(id: Int, tps: Array[Int], args: Array[AnyRef]): AnyRef
 
-  def onChooseInvocation(id: Int, args: Array[AnyRef]): AnyRef
+  def onForallInvocation(id: Int, tps: Array[Int], args: Array[AnyRef]): Boolean
 }
 
 class NoMonitor extends Monitor {
   def onInvocation(): Unit = {}
 
-  def onAbstractInvocation(id: Int, args: Array[AnyRef]): AnyRef = {
-    throw new LeonCodeGenEvaluationException("No monitor available.");
+  def typeParams(params: Array[Int], tps: Array[Int], newTps: Array[Int]): Array[Int] = {
+    throw new LeonCodeGenEvaluationException("No monitor available.")
   }
 
-  def onChooseInvocation(id: Int, args: Array[AnyRef]): AnyRef = {
-    throw new LeonCodeGenEvaluationException("No monitor available.");
+  def onAbstractInvocation(id: Int, tps: Array[Int], args: Array[AnyRef]): AnyRef = {
+    throw new LeonCodeGenEvaluationException("No monitor available.")
+  }
+
+  def onChooseInvocation(id: Int, tps: Array[Int], args: Array[AnyRef]): AnyRef = {
+    throw new LeonCodeGenEvaluationException("No monitor available.")
+  }
+
+  def onForallInvocation(id: Int, tps: Array[Int], args: Array[AnyRef]): Boolean = {
+    throw new LeonCodeGenEvaluationException("No monitor available.")
   }
 }
 
-class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Identifier, Expr]) extends Monitor {
+class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Identifier, Expr], domains: Option[HenkinDomains] = None) extends Monitor {
 
   private[this] var invocations = 0
 
@@ -54,9 +69,19 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
     }
   }
 
-  def onAbstractInvocation(id: Int, args: Array[AnyRef]): AnyRef = {
+  def typeParams(params: Array[Int], tps: Array[Int], newTps: Array[Int]): Array[Int] = {
+    val tparams = params.toSeq.map(unit.runtimeIdToTypeMap(_).asInstanceOf[TypeParameter])
+    val static = tps.toSeq.map(unit.runtimeIdToTypeMap(_))
+    val newTypes = newTps.toSeq.map(unit.runtimeIdToTypeMap(_))
+    val tpMap = (tparams.map(TypeParameterDef(_)) zip newTypes).toMap
+    static.map(tpe => unit.registerType(instantiateType(tpe, tpMap))).toArray
+  }
+
+  def onAbstractInvocation(id: Int, tps: Array[Int], args: Array[AnyRef]): AnyRef = {
     val fd = unit.runtimeAbstractMap(id)
 
+    // TODO: extract types too!
+
     bodies.get(fd.id) match {
       case Some(expr) =>
         throw new LeonCodeGenRuntimeException("Found body!")
@@ -66,14 +91,12 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
     }
   }
 
+  private[this] val chooseCache = new MutableMap[(Int, Seq[AnyRef]), AnyRef]()
 
-  private[this] val cache   = new MutableMap[(Int, Seq[AnyRef]), AnyRef]()
-
-  def onChooseInvocation(id: Int, inputs: Array[AnyRef]): AnyRef = {
-
+  def onChooseInvocation(id: Int, tps: Array[Int], inputs: Array[AnyRef]): AnyRef = {
     implicit val debugSection = DebugSectionSynthesis
 
-    val p = unit.runtimeProblemMap(id)
+    val (tparams, p) = unit.runtimeProblemMap(id)
 
     val program = unit.program
     val ctx     = unit.ctx
@@ -81,20 +104,27 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
     ctx.reporter.debug("Executing choose (codegen)!")
     val is = inputs.toSeq
 
-    if (cache contains ((id, is))) {
-      cache((id, is))
+    if (chooseCache contains ((id, is))) {
+      chooseCache((id, is))
     } else {
       val tStart = System.currentTimeMillis
 
       val solverf = SolverFactory.default(ctx, program).withTimeout(10.second)
       val solver = solverf.getNewSolver()
 
-      val inputsMap = (p.as zip inputs).map {
-        case (id, v) =>
-          Equals(Variable(id), unit.jvmToValue(v, id.getType))
+      val newTypes = tps.toSeq.map(unit.runtimeIdToTypeMap(_))
+      val tpMap = (tparams.map(TypeParameterDef(_)) zip newTypes).toMap
+
+      val vars = (variablesOf(p.pc) ++ variablesOf(p.phi)).toSeq.sortBy(_.uniqueName)
+      val newVars = vars.map(id => FreshIdentifier(id.name, instantiateType(id.getType, tpMap), true))
+
+      val args = p.as.map(id => FreshIdentifier(id.name, instantiateType(id.getType, tpMap), true))
+      val inputsMap = (args zip inputs).map {
+        case (id, v) => Equals(Variable(id), unit.jvmToValue(v, id.getType))
       }
 
-      solver.assertCnstr(andJoin(Seq(p.pc, p.phi) ++ inputsMap))
+      val expr = instantiateType(and(p.pc, p.phi), tpMap, (vars zip newVars).toMap)
+      solver.assertCnstr(andJoin(expr +: inputsMap))
 
       try {
         solver.check match {
@@ -112,7 +142,7 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
             ctx.reporter.debug("Finished synthesis with "+leonRes.asString(ctx))
 
             val obj = unit.valueToJVM(leonRes)(this)
-            cache += (id, is) -> obj
+            chooseCache += (id, is) -> obj
             obj
           case Some(false) =>
             throw new LeonCodeGenRuntimeException("Constraint is UNSAT")
@@ -126,6 +156,86 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
     }
   }
 
+  private[this] val forallCache = new MutableMap[(Int, Seq[AnyRef]), Boolean]()
+
+  def onForallInvocation(id: Int, tps: Array[Int], args: Array[AnyRef]): Boolean = {
+    implicit val debugSection = DebugSectionVerification
+
+    val (tparams, f) = unit.runtimeForallMap(id)
+
+    val program = unit.program
+    val ctx     = unit.ctx
+
+    ctx.reporter.debug("Executing forall (codegen)!")
+    val argsSeq = args.toSeq
+
+    if (forallCache contains ((id, argsSeq))) {
+      forallCache((id, argsSeq))
+    } else {
+      val tStart = System.currentTimeMillis
+
+      val solverf = SolverFactory.default(ctx, program).withTimeout(1.second)
+      val solver = solverf.getNewSolver()
+
+      val newTypes = tps.toSeq.map(unit.runtimeIdToTypeMap(_))
+      val tpMap = (tparams.map(TypeParameterDef(_)) zip newTypes).toMap
+
+      val vars = variablesOf(f).toSeq.sortBy(_.uniqueName)
+      val newVars = vars.map(id => FreshIdentifier(id.name, instantiateType(id.getType, tpMap), true))
+
+      val Forall(fargs, body) = instantiateType(f, tpMap, (vars zip newVars).toMap)
+      val mapping = (newVars zip argsSeq).map(p => p._1 -> unit.jvmToValue(p._2, p._1.getType)).toMap
+      val cnstr = Not(replaceFromIDs(mapping, body))
+      solver.assertCnstr(cnstr)
+
+      if (domains.isDefined) {
+        val dom = domains.get
+        val quantifiers = fargs.map(_.id).toSet
+        val quorums = extractQuorums(body, quantifiers)
+
+        val domainCnstr = orJoin(quorums.map { quorum =>
+          val quantifierDomains = quorum.flatMap { case (path, caller, args) =>
+            val domain = caller match {
+              case Variable(id) => dom.get(mapping(id))
+              case _ => ctx.reporter.fatalError("Unexpected quantifier matcher: " + caller)
+            }
+
+            args.zipWithIndex.flatMap {
+              case (Variable(id),idx) if quantifiers(id) =>
+                Some(id -> domain.map(cargs => path -> cargs(idx)))
+              case _ => None
+            }
+          }
+
+          val domainMap = quantifierDomains.groupBy(_._1).mapValues(_.map(_._2).flatten)
+          andJoin(domainMap.toSeq.map { case (id, dom) =>
+            orJoin(dom.toSeq.map { case (path, value) => and(path, Equals(Variable(id), value)) })
+          })
+        })
+
+        solver.assertCnstr(domainCnstr)
+      }
+
+      try {
+        solver.check match {
+          case Some(negRes) =>
+            val res = !negRes
+            val total = System.currentTimeMillis-tStart
+
+            ctx.reporter.debug("Verification took "+total+"ms")
+            ctx.reporter.debug("Finished forall evaluation with: "+res)
 
+            forallCache += (id, argsSeq) -> res
+            res
+
+          case _ =>
+            throw new LeonCodeGenRuntimeException("Timeout exceeded")
+        }
+      } finally {
+        solver.free()
+        solverf.shutdown()
+      }
+    }
+  }
 }
 
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index f63bed50fb2835eca2ebf91102992b0e5951968e..59e9be41863b313202f3821e137419e8872cbc01 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -13,7 +13,6 @@ import codegen.CodeGenParams
 
 import leon.codegen.runtime.LeonCodeGenRuntimeException
 import leon.codegen.runtime.LeonCodeGenEvaluationException
-import leon.codegen.runtime.LeonCodeGenQuantificationException
 
 class CodeGenEvaluator(ctx: LeonContext, val unit : CompilationUnit) extends Evaluator(ctx, unit.program) with DeterministicEvaluator {
 
diff --git a/src/main/scala/leon/evaluators/DualEvaluator.scala b/src/main/scala/leon/evaluators/DualEvaluator.scala
index b61bcb5a038dc47482beb926f5a6bce43e2fccee..e387e4f0c6eb0f19064e7575a400b004ea13e2aa 100644
--- a/src/main/scala/leon/evaluators/DualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DualEvaluator.scala
@@ -128,7 +128,7 @@ class DualEvaluator(ctx: LeonContext, prog: Program, params: CodeGenParams)
 
 
   override def eval(ex: Expr, model: solvers.Model) = {
-    monitor = unit.getMonitor(model, params.maxFunctionInvocations, false)
+    monitor = unit.getMonitor(model, params.maxFunctionInvocations)
     super.eval(ex, model)
   }
 
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index ad705725688dbccc5c858fd745980a9719c0ad53..22aa09a4dd90d59a5f013e242f1b2337567eef4c 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -3,7 +3,7 @@
 package leon
 package evaluators
 
-import leon.purescala.Quantification._
+import purescala.Quantification._
 import purescala.Constructors._
 import purescala.ExprOps._
 import purescala.Expressions.Pattern
@@ -13,9 +13,10 @@ import purescala.Types._
 import purescala.Common._
 import purescala.Expressions._
 import purescala.Definitions._
-import leon.solvers.{HenkinModel, Model, SolverFactory}
+import purescala.DefOps
+import solvers.{HenkinModel, Model, SolverFactory}
 import scala.collection.mutable.{Map => MutableMap}
-import leon.purescala.DefOps
+import scala.concurrent.duration._
 import org.apache.commons.lang3.StringEscapeUtils
 
 abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int)
@@ -521,7 +522,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
       frlCache.getOrElse((f, context), {
         val tStart = System.currentTimeMillis
 
-        val solverf = SolverFactory.getFromSettings(ctx, program)
+        val solverf = SolverFactory.getFromSettings(ctx, program).withTimeout(1.second)
         val solver  = solverf.getNewSolver()
 
         try {
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 23b32e0ee96ec98dca890a4a17ae8541c20244cb..3437d34efeef0d47a37eded5d85cb167d8ee2b6b 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -345,6 +345,7 @@ object Constructors {
       val (ids, bds) = defs.unzip
 
       letTuple(ids, tupleWrap(bds), replaceFromIDs(subst, body))
+
     case _ =>
       Application(fn, realArgs)
    }
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index ce6b7fb4d863f290dd087074e8734cdc6f8b5013..af5a04eb8a07c404b7d7f0ac6945254a7ec5c227 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1994,7 +1994,7 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
           Let(i, e, apply(b, args))
         case LetTuple(is, es, b) =>
           letTuple(is, es, apply(b, args))
-        case l@Lambda(params, body) =>
+        case l @ Lambda(params, body) =>
           l.withParamSubst(args, body)
         case _ => Application(expr, args)
       }
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 14cf3b8250682a71285fffb3fd34e2e25608cdb1..6e694843c477ccfa9f2c706e7208f783e2cca677 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -127,9 +127,43 @@ object TypeOps extends { val Deconstructor = NAryType } with SubTreeOps[TypeTree
       if (args.forall(_.isDefined)) Some(TupleType(args.map(_.get))) else None
 
     case (FunctionType(from1, to1), FunctionType(from2, to2)) =>
-      // TODO: make functions contravariant to arg. types
-      if (from1 == from2) {
-        leastUpperBound(to1, to2) map { FunctionType(from1, _) }
+      val args = (from1 zip from2).map(p => greatestLowerBound(p._1, p._2))
+      if (args.forall(_.isDefined)) {
+        leastUpperBound(to1, to2) map { FunctionType(args.map(_.get), _) }
+      } else {
+        None
+      }
+
+    case (o1, o2) if o1 == o2 => Some(o1)
+    case _ => None
+  }
+
+  def greatestLowerBound(t1: TypeTree, t2: TypeTree): Option[TypeTree] = (t1,t2) match {
+    case (c1: ClassType, c2: ClassType) =>
+
+      def computeChains(ct: ClassType): Set[ClassType] = ct.parent match {
+        case Some(pct) =>
+          computeChains(pct) + ct
+        case None =>
+          Set(ct)
+      }
+
+      if (computeChains(c1)(c2)) {
+        Some(c2)
+      } else if (computeChains(c2)(c1)) {
+        Some(c1)
+      } else {
+        None
+      }
+
+    case (TupleType(args1), TupleType(args2)) =>
+      val args = (args1 zip args2).map(p => greatestLowerBound(p._1, p._2))
+      if (args.forall(_.isDefined)) Some(TupleType(args.map(_.get))) else None
+
+    case (FunctionType(from1, to1), FunctionType(from2, to2)) =>
+      val args = (from1 zip from2).map(p => leastUpperBound(p._1, p._2))
+      if (args.forall(_.isDefined)) {
+        greatestLowerBound(to1, to2).map { FunctionType(args.map(_.get), _) }
       } else {
         None
       }
@@ -381,6 +415,10 @@ object TypeOps extends { val Deconstructor = NAryType } with SubTreeOps[TypeTree
           case m @ FiniteMap(elems, from, to) =>
             FiniteMap(elems.map{ case (k, v) => (srec(k), srec(v)) }, tpeSub(from), tpeSub(to)).copiedFrom(m)
 
+          case f @ FiniteLambda(mapping, dflt, FunctionType(from, to)) =>
+            FiniteLambda(mapping.map { case (ks, v) => ks.map(srec) -> srec(v) }, srec(dflt),
+              FunctionType(from.map(tpeSub), tpeSub(to))).copiedFrom(f)
+
           case v @ Variable(id) if idsMap contains id =>
             Variable(idsMap(id)).copiedFrom(v)
 
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index bba8ba20d9bbf849874052924647d55cb6420d2d..10447122bfa64a3bfc0fe7eecd996b1028b68229 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -190,7 +190,7 @@ trait AbstractUnrollingSolver[T]
     if (silenceErrors) reporter.debug(msg) else reporter.warning(msg)
 
   private def extractModel(wrapper: ModelWrapper): Model =
-    new Model(freeVars.toMap.map(p => p._1 -> wrapper.get(p._1).get))
+    new Model(freeVars.toMap.map(p => p._1 -> wrapper.get(p._1).getOrElse(simplestValue(p._1.getType))))
 
   private def validateModel(model: Model, assumptions: Seq[Expr], silenceErrors: Boolean): Boolean = {
     val expr = andJoin(assumptions ++ constraints)
@@ -234,7 +234,7 @@ trait AbstractUnrollingSolver[T]
     }
 
     val model = new Model(freeVars.toMap.map { case (id, _) =>
-      val value = wrapped.get(id).get
+      val value = wrapped.get(id).getOrElse(simplestValue(id.getType))
       id -> (funDomains.get(id) match {
         case Some(domain) =>
           val FiniteLambda(_, dflt, tpe) = value
@@ -281,7 +281,7 @@ trait AbstractUnrollingSolver[T]
     }
 
     new Model(freeVars.toMap.map { case (id, idT) =>
-      val value = wrapped.get(id).get
+      val value = wrapped.get(id).getOrElse(simplestValue(id.getType))
       id -> (id.getType match {
         case FunctionType(from, to) =>
           val params = from.map(tpe => FreshIdentifier("x", tpe, true))
@@ -481,32 +481,29 @@ trait AbstractUnrollingSolver[T]
       if (!foundDefinitiveAnswer && !interrupted) {
         reporter.debug("- We need to keep going")
 
-        if (quantify) {
-          // further quantifier instantiations are required!
-          val newClauses = unrollingBank.instantiateQuantifiers
-          reporter.debug(" - more instantiations")
+        reporter.debug(" - more instantiations")
+        val newClauses = unrollingBank.instantiateQuantifiers(force = quantify)
 
-          for (cls <- newClauses) {
-            solverAssert(cls)
-          }
+        for (cls <- newClauses) {
+          solverAssert(cls)
+        }
 
-          reporter.debug(" - finished instantiating")
-        } else {
-          // unfolling `unfoldFactor` times
-          for (i <- 1 to unfoldFactor.toInt) {
-            val toRelease = unrollingBank.getBlockersToUnlock
+        reporter.debug(" - finished instantiating")
 
-            reporter.debug(" - more unrollings")
+        // unfolling `unfoldFactor` times
+        for (i <- 1 to unfoldFactor.toInt) {
+          val toRelease = unrollingBank.getBlockersToUnlock
 
-            val newClauses = unrollingBank.unrollBehind(toRelease)
+          reporter.debug(" - more unrollings")
 
-            for (ncl <- newClauses) {
-              solverAssert(ncl)
-            }
-          }
+          val newClauses = unrollingBank.unrollBehind(toRelease)
 
-          reporter.debug(" - finished unrolling")
+          for (ncl <- newClauses) {
+            solverAssert(ncl)
+          }
         }
+
+        reporter.debug(" - finished unrolling")
       }
     }
 
@@ -579,6 +576,7 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
     val model = solver.getModel
     def get(id: Identifier): Option[Expr] = model.get(id)
     def eval(elem: Expr, tpe: TypeTree): Option[Expr] = evaluator.eval(elem, model).result
+    override def toString = model.toMap.mkString("\n")
   }
 
   override def dbg(msg: => Any) = underlying.dbg(msg)
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index 5262ab9c72aaf3ccc677ad1124ad8a28fd424fa8..ea5369e8c4c1c2a489d91e0e5f3f99c22bbdce54 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -135,7 +135,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
   private val quantifications = new IncrementalSeq[MatcherQuantification]
   private val instCtx         = new InstantiationContext
 
-  private val ignoredMatchers = new ContextMap
+  private val ignoredMatchers = new IncrementalSeq[(Int, Set[T], Matcher[T])]
   private val ignoredSubsts   = new IncrementalMap[MatcherQuantification, MutableSet[(Int, Set[T], Map[T,Arg[T]])]]
   private val handledSubsts   = new IncrementalMap[MatcherQuantification, MutableSet[(Set[T], Map[T,Arg[T]])]]
 
@@ -148,10 +148,6 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
       handledSubsts, known, lambdaAxioms, templates) ++ super.incrementals
 
   private var currentGen = 0
-  private def minGen = {
-    val gens = ignoredSubsts.toSeq.flatMap(_._2).map(_._1)
-    if (gens.isEmpty) currentGen else gens.min
-  }
 
   private sealed abstract class MatcherKey(val tpe: TypeTree)
   private case class CallerKey(caller: T, tt: TypeTree) extends MatcherKey(tt)
@@ -168,9 +164,11 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
   private def correspond(qm: Matcher[T], m: Matcher[T]): Boolean =
     correspond(qm, m.caller, m.tpe)
 
-  @inline
-  private def correspond(qm: Matcher[T], caller: T, tpe: TypeTree): Boolean =
-    matcherKey(qm.caller, qm.tpe) == matcherKey(caller, tpe)
+  private def correspond(qm: Matcher[T], caller: T, tpe: TypeTree): Boolean = {
+    val qkey = matcherKey(qm.caller, qm.tpe)
+    val key = matcherKey(caller, tpe)
+    qkey == key || (qkey.tpe == key.tpe && (qkey.isInstanceOf[TypeKey] || key.isInstanceOf[TypeKey]))
+  }
 
   private val uniformQuantMap: MutableMap[TypeTree, Seq[T]] = MutableMap.empty
   private val uniformQuantSet: MutableSet[T]                = MutableSet.empty
@@ -299,16 +297,6 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
 
     def instantiations: Map[MatcherKey, Matchers] =
       (funMap.toMap ++ tpeMap.map { case (tpe,ms) => TypeKey(tpe) -> ms }).mapValues(_.toMatchers)
-
-    def consume: Matchers = {
-      val matchers = funMap.iterator.flatMap(_._2.toMatchers).toSet ++ tpeMap.flatMap(_._2.toMatchers)
-      funMap.clear
-      tpeMap.clear
-      matchers
-    }
-
-    def isEmpty = funMap.isEmpty && tpeMap.isEmpty
-    def nonEmpty = !isEmpty
   }
 
   private class InstantiationContext private (
@@ -486,9 +474,10 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
         Instantiation.empty[T]
       } else {
         handledSubsts(this) += enablers -> subst
+        val allEnablers = fixpoint((enablers: Set[T]) => enablers.flatMap(blockerParents))(enablers)
 
         var instantiation = Instantiation.empty[T]
-        val (enabler, optEnabler) = freshBlocker(enablers)
+        val (enabler, optEnabler) = freshBlocker(allEnablers)
         if (optEnabler.isDefined) {
           instantiation = instantiation withClause encoder.mkEquals(enabler, optEnabler.get)
         }
@@ -510,7 +499,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
           if (strict && (matchers(m) || transMatchers(m))) {
             instantiation ++= instCtx.instantiate(sb, sm)(quantifications.toSeq : _*)
           } else if (!matchers(m)) {
-            ignoredMatchers += sb -> sm
+            ignoredMatchers += ((currentGen + 3, sb, sm))
           }
         }
 
@@ -524,7 +513,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
       val nextGen = (if (matchers.forall { m =>
         val sm = m.substitute(substituter, msubst)
         instCtx(enablers -> sm)
-      }) currentGen + 3 else currentGen + 5)
+      }) currentGen + 3 else currentGen + 3)
 
       ignoredSubsts(this) += ((nextGen, enablers, subst))
     }
@@ -565,19 +554,26 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
   }
 
   private lazy val blockerId = FreshIdentifier("blocker", BooleanType, true)
-  private lazy val blockerCache: MutableMap[T, T] = MutableMap.empty
+  private lazy val enablersToBlocker: MutableMap[Set[T], T] = MutableMap.empty
+  private lazy val blockerToEnablers: MutableMap[T, Set[T]] = MutableMap.empty
   private def freshBlocker(enablers: Set[T]): (T, Option[T]) = enablers.toSeq match {
     case Seq(b) if isBlocker(b) => (b, None)
     case _ =>
-      val enabler = encodeEnablers(enablers)
-      blockerCache.get(enabler) match {
+      val last = enablersToBlocker.get(enablers).orElse {
+        val initialEnablers = enablers.flatMap(blockerToEnablers.get).flatten
+        enablersToBlocker.get(initialEnablers)
+      }
+
+      last match {
         case Some(b) => (b, None)
         case None =>
           val nb = encoder.encodeId(blockerId)
-          blockerCache += enabler -> nb
+          enablersToBlocker += enablers -> nb
+          blockerToEnablers += nb -> enablers
           for (b <- enablers if isBlocker(b)) implies(b, nb)
           blocker(nb)
-          (nb, Some(enabler))
+
+          (nb, Some(encodeEnablers(enablers)))
       }
   }
 
@@ -818,17 +814,31 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
 
   def hasIgnored: Boolean = ignoredSubsts.nonEmpty || ignoredMatchers.nonEmpty
 
-  def instantiateIgnored: Instantiation[T] = {
+  def instantiateIgnored(force: Boolean = false): Instantiation[T] = {
+    currentGen = if (!force) currentGen + 1 else {
+      val gens = ignoredSubsts.toSeq.flatMap(_._2).map(_._1) ++ ignoredMatchers.toSeq.map(_._1)
+      if (gens.isEmpty) currentGen else gens.min
+    }
+
     var instantiation = Instantiation.empty[T]
-    for ((b,m) <- ignoredMatchers.consume) {
-      instantiation ++= instantiateMatcher(b, m)
+
+    val matchersToRelease = ignoredMatchers.toList.flatMap { case e @ (gen, b, m) =>
+      if (gen == currentGen) {
+        ignoredMatchers -= e
+        Some(b -> m)
+      } else {
+        None
+      }
     }
 
-    val min = minGen
-    val toRelease = quantifications.toList.flatMap { q =>
+    for ((bs,m) <- matchersToRelease) {
+      instCtx.instantiate(bs, m)(quantifications.toSeq : _*)
+    }
+
+    val substsToRelease = quantifications.toList.flatMap { q =>
       val qsubsts = ignoredSubsts(q)
       qsubsts.toList.flatMap { case e @ (gen, enablers, subst) =>
-        if (gen == min) {
+        if (gen == currentGen) {
           qsubsts -= e
           Some((q, enablers, subst))
         } else {
@@ -837,12 +847,10 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
       }
     }
 
-    for ((q, enablers, subst) <- toRelease) {
+    for ((q, enablers, subst) <- substsToRelease) {
       instantiation ++= q.instantiateSubst(enablers, subst, strict = false)
     }
 
-    // Note that minGen changed after removing stuff from ignoredSubsts!
-    currentGen = minGen
     instantiation
   }
 
@@ -851,7 +859,8 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
     //val keySets = scala.collection.mutable.Map.empty[MatcherKey, T]
     val keyClause = MutableMap.empty[MatcherKey, (Seq[T], T)]
 
-    for ((key, ctx) <- ignoredMatchers.instantiations) {
+    for ((_, bs, m) <- ignoredMatchers) {
+      val key = matcherKey(m.caller, m.tpe)
       val QTM(argTypes, _) = key.tpe
 
       val (values, clause) = keyClause.getOrElse(key, {
@@ -877,10 +886,9 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
         res
       })
 
-      for ((b, m) <- ctx.toSeq) {
-        val substMap = (values zip m.args.map(_.encoded)).toMap
-        clauses += encoder.substitute(substMap)(encoder.mkImplies(b, clause))
-      }
+      val b = encodeEnablers(bs)
+      val substMap = (values zip m.args.map(_.encoded)).toMap
+      clauses += encoder.substitute(substMap)(encoder.mkImplies(b, clause))
     }
 
     for (q <- quantifications) {
@@ -894,11 +902,14 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
       val valuesP = values.map(v => v -> encoder.encodeId(v))
       val exprT = encoder.encodeExpr(elemsP.toMap ++ valuesP + guardP)(expr)
 
-      val disjunction = encoder.mkOr(handledSubsts(q).toSeq.map { case (enablers, subst) =>
-        val b = if (enablers.isEmpty) trueT else encoder.mkAnd(enablers.toSeq : _*)
-        val substMap = (elemsP.map(_._2) zip q.quantifiers.map(p => subst(p._2).encoded)).toMap + (guardP._2 -> b)
-        encoder.substitute(substMap)(exprT)
-      } : _*)
+      val disjunction = handledSubsts(q) match {
+        case set if set.isEmpty => encoder.encodeExpr(Map.empty)(BooleanLiteral(false))
+        case set => encoder.mkOr(set.toSeq.map { case (enablers, subst) =>
+          val b = if (enablers.isEmpty) trueT else encoder.mkAnd(enablers.toSeq : _*)
+          val substMap = (elemsP.map(_._2) zip q.quantifiers.map(p => subst(p._2).encoded)).toMap + (guardP._2 -> b)
+          encoder.substitute(substMap)(exprT)
+        } : _*)
+      }
 
       for ((_, enablers, subst) <- ignoredSubsts(q)) {
         val b = if (enablers.isEmpty) trueT else encoder.mkAnd(enablers.toSeq : _*)
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index b9c95ba768064133a64c61ae64efd85360d1fb07..2b0e95a4d77de19253730a7fde9b2e04890ca5f6 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -32,6 +32,16 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
 
   private def emptyClauses: Clauses = (Map.empty, Map.empty, Map.empty, Map.empty, Seq.empty, Seq.empty)
 
+  private implicit class ClausesWrapper(clauses: Clauses) {
+    def ++(that: Clauses): Clauses = {
+      val (thisConds, thisExprs, thisTree, thisGuarded, thisLambdas, thisQuants) = clauses
+      val (thatConds, thatExprs, thatTree, thatGuarded, thatLambdas, thatQuants) = that
+
+      (thisConds ++ thatConds, thisExprs ++ thatExprs, thisTree merge thatTree,
+        thisGuarded merge thatGuarded, thisLambdas ++ thatLambdas, thisQuants ++ thatQuants)
+    }
+  }
+
   val manager = new QuantificationManager[T](encoder)
 
   def mkTemplate(body: Expr): FunctionTemplate[T] = {
@@ -54,7 +64,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
     }
 
     // The precondition if it exists.
-    val prec : Option[Expr] = tfd.precondition.map(p => matchToIfThenElse(p))
+    val prec : Option[Expr] = tfd.precondition.map(p => simplifyHOFunctions(matchToIfThenElse(p)))
 
     val newBody : Option[Expr] = tfd.body.map(b => matchToIfThenElse(b))
     val lambdaBody : Option[Expr] = newBody.map(b => simplifyHOFunctions(b))
@@ -63,20 +73,18 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
     val lambdaArguments: Seq[Identifier] = lambdaBody.map(lambdaArgs).toSeq.flatten
     val invocation : Expr = FunctionInvocation(tfd, funDefArgs.map(_.toVariable))
 
-    val invocationEqualsBody : Option[Expr] = lambdaBody match {
+    val invocationEqualsBody : Seq[Expr] = lambdaBody match {
       case Some(body) if isRealFunDef =>
-        val b : Expr = and(
-          liftedEquals(invocation, body, lambdaArguments),
-          Equals(invocation, body))
+        val bs = liftedEquals(invocation, body, lambdaArguments) :+ Equals(invocation, body)
 
-        Some(if(prec.isDefined) {
-          Implies(prec.get, b)
+        if(prec.isDefined) {
+          bs.map(Implies(prec.get, _))
         } else {
-          b
-        })
+          bs
+        }
 
       case _ =>
-        None
+        Seq.empty
     }
 
     val start : Identifier = FreshIdentifier("start", BooleanType, true)
@@ -88,7 +96,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
     val substMap : Map[Identifier, T] = arguments.toMap + pathVar
 
     val (bodyConds, bodyExprs, bodyTree, bodyGuarded, bodyLambdas, bodyQuantifications) = if (isRealFunDef) {
-      invocationEqualsBody.map(expr => mkClauses(start, expr, substMap)).getOrElse(emptyClauses)
+      invocationEqualsBody.foldLeft(emptyClauses)((clsSet, cls) => clsSet ++ mkClauses(start, cls, substMap))
     } else {
       mkClauses(start, lambdaBody.get, substMap)
     }
@@ -96,7 +104,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
     // Now the postcondition.
     val (condVars, exprVars, condTree, guardedExprs, lambdas, quantifications) = tfd.postcondition match {
       case Some(post) =>
-        val newPost : Expr = application(matchToIfThenElse(post), Seq(invocation))
+        val newPost : Expr = simplifyHOFunctions(application(matchToIfThenElse(post), Seq(invocation)))
 
         val postHolds : Expr =
           if(tfd.hasPrecondition) {
@@ -128,7 +136,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
     case _ => Seq.empty
   }
 
-  private def liftedEquals(invocation: Expr, body: Expr, args: Seq[Identifier], inlineFirst: Boolean = false): Expr = {
+  private def liftedEquals(invocation: Expr, body: Expr, args: Seq[Identifier], inlineFirst: Boolean = false): Seq[Expr] = {
     def rec(i: Expr, b: Expr, args: Seq[Identifier], inline: Boolean): Seq[Expr] = i.getType match {
       case FunctionType(from, to) =>
         val (currArgs, nextArgs) = args.splitAt(from.size)
@@ -141,7 +149,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
         Seq.empty
     }
 
-    andJoin(rec(invocation, body, args, inlineFirst))
+    rec(invocation, body, args, inlineFirst)
   }
 
   private def minimalFlattening(inits: Set[Identifier], conj: Expr): (Set[Identifier], Expr) = {
@@ -318,8 +326,8 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
               storeExpr(newExpr)
 
               def recAnd(pathVar: Identifier, partitions: Seq[Expr]): Unit = partitions match {
-                case x :: Nil if !requireDecomposition(x) =>
-                  storeGuarded(pathVar, Equals(Variable(newExpr), x))
+                case x :: Nil =>
+                  storeGuarded(pathVar, Equals(Variable(newExpr), rec(pathVar, x)))
 
                 case x :: xs =>
                   val newBool : Identifier = FreshIdentifier("b", BooleanType, true)
@@ -331,8 +339,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
 
                   recAnd(newBool, xs)
 
-                case Nil =>
-                  storeGuarded(pathVar, Variable(newExpr))
+                case Nil => scala.sys.error("Should never happen!")
               }
 
               recAnd(pathVar, seq)
@@ -348,8 +355,8 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
               storeExpr(newExpr)
 
               def recOr(pathVar: Identifier, partitions: Seq[Expr]): Unit = partitions match {
-                case x :: Nil if !requireDecomposition(x) =>
-                  storeGuarded(pathVar, Equals(Variable(newExpr), x))
+                case x :: Nil =>
+                  storeGuarded(pathVar, Equals(Variable(newExpr), rec(pathVar, x)))
 
                 case x :: xs =>
                   val newBool : Identifier = FreshIdentifier("b", BooleanType, true)
@@ -361,8 +368,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
 
                   recOr(newBool, xs)
 
-                case Nil =>
-                  storeGuarded(pathVar, Not(Variable(newExpr)))
+                case Nil => scala.sys.error("Should never happen!")
               }
 
               recOr(pathVar, seq)
@@ -423,11 +429,12 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
           val trArgs : Seq[T] = idArgs.map(id => substMap.getOrElse(id, encoder.encodeId(id)))
 
           val lid = FreshIdentifier("lambda", bestRealType(l.getType), true)
-          val clause = liftedEquals(Variable(lid), l, idArgs, inlineFirst = true)
+          val clauses = liftedEquals(Variable(lid), l, idArgs, inlineFirst = true)
 
           val localSubst: Map[Identifier, T] = substMap ++ condVars ++ exprVars ++ lambdaVars
           val clauseSubst: Map[Identifier, T] = localSubst ++ (idArgs zip trArgs)
-          val (lambdaConds, lambdaExprs, lambdaTree, lambdaGuarded, lambdaTemplates, lambdaQuants) = mkClauses(pathVar, clause, clauseSubst)
+          val (lambdaConds, lambdaExprs, lambdaTree, lambdaGuarded, lambdaTemplates, lambdaQuants) =
+            clauses.foldLeft(emptyClauses)((clsSet, cls) => clsSet ++ mkClauses(pathVar, cls, clauseSubst))
 
           val ids: (Identifier, T) = lid -> storeLambda(lid)
           val dependencies: Map[Identifier, T] = variablesOf(l).map(id => id -> localSubst(id)).toMap
diff --git a/src/main/scala/leon/solvers/templates/TemplateManager.scala b/src/main/scala/leon/solvers/templates/TemplateManager.scala
index cdfe0c9ed6462b322b760e635122f5c3b11d2923..332d3fdf1442bfab25f72839d9ef00e04de73dd5 100644
--- a/src/main/scala/leon/solvers/templates/TemplateManager.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateManager.scala
@@ -436,7 +436,8 @@ class TemplateManager[T](protected[templates] val encoder: TemplateEncoder[T]) e
 
   def blocker(b: T): Unit = condImplies += (b -> Set.empty)
   def isBlocker(b: T): Boolean = condImplies.isDefinedAt(b) || condImplied.isDefinedAt(b)
-  
+  def blockerParents(b: T): Set[T] = condImplied(b)
+
   def implies(b1: T, b2: T): Unit = implies(b1, Set(b2))
   def implies(b1: T, b2s: Set[T]): Unit = {
     val fb2s = b2s.filter(_ != b1)
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index ce2af7c9e29634ff5a50dc4b493477c63f774229..a84dc350e38275bf30b592d1e82badd0576b87c8 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -232,8 +232,8 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
     }
   }
 
-  def instantiateQuantifiers: Seq[T] = {
-    val (newExprs, callBlocks, appBlocks) = manager.instantiateIgnored
+  def instantiateQuantifiers(force: Boolean = false): Seq[T] = {
+    val (newExprs, callBlocks, appBlocks) = manager.instantiateIgnored(force)
     val blockExprs = freshAppBlocks(appBlocks.keys)
     val gens = (callInfos.values.map(_._1) ++ appInfos.values.map(_._1))
     val gen = if (gens.nonEmpty) gens.min else 0
@@ -246,7 +246,15 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
       registerAppBlocker(nextGeneration(gen), newApp, newInfos)
     }
 
-    newExprs ++ blockExprs
+    val clauses = newExprs ++ blockExprs
+    if (clauses.nonEmpty) {
+      reporter.debug("Instantiating ignored quantifiers ("+clauses.size+")")
+      for (cl <- clauses) {
+        reporter.debug("  . "+cl)
+      }
+    }
+
+    clauses
   }
 
   def unrollBehind(ids: Seq[T]): Seq[T] = {
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index f1ee6bfba315c53f4e094a95959039f2c6f7ed72..3cadf39a6e3853196d4cdf6b7493ea91a6077c73 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -618,7 +618,7 @@ trait AbstractZ3Solver extends Solver {
 
         case Z3AppAST(decl, args) =>
           val argsSize = args.size
-          if(argsSize == 0 && (variables containsB t)) {
+          if (argsSize == 0 && (variables containsB t)) {
             variables.toA(t)
           } else if(functions containsB decl) {
             val tfd = functions.toA(decl)
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 7ba4bf9eade43bc1f567e447c067a1e61bf16360..1fb0088348d1ebdd9e587aa5231d57338140b75a 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -100,7 +100,10 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
     */
 
     def get(id: Identifier): Option[Expr] = variables.getB(id.toVariable).flatMap {
-      z3ID => eval(z3ID, id.getType)
+      z3ID => eval(z3ID, id.getType) match {
+        case Some(Variable(id)) => None
+        case e => e
+      }
     }
 
     def eval(elem: Z3AST, tpe: TypeTree): Option[Expr] = tpe match {
@@ -114,6 +117,8 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
         case Some(t) => softFromZ3Formula(model, t, other)
       }
     }
+
+    override def toString = model.toString
   }
 
   val printable = (z3: Z3AST) => new Printable {
diff --git a/src/main/scala/leon/utils/IncrementalSeq.scala b/src/main/scala/leon/utils/IncrementalSeq.scala
index 4ec9290b5eb5c2672b0f4fae44760081ca14ba80..fbf042868415378d4af4877ee8766f1303632373 100644
--- a/src/main/scala/leon/utils/IncrementalSeq.scala
+++ b/src/main/scala/leon/utils/IncrementalSeq.scala
@@ -13,6 +13,7 @@ class IncrementalSeq[A] extends IncrementalState
                         with Builder[A, IncrementalSeq[A]] {
 
   private[this] val stack = new Stack[ArrayBuffer[A]]()
+  stack.push(new ArrayBuffer())
 
   def clear() : Unit = {
     stack.clear()
@@ -20,11 +21,11 @@ class IncrementalSeq[A] extends IncrementalState
 
   def reset(): Unit = {
     clear()
-    push()
+    stack.push(new ArrayBuffer())
   }
 
   def push(): Unit = {
-    stack.push(new ArrayBuffer())
+    stack.push(stack.head.clone)
   }
 
   def pop(): Unit = {
@@ -33,9 +34,8 @@ class IncrementalSeq[A] extends IncrementalState
 
   def iterator = stack.flatten.iterator
   def +=(e: A) = { stack.head += e; this }
+  def -=(e: A) = { stack.head -= e; this }
 
   override def newBuilder = new scala.collection.mutable.ArrayBuffer()
   def result = this
-
-  push()
 }
diff --git a/src/main/scala/leon/utils/InliningPhase.scala b/src/main/scala/leon/utils/InliningPhase.scala
index 17fdf48bc88d88cca9c49e63672af6f3c76afa48..d69bbb9c32d6cd9f0d32281ec7b5af628aac5a15 100644
--- a/src/main/scala/leon/utils/InliningPhase.scala
+++ b/src/main/scala/leon/utils/InliningPhase.scala
@@ -3,12 +3,13 @@
 package leon.utils
 
 import leon._
+import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.TypeOps.instantiateType
 import purescala.ExprOps._
 import purescala.DefOps._
-import purescala.Constructors.caseClassSelector
+import purescala.Constructors.{caseClassSelector, application}
 
 object InliningPhase extends TransformationPhase {
 
@@ -25,26 +26,20 @@ object InliningPhase extends TransformationPhase {
 
     def doInline(fd: FunDef) = fd.flags(IsInlined) && !doNotInline(fd)
 
-    def simplifyImplicitClass(e: Expr) = e match {
-      case CaseClassSelector(cct, cc: CaseClass, id) =>
-        Some(caseClassSelector(cct, cc, id))
+    for (fd <- p.definedFunctions) {
+      fd.fullBody = preMap ({
+        case FunctionInvocation(tfd, args) if doInline(tfd.fd) =>
+          Some(replaceFromIDs((tfd.params.map(_.id) zip args).toMap, tfd.fullBody))
 
-      case _ =>
-        None
-    }
+        case CaseClassSelector(cct, cc: CaseClass, id) =>
+          Some(caseClassSelector(cct, cc, id))
 
-    def simplify(e: Expr) = {
-      fixpoint(postMap(simplifyImplicitClass))(e)
-    }
+        case Application(caller: Lambda, args) =>
+          Some(application(caller, args))
 
-    for (fd <- p.definedFunctions) {
-      fd.fullBody = simplify(preMap ({
-        case FunctionInvocation(TypedFunDef(fd, tps), args) if doInline(fd) =>
-          val newBody = instantiateType(fd.fullBody, (fd.tparams zip tps).toMap, Map())
-          Some(replaceFromIDs(fd.params.map(_.id).zip(args).toMap, newBody))
         case _ =>
           None
-      }, applyRec = true)(fd.fullBody))
+      }, applyRec = true)(fd.fullBody)
     }
 
     filterFunDefs(p, fd => !doInline(fd))
diff --git a/src/test/resources/regression/verification/purescala/invalid/AssociativityProperties.scala b/src/test/resources/regression/verification/purescala/invalid/AssociativityProperties.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b143816e8d5a28437701567b2459511882a805dd
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/AssociativityProperties.scala
@@ -0,0 +1,26 @@
+import leon.lang._
+
+object AssociativityProperties {
+
+  def isAssociative[A](f: (A,A) => A): Boolean = {
+    forall((x: A, y: A, z: A) => f(f(x, y), z) == f(x, f(y, z)))
+  }
+
+  def isCommutative[A](f: (A,A) => A): Boolean = {
+    forall((x: A, y: A) => f(x, y) == f(y, x))
+  }
+
+  def isRotate[A](f: (A,A) => A): Boolean = {
+    forall((x: A, y: A, z: A) => f(f(x, y), z) == f(f(y, z), x))
+  }
+
+  def assocNotCommutative[A](f: (A,A) => A): Boolean = {
+    require(isAssociative(f))
+    isCommutative(f)
+  }.holds
+
+  def commNotAssociative[A](f: (A,A) => A): Boolean = {
+    require(isCommutative(f))
+    isAssociative(f)
+  }.holds
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/AssociativityProperties.scala b/src/test/resources/regression/verification/purescala/valid/AssociativityProperties.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5c8530615dff1cdc15868be54a2b0019acba1844
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/AssociativityProperties.scala
@@ -0,0 +1,33 @@
+import leon.lang._
+
+object AssociativityProperties {
+
+  def isAssociative[A](f: (A,A) => A): Boolean = {
+    forall((x: A, y: A, z: A) => f(f(x, y), z) == f(x, f(y, z)))
+  }
+
+  def isCommutative[A](f: (A,A) => A): Boolean = {
+    forall((x: A, y: A) => f(x, y) == f(y, x))
+  }
+
+  def isRotate[A](f: (A,A) => A): Boolean = {
+    forall((x: A, y: A, z: A) => f(f(x, y), z) == f(f(y, z), x))
+  }
+
+  def assocPairs[A,B](f1: (A,A) => A, f2: (B,B) => B) = {
+    require(isAssociative(f1) && isAssociative(f2))
+    val fp = ((p1: (A,B), p2: (A,B)) => (f1(p1._1, p2._1), f2(p1._2, p2._2)))
+    isAssociative(fp)
+  }.holds
+
+  def assocRotate[A](f: (A,A) => A): Boolean = {
+    require(isCommutative(f) && isRotate(f))
+    isAssociative(f)
+  }.holds
+
+  def assocRotateInt(f: (BigInt, BigInt) => BigInt): Boolean = {
+    require(isCommutative(f) && isRotate(f))
+    isAssociative(f)
+  }.holds
+
+}
diff --git a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
index 6c450c1c8613f74c5a6679aaaf6035f59e593e66..ab1bfc6c469ecb167a760a84bd30443cdcc8b0dc 100644
--- a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
@@ -19,8 +19,8 @@ abstract class PureScalaVerificationSuite extends VerificationSuite {
   val opts: List[List[String]] = {
     List(
       List("--feelinglucky"),
-      List("--codegen", "--evalground", "--feelinglucky"),
-      List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky")
+      List("--codegen", /*"--evalground",*/ "--feelinglucky"),
+      List("--solvers=fairz3,enum", "--codegen", /*"--evalground",*/ "--feelinglucky")
     ) ++ (
       if (isZ3Available) List(
         List("--solvers=smt-z3", "--feelinglucky")