diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 0a80b3b53933a6bb6f5c88d8785ea8f3eb1cebaa..4efc43706dbe85879ed68e6a7b8a4989f95ab20e 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -25,6 +25,7 @@ import ExprOps._
 import TypeOps.{leastUpperBound, typesCompatible, typeParamsOf, canBeSubtypeOf}
 import xlang.Expressions.{Block => LeonBlock, _}
 import xlang.ExprOps._
+import xlang.Constructors.{block => leonBlock}
 
 import leon.utils.{Position => LeonPosition, OffsetPosition => LeonOffsetPosition, RangePosition => LeonRangePosition, Bijection, DefinedPosition}
 
@@ -1916,7 +1917,7 @@ trait CodeExtraction extends ASTExtractors {
 
       rest match {
         case Some(r) =>
-          LeonBlock(Seq(res), extractTree(r))
+          leonBlock(Seq(res, extractTree(r)))
         case None =>
           res
       }
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 0dbf1aba944dfbba2350a43163b6fa852e16ad2e..04e32eb311aec70c4b23a04d2cf50caacd65874e 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -633,6 +633,7 @@ class PrettyPrinter(opts: PrinterOptions,
   protected def noBracesSub(e: Expr): Seq[Expr] = e match {
     case Assert(_, _, bd) => Seq(bd)
     case Let(_, _, bd) => Seq(bd)
+    case xlang.Expressions.LetVar(_, _, bd) => Seq(bd)
     case LetDef(_, bd) => Seq(bd)
     case LetPattern(_, _, bd) => Seq(bd)
     case Require(_, bd) => Seq(bd)
@@ -646,6 +647,10 @@ class PrettyPrinter(opts: PrinterOptions,
     case (e: Expr, Some(within: Expr)) if noBracesSub(within) contains e => false
     case (_: Expr, Some(_: MatchCase)) => false
     case (_: LetDef, Some(_: LetDef)) => false
+    case (_: Expr, Some(_: xlang.Expressions.Block)) => false
+    case (_: xlang.Expressions.Block, Some(_: xlang.Expressions.While)) => false
+    case (_: xlang.Expressions.Block, Some(_: FunDef)) => false
+    case (_: xlang.Expressions.Block, Some(_: LetDef)) => false
     case (e: Expr, Some(_)) => true
     case _ => false
   }
diff --git a/src/main/scala/leon/xlang/Constructors.scala b/src/main/scala/leon/xlang/Constructors.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c55842f920a81cd06d508f3f4e76e29ceecbafaf
--- /dev/null
+++ b/src/main/scala/leon/xlang/Constructors.scala
@@ -0,0 +1,36 @@
+package leon
+package xlang
+
+import purescala.Expressions._
+import purescala.Types._
+import xlang.Expressions._
+import xlang.ExprOps._
+
+object Constructors {
+
+  def block(exprs: Seq[Expr]): Expr = {
+    require(exprs.nonEmpty)
+
+    val flat = exprs.flatMap{
+      case Block(es2, el) => es2 :+ el
+      case e2 => Seq(e2)
+    }
+
+    val init = flat.init
+    val last = flat.last
+    val filtered = init.filter{
+      case UnitLiteral() => false
+      case _ => true
+    }
+
+    val finalSeq = 
+      if(last == UnitLiteral() && filtered.last.getType == UnitType) filtered else (filtered :+ last)
+
+    finalSeq match {
+      case Seq() => UnitLiteral()
+      case Seq(e) => e
+      case es => Block(es.init, es.last)
+    }
+  }
+
+}
diff --git a/src/main/scala/leon/xlang/Expressions.scala b/src/main/scala/leon/xlang/Expressions.scala
index c0e2d4deb3c8b71347a1fc63bbbc8a91034d597d..e8dd17c3d281df05cd82bc369fbdc67503309ce5 100644
--- a/src/main/scala/leon/xlang/Expressions.scala
+++ b/src/main/scala/leon/xlang/Expressions.scala
@@ -50,7 +50,7 @@ object Expressions {
     }
 
     def printWith(implicit pctx: PrinterContext) {
-      p"$varId = $expr;"
+      p"$varId = $expr"
     }
   }
 
@@ -62,7 +62,7 @@ object Expressions {
     }
 
     def printWith(implicit pctx: PrinterContext) {
-      p"${obj}.${varId} = ${expr};"
+      p"${obj}.${varId} = ${expr}"
     }
   }