diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 22c8c174b746865e2e6f6de250744a16ff9633f2..57618655f1e3f793030f9cc37f920bf628870a2f 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -123,6 +123,10 @@ class PrettyPrinter(opts: PrinterOptions,
         } else {
           p"""|?($es)"""
         }
+
+      case Forall(args, e) =>
+        p"""\u2200${typed(args.map(_.id))}. $e"""
+
       case e @ CaseClass(cct, args) =>
         opgm.flatMap { pgm => isListLiteral(e)(pgm) } match {
           case Some((tpe, elems)) =>
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 9942cc3b7638dfd6eb71bfa43935f6b32299c746..4c49c3101511df385988a3f8a429cee93adcd330 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -161,7 +161,9 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
 
     def requireDecomposition(e: Expr) = {
       exists{
-        case (_: FunctionInvocation) | (_: Assert) | (_: Ensuring) | (_: Choose) | (_: Application) => true
+        case (_: Choose) | (_: Forall) => true
+        case (_: Assert) | (_: Ensuring) => true
+        case (_: FunctionInvocation) | (_: Application) => true
         case _ => false
       }(e)
     }