most tests are working

src/main/scala/leon/solvers/z3/FairZ3Solver.scala

@@ -291,7 +291,6 @@ class FairZ3Solver(context : LeonContext)
       val newClauses = unrollingBank.scanForNewTemplates(expression)
 
       for (cl <- newClauses) {
-        println("transforming to z3: " + cl)
         solver.assertCnstr(z3.mkImplies(guard, toZ3Formula(cl).get))
       }
     }

src/main/scala/leon/verification/AnalysisPhase.scala

@@ -21,7 +21,6 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
   )
 
   def run(ctx: LeonContext)(program: Program) : VerificationReport = {
-    println(program)
     val functionsToAnalyse : MutableSet[String] = MutableSet.empty
 
     for(opt <- ctx.options) opt match {

src/main/scala/leon/xlang/ImperativeCodeElimination.scala

@@ -24,7 +24,6 @@ object ImperativeCodeElimination extends TransformationPhase {
 
     val allFuns = pgm.definedFunctions
     allFuns.foreach(fd => fd.body.map(body => {
-      println("processing fun: " + fd)
       parent = fd
       val (res, scope, _) = toFunction(body)
       fd.body = Some(scope(res))
@@ -39,7 +38,6 @@ object ImperativeCodeElimination extends TransformationPhase {
   private def toFunction(expr: Expr): (Expr, Expr => Expr, Map[Identifier, Identifier]) = {
     val res = expr match {
       case LetVar(id, e, b) => {
-        println("in letvar with id: " + id)
         val newId = FreshIdentifier(id.name).setType(id.getType)
         val (rhsVal, rhsScope, rhsFun) = toFunction(e)
         varInScope += id

src/test/resources/regression/verification/xlang/invalid/MyTuple1.scala

-object MyTuple1 {
-
-  def foo(): Int = {
-    val t = (1, true, 3)
-    val a1 = t._1
-    val a2 = t._2
-    val a3 = t._3
-    a3
-  } ensuring( _ == 1)
-
-}

src/test/resources/regression/verification/xlang/invalid/MyTuple2.scala

-object MyTuple2 {
-
-  abstract class A
-  case class B(i: Int) extends A
-  case class C(a: A) extends A
-
-  def foo(): Int = {
-    val t = (B(2), C(B(3)))
-    t match {
-      case (B(x), C(y)) => x
-    }
-  } ensuring( _ == 3)
-
-}

src/test/resources/regression/verification/xlang/invalid/MyTuple3.scala

-object MyTuple3 {
-
-  def foo(t: (Int, Int)): (Int, Int) = {
-    t
-  } ensuring(res => res._1 > 0 && res._2 > 1)
-
-}

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

-object MyTuple1 {
-
-  def foo(): Int = {
-    val t = (1, true, 3)
-    val a1 = t._1
-    val a2 = t._2
-    val a3 = t._3
-    a3
-  } ensuring( _ == 3)
-
-}

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

-object MyTuple3 {
-
-  def foo(): Int = {
-    val t = ((2, 3), true)
-    t._1._2
-  } ensuring( _ == 3)
-
-}

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

-
-object MyTuple4 {
-
-  abstract class A
-  case class B(i: Int) extends A
-  case class C(a: A) extends A
-
-  def foo(): Int = {
-    val t = (1, (C(B(4)), 2), 3)
-    val (a1, (C(B(x)), a2), a3) = t
-    x
-  } ensuring( _ == 4)
-
-}

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

-object MyTuple1 {
-
-  abstract class A
-  case class B(t: (Int, Int)) extends A
-  case class C(a: A) extends A
-
-  def foo(): Int = {
-    val t: (Int, (A, Int), Int) = (1, (C(B((4, 5))), 2), 3)
-    t match {
-      case (_, (B((x, y)), _), _) => x
-      case (_, (C(B((_, x))), _), y) => x
-      case (_, _, x) => x
-    }
-  } ensuring( _ == 5)
-
-}

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

-object MyTuple6 {
-
-  def foo(t: (Int, Int)): (Int, Int) = {
-    require(t._1 > 0 && t._2 > 1)
-    t
-  } ensuring(res => res._1 > 0 && res._2 > 1)
-
-}

src/test/scala/leon/test/verification/XLangVerificationRegression.scala

@@ -20,10 +20,10 @@ class XLangVerificationRegression extends FunSuite {
 
   private def mkPipeline : Pipeline[List[String],VerificationReport] =
     leon.plugin.ExtractionPhase andThen       
+    xlang.ArrayTransformation andThen
     xlang.EpsilonElimination andThen
     xlang.ImperativeCodeElimination andThen
     xlang.FunctionClosure andThen
-    xlang.ArrayTransformation andThen
     leon.verification.AnalysisPhase
 
   private def mkTest(file : File)(block: Output=>Unit) = {
@@ -40,6 +40,8 @@ class XLangVerificationRegression extends FunSuite {
       assert(file.exists && file.isFile && file.canRead,
              "Benchmark %s is not a readable file".format(displayName))
 
+      println("testing " + displayName)
+
       val ctx = LeonContext(
         settings = Settings(
           synthesis = false,