diff --git a/src/test/resources/regression/termination/looping/LambdaCalculus.scala b/src/test/resources/regression/termination/looping/LambdaCalculus.scala
index 16e10bb622b74b15c2da098de1c706603d2a6465..884e5dee5564e90eb9b97210e000a30418ea22f8 100644
--- a/src/test/resources/regression/termination/looping/LambdaCalculus.scala
+++ b/src/test/resources/regression/termination/looping/LambdaCalculus.scala
@@ -22,16 +22,16 @@ object LambdaCalculus {
   }
   
   /* Termination checker (LoopProcessor) says:
-  ✗ Non-terminating for call: eval(App(Abs(0, App(Var(0), Var(0))), Abs(0, App(Var(0), Var(0)))))
+  ✗ Non-terminating for call: looping_eval(App(Abs(0, App(Var(0), Var(0))), Abs(0, App(Var(0), Var(0)))))
   i.e.
   (λx. x x)(λx. x x)
   This is the well-known "omega".
   */
-  // big step call-by-value evaluation
-  def eval(t: Term): Option[Term] = (t match {
-    case App(t1, t2) => eval(t1) match {
-      case Some(Abs(x, body)) => eval(t2) match {
-        case Some(v2) => eval(subst(x, v2, body))
+  // big step call-by-value looping_evaluation
+  def looping_eval(t: Term): Option[Term] = (t match {
+    case App(t1, t2) => looping_eval(t1) match {
+      case Some(Abs(x, body)) => looping_eval(t2) match {
+        case Some(v2) => looping_eval(subst(x, v2, body))
         case None() => None()
       }
       case _ => None() // stuck
diff --git a/src/test/resources/regression/termination/looping/OddEven.scala b/src/test/resources/regression/termination/looping/OddEven.scala
index e26e455557ee19342183853ece4997809565fa29..078b4c25834c8fc3a348f71771d6c21deb9698c1 100644
--- a/src/test/resources/regression/termination/looping/OddEven.scala
+++ b/src/test/resources/regression/termination/looping/OddEven.scala
@@ -1,12 +1,12 @@
 
 object Test {
 
-  def isOdd(n: BigInt): Boolean = {
-    isEven(n-1)
+  def looping_isOdd(n: BigInt): Boolean = {
+    looping_isEven(n-1)
   } ensuring { res => (n % 2 == 1) == res }
   
-  def isEven(n: BigInt): Boolean = {
-    isOdd(n-1)
+  def looping_isEven(n: BigInt): Boolean = {
+    looping_isOdd(n-1)
   } ensuring { res => (n % 2 == 0) == res }
   
   
diff --git a/src/test/resources/regression/termination/looping/UniversalEquality.scala b/src/test/resources/regression/termination/looping/UniversalEquality.scala
index fbfd76d2759a85c29997635e6933197b55b29a74..7b7181a6f3d90105d2a1c93603d86e32e025cdc5 100644
--- a/src/test/resources/regression/termination/looping/UniversalEquality.scala
+++ b/src/test/resources/regression/termination/looping/UniversalEquality.scala
@@ -5,12 +5,12 @@ import leon._
 object test {
   
   def universalEquality(e1: BigInt, e2: BigInt): Boolean = {
-    val b = proveEquality(e1, e2)
+    val b = looping_proveEquality(e1, e2)
     e1 == e2
   }.holds
   
-  def proveEquality(a: BigInt, b: BigInt): Boolean = {
-    proveEquality(a, b)
+  def looping_proveEquality(a: BigInt, b: BigInt): Boolean = {
+    looping_proveEquality(a, b)
   } ensuring { res => res == (a == b) && res }
 
 }
diff --git a/src/test/resources/regression/termination/looping/WrongFibonacci.scala b/src/test/resources/regression/termination/looping/WrongFibonacci.scala
index 2b53eaaef8a61bb4673a61bf07c872791cf541ec..9911ee76dcdd83878b19a042bb9db44737848fb9 100644
--- a/src/test/resources/regression/termination/looping/WrongFibonacci.scala
+++ b/src/test/resources/regression/termination/looping/WrongFibonacci.scala
@@ -1,8 +1,8 @@
 
 object Test {
   
-  def fib(n: BigInt): BigInt = {
-    fib(n-1) + fib(n-2)
+  def looping_fib(n: BigInt): BigInt = {
+    looping_fib(n-1) + looping_fib(n-2)
   } ensuring {res => res == (5*n + 1)*(5*n - 1)}
   
 }