diff --git a/src/main/scala/leon/xlang/ExprOps.scala b/src/main/scala/leon/xlang/ExprOps.scala
index a5013e5f8d87ccd0b6bb66e1b6db91e8c0528d9a..e4680286f9f52c1462f7510433606b93c862f8e9 100644
--- a/src/main/scala/leon/xlang/ExprOps.scala
+++ b/src/main/scala/leon/xlang/ExprOps.scala
@@ -21,9 +21,12 @@ object ExprOps {
   def flattenBlocks(expr: Expr): Expr = {
     postMap({
       case Block(exprs, last) =>
-        val nexprs = (exprs :+ last).flatMap{
+        val filtered = exprs.filter{
+          case UnitLiteral() => false
+          case _ => true
+        }
+        val nexprs = (filtered :+ last).flatMap{
           case Block(es2, el) => es2 :+ el
-          case UnitLiteral() => Seq()
           case e2 => Seq(e2)
         }
         Some(nexprs match {
diff --git a/src/main/scala/leon/xlang/Expressions.scala b/src/main/scala/leon/xlang/Expressions.scala
index 6426550620149de3d099e4cff99486ab327da5f5..c0e2d4deb3c8b71347a1fc63bbbc8a91034d597d 100644
--- a/src/main/scala/leon/xlang/Expressions.scala
+++ b/src/main/scala/leon/xlang/Expressions.scala
@@ -28,8 +28,9 @@ object Expressions {
       Some((exprs :+ last, exprs => Block(exprs.init, exprs.last)))
     }
 
-    override def getPos = {
-      Position.between(exprs.head.getPos, last.getPos)
+    override def getPos = exprs.headOption match {
+      case Some(head) => Position.between(head.getPos, last.getPos)
+      case None => last.getPos
     }
 
     def printWith(implicit pctx: PrinterContext) {
diff --git a/src/test/resources/regression/verification/xlang/valid/Blocks1.scala b/src/test/resources/regression/verification/xlang/valid/Blocks1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a2266bcc6229c4a9fe91440f6738b3e6ea78de28
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Blocks1.scala
@@ -0,0 +1,10 @@
+object Blocks1 {
+
+  //this used to crash as we would simplify away the final Unit, and get a typing
+  //error during the solving part
+  def test(a: BigInt): Unit = {
+    42
+    ()
+  } ensuring(_ => a == (a + a - a))
+
+}
diff --git a/src/test/scala/leon/unit/xlang/ExprOpsSuite.scala b/src/test/scala/leon/unit/xlang/ExprOpsSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..df9b8022582c5922133a262ade700ef9a629f2b5
--- /dev/null
+++ b/src/test/scala/leon/unit/xlang/ExprOpsSuite.scala
@@ -0,0 +1,52 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.unit.xlang
+
+import org.scalatest._
+
+import leon.test._
+import leon.purescala.Common._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
+import leon.purescala.TypeOps.isSubtypeOf
+import leon.purescala.Definitions._
+import leon.xlang.Expressions._
+import leon.xlang.ExprOps._
+
+class ExprOpsSuite extends FunSuite with helpers.ExpressionsDSL {
+
+  test("flattenBlocks does not change a simple block") {
+    assert(flattenBlocks(Block(Seq(y), x)) === Block(Seq(y), x))
+    assert(flattenBlocks(Block(Seq(y, z), x)) === Block(Seq(y, z), x))
+  }
+
+  test("flattenBlocks of a single statement removes the block") {
+    assert(flattenBlocks(Block(Seq(), x)) === x)
+    assert(flattenBlocks(Block(Seq(), y)) === y)
+  }
+
+  test("flattenBlocks of a one nested block flatten everything") {
+    assert(flattenBlocks(Block(Seq(Block(Seq(y), z)), x)) === Block(Seq(y, z), x))
+    assert(flattenBlocks(Block(Seq(y, Block(Seq(), z)), x)) === Block(Seq(y, z), x))
+  }
+
+  test("flattenBlocks of a several nested blocks flatten everything") {
+    assert(flattenBlocks(Block(Seq(Block(Seq(), y), Block(Seq(), z)), x)) === Block(Seq(y, z), x))
+  }
+
+  test("flattenBlocks of a nested block in last expr should flatten") {
+    assert(flattenBlocks(Block(Seq(Block(Seq(), y)), Block(Seq(z), x))) === Block(Seq(y, z), x))
+  }
+
+  test("flattenBlocks should eliminate intermediate UnitLiteral") {
+    assert(flattenBlocks(Block(Seq(UnitLiteral(), y, z), x)) === Block(Seq(y, z), x))
+    assert(flattenBlocks(Block(Seq(y, UnitLiteral(), z), x)) === Block(Seq(y, z), x))
+    assert(flattenBlocks(Block(Seq(UnitLiteral(), UnitLiteral(), z), x)) === Block(Seq(z), x))
+    assert(flattenBlocks(Block(Seq(UnitLiteral()), x)) === x)
+  }
+
+  test("flattenBlocks should not eliminate trailing UnitLiteral") {
+    assert(flattenBlocks(Block(Seq(x), UnitLiteral())) === Block(Seq(x), UnitLiteral()))
+  }
+
+}