diff --git a/src/main/scala/leon/Extensions.scala b/src/main/scala/leon/Extensions.scala
index 5905ec99820c7dff51cef6fef88705017a17614d..7d8469998f53c9abb14c9c84dfa123fb462900c2 100644
--- a/src/main/scala/leon/Extensions.scala
+++ b/src/main/scala/leon/Extensions.scala
@@ -98,6 +98,7 @@ object Extensions {
 
     allLoaded = defaultExtensions ++ loaded
     analysisExtensions = allLoaded.filter(_.isInstanceOf[Analyser]).map(_.asInstanceOf[Analyser])
+    analysisExtensions = new TestGeneration(extensionsReporter) +: analysisExtensions
 
     val solverExtensions0 = allLoaded.filter(_.isInstanceOf[Solver]).map(_.asInstanceOf[Solver])
     val solverExtensions1 = if(Settings.useQuickCheck) new RandomSolver(extensionsReporter) +: solverExtensions0 else solverExtensions0
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 638db0c2024152c46b9f735263b11e9ce01b5ca2..ee3daffb735a3fa97adb1600be050e3b3f258180 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -842,6 +842,18 @@ object Trees {
     }
     treeCatamorphism(convert, combine, compute, expr)
   }
+  def containsIfExpr(expr: Expr): Boolean = {
+    def convert(t : Expr) : Boolean = t match {
+      case (i: IfExpr) => true
+      case _ => false
+    }
+    def combine(c1 : Boolean, c2 : Boolean) : Boolean = c1 || c2
+    def compute(t : Expr, c : Boolean) = t match {
+      case (i: IfExpr) => true
+      case _ => c
+    }
+    treeCatamorphism(convert, combine, compute, expr)
+  }
 
   def variablesOf(expr: Expr) : Set[Identifier] = {
     def convert(t: Expr) : Set[Identifier] = t match {
diff --git a/testcases/Abs.scala b/testcases/Abs.scala
index 5efb41797b5dc4401407c5fea7c3fc6a7591f4f2..52baf710140b76bf5edeeda52ef9e0da5385734f 100644
--- a/testcases/Abs.scala
+++ b/testcases/Abs.scala
@@ -1,51 +1,5 @@
-import leon.Utils._
-
 object Abs {
 
-
-  def abs(tab: Map[Int, Int], size: Int): Map[Int, Int] = ({
-    require(size <= 5 && isArray(tab, size))
-    var k = 0
-    var tabres = Map.empty[Int, Int]
-    (while(k < size) {
-      if(tab(k) < 0)
-        tabres = tabres.updated(k, -tab(k))
-      else
-        tabres = tabres.updated(k, tab(k))
-      k = k + 1
-    }) invariant(isArray(tabres, k) && k >= 0 && k <= size && isPositive(tabres, k))
-    tabres
-  }) ensuring(res => isArray(res, size) && isPositive(res, size))
-
-  def isPositive(a: Map[Int, Int], size: Int): Boolean = {
-    require(size <= 10 && isArray(a, size))
-    def rec(i: Int): Boolean = {
-      require(i >= 0)
-      if(i >= size) 
-        true 
-      else {
-        if(a(i) < 0) 
-          false 
-        else 
-          rec(i+1)
-      }
-    }
-    rec(0)
-  }
-
-  def isArray(a: Map[Int, Int], size: Int): Boolean = {
-
-    def rec(i: Int): Boolean = {
-      require(i >= 0)  
-      if(i >= size) true else {
-        if(a.isDefinedAt(i)) rec(i+1) else false
-      }
-    }
-
-    if(size < 0)
-      false
-    else
-      rec(0)
-  }
+  def abs(x: Int): Int = (if(x < 0) -x else x) ensuring(_ >= 0)
 
 }
diff --git a/testcases/AbsArray.scala b/testcases/AbsArray.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0086891cdafc5a62987d5563695b38983de24fb4
--- /dev/null
+++ b/testcases/AbsArray.scala
@@ -0,0 +1,51 @@
+import leon.Utils._
+
+object AbsArray {
+
+
+  def abs(tab: Map[Int, Int], size: Int): Map[Int, Int] = ({
+    require(size <= 5 && isArray(tab, size))
+    var k = 0
+    var tabres = Map.empty[Int, Int]
+    (while(k < size) {
+      if(tab(k) < 0)
+        tabres = tabres.updated(k, -tab(k))
+      else
+        tabres = tabres.updated(k, tab(k))
+      k = k + 1
+    }) invariant(isArray(tabres, k) && k >= 0 && k <= size && isPositive(tabres, k))
+    tabres
+  }) ensuring(res => isArray(res, size) && isPositive(res, size))
+
+  def isPositive(a: Map[Int, Int], size: Int): Boolean = {
+    require(size <= 10 && isArray(a, size))
+    def rec(i: Int): Boolean = {
+      require(i >= 0)
+      if(i >= size) 
+        true 
+      else {
+        if(a(i) < 0) 
+          false 
+        else 
+          rec(i+1)
+      }
+    }
+    rec(0)
+  }
+
+  def isArray(a: Map[Int, Int], size: Int): Boolean = {
+
+    def rec(i: Int): Boolean = {
+      require(i >= 0)  
+      if(i >= size) true else {
+        if(a.isDefinedAt(i)) rec(i+1) else false
+      }
+    }
+
+    if(size < 0)
+      false
+    else
+      rec(0)
+  }
+
+}