fix flatten blocks

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 {

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) {

src/test/resources/regression/verification/xlang/valid/Blocks1.scala

+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))
+
+}

src/test/scala/leon/unit/xlang/ExprOpsSuite.scala

+/* 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()))
+  }
+
+}