diff --git a/src/test/resources/regression/termination/looping/LambdaCalculus.scala b/src/test/resources/regression/termination/looping/LambdaCalculus.scala
new file mode 100644
index 0000000000000000000000000000000000000000..16e10bb622b74b15c2da098de1c706603d2a6465
--- /dev/null
+++ b/src/test/resources/regression/termination/looping/LambdaCalculus.scala
@@ -0,0 +1,51 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object LambdaCalculus {
+ abstract class Term
+ case class Var(x: BigInt) extends Term
+ case class Abs(x: BigInt, body: Term) extends Term
+ case class App(func: Term, arg: Term) extends Term
+
+ def fv(t: Term): Set[BigInt] = t match {
+ case Var(x) => Set(x)
+ case Abs(x, body) => fv(body) ++ Set(x)
+ case App(func, arg) => fv(func) ++ fv(arg)
+ }
+
+ // [x->u]t
+ def subst(x: BigInt, u: Term, t: Term): Term = t match {
+ case Var(y) => if (x == y) u else t
+ case Abs(y, body) => if (x == y) t else Abs(y, subst(x, u, body))
+ case App(f, a) => App(subst(x, u, f), subst(x, u, a))
+ }
+
+ /* Termination checker (LoopProcessor) says:
+ ✗ Non-terminating for call: 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))
+ case None() => None()
+ }
+ case _ => None() // stuck
+ }
+ case _ => Some(t) // Abs or Var, already a value
+ }) ensuring { res => res match {
+ case Some(t) => isValue(t)
+ case None() => true
+ }}
+
+ def isValue(t: Term): Boolean = t match {
+ case Var(x) => true
+ case Abs(x, body) => true
+ case App(f, a) => false
+ }
+
+}
diff --git a/src/test/resources/regression/termination/looping/OddEven.scala b/src/test/resources/regression/termination/looping/OddEven.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e26e455557ee19342183853ece4997809565fa29
--- /dev/null
+++ b/src/test/resources/regression/termination/looping/OddEven.scala
@@ -0,0 +1,13 @@
+
+object Test {
+
+ def isOdd(n: BigInt): Boolean = {
+ isEven(n-1)
+ } ensuring { res => (n % 2 == 1) == res }
+
+ def isEven(n: BigInt): Boolean = {
+ isOdd(n-1)
+ } ensuring { res => (n % 2 == 0) == res }
+
+
+}
\ No newline at end of file
diff --git a/src/test/resources/regression/termination/looping/UniversalEquality.scala b/src/test/resources/regression/termination/looping/UniversalEquality.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fbfd76d2759a85c29997635e6933197b55b29a74
--- /dev/null
+++ b/src/test/resources/regression/termination/looping/UniversalEquality.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object test {
+
+ def universalEquality(e1: BigInt, e2: BigInt): Boolean = {
+ val b = proveEquality(e1, e2)
+ e1 == e2
+ }.holds
+
+ def proveEquality(a: BigInt, b: BigInt): Boolean = {
+ 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
new file mode 100644
index 0000000000000000000000000000000000000000..2b53eaaef8a61bb4673a61bf07c872791cf541ec
--- /dev/null
+++ b/src/test/resources/regression/termination/looping/WrongFibonacci.scala
@@ -0,0 +1,8 @@
+
+object Test {
+
+ def fib(n: BigInt): BigInt = {
+ fib(n-1) + fib(n-2)
+ } ensuring {res => res == (5*n + 1)*(5*n - 1)}
+
+}
diff --git a/src/test/resources/regression/termination/valid/CountTowardsZero.scala b/src/test/resources/regression/termination/valid/CountTowardsZero.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4ef5ba8b07ccbe508c4a88945f9ccf7faaf5231d
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/CountTowardsZero.scala
@@ -0,0 +1,14 @@
+
+object Test {
+ def f(x: BigInt): BigInt = {
+ if (x == 0) {
+ 0
+ } else if (x > 0) {
+ f(x-1)+2
+ } else if (x < 0) {
+ f(x+1)-2
+ } else {
+ 33
+ }
+ } ensuring (_ == x*2)
+}
diff --git a/testcases/termination/pending/McCarthy91.scala b/testcases/termination/pending/McCarthy91.scala
new file mode 100644
index 0000000000000000000000000000000000000000..66a15d68fe20906c7ca3209810ac28ddff2eeb5f
--- /dev/null
+++ b/testcases/termination/pending/McCarthy91.scala
@@ -0,0 +1,10 @@
+
+/*
+This function terminates for all inputs, see
+http://en.wikipedia.org/wiki/McCarthy_91_function
+
+But the termination checker returns NoGuarantee after 75s.
+*/
+object McCarthy91 {
+ def M(n: BigInt): BigInt = if (n > 100) n-10 else M(M(n+11))
+}
diff --git a/testcases/termination/pending/lambdaDot.scala b/testcases/termination/pending/lambdaDot.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d3ea7ab54ed0057ae6346a9c631fc1325ee99ee0
--- /dev/null
+++ b/testcases/termination/pending/lambdaDot.scala
@@ -0,0 +1,112 @@
+/*
+A very much simplified implementation of the types in the
+Dependent Object Calculus (http://lampwww.epfl.ch/~amin/dot/fool.pdf).
+
+It's interesting because expansion calls itself recursively (through
+lookupInVar), and passes the results of this recursive call to another
+recursive call.
+
+The termination checker loops forever [or at least longer than several
+minutes ;-)] on this case.
+*/
+
+import leon.lang._
+import leon.collection._
+import leon._
+
+object lambdaDot {
+ abstract class Label
+ case class TypLabel(id: BigInt) extends Label
+ case class MtdLabel(id: BigInt) extends Label
+
+ abstract class Type
+ case class Top() extends Type
+ case class Bot() extends Type
+ case class Rcd(ds: List[Dec]) extends Type
+ case class TSel(x: BigInt, l: BigInt) extends Type
+
+ abstract class Dec {
+ def label: Label = this match {
+ case TDec(l, _, _) => TypLabel(l)
+ case MDec(m, _, _) => MtdLabel(m)
+ }
+ }
+ case class TDec(l: BigInt, lowerBound: Type, upperBound: Type) extends Dec
+ case class MDec(m: BigInt, argType: Type, retType: Type) extends Dec
+
+ abstract class Decs
+ case class FiniteDecs(l: List[Dec]) extends Decs
+ case class BotDecs() extends Decs
+
+ def lookupInEnv(x: BigInt, env: List[(BigInt, Type)]): Option[Type] = env match {
+ case Cons((y, t), rest) => if (x == y) Some(t) else lookupInEnv(x, rest)
+ case Nil() => None()
+ }
+
+ def lookupInDecList(name: Label, l: List[Dec]): Option[Dec] = (l match {
+ case Cons(d, ds) => if (d.label == name) Some(d) else lookupInDecList(name, ds)
+ case Nil() => None()
+ }) ensuring { res => res match {
+ case Some(d) => d.label == name
+ case None() => true
+ }}
+
+ def lookupInDecs(name: Label, l: Decs): Option[Dec] = (l match {
+ case FiniteDecs(l) => lookupInDecList(name, l)
+ case BotDecs() => name match {
+ case TypLabel(l) => Some(TDec(l, Top(), Bot()))
+ case MtdLabel(m) => Some(MDec(m, Top(), Bot()))
+ }
+ }) ensuring { res => res match {
+ case Some(d) => d.label == name
+ case None() => true
+ }}
+
+ def wfType(env: List[(BigInt, Type)], t: Type, shallow: Boolean): Boolean = t match {
+ case Top() => true
+ case Bot() => true
+ case Rcd(ds) => shallow || wfDecList(env, ds)
+ case TSel(x, l) => lookupInVar(env, x, TypLabel(l)) match {
+ case Some(TDec(l, lo, hi)) => wfType(env, lo, true) && wfType(env, hi, true)
+ case None() => false
+ }
+ }
+
+ def wfDec(env: List[(BigInt, Type)], d: Dec): Boolean = d match {
+ case TDec(l, lo, hi) => wfType(env, lo, false) && wfType(env, hi, false)
+ case MDec(m, a, r) => wfType(env, a, false) && wfType(env, r, false)
+ }
+
+ def wfDecList(env: List[(BigInt, Type)], ds: List[Dec]): Boolean = ds match {
+ case Cons(d, ds) => wfDec(env, d) && wfDecList(env, ds)
+ case Nil() => true
+ }
+
+ def expansion(env: List[(BigInt, Type)], t: Type): Option[Decs] = {
+ //require(wfType(env, t, false))
+ t match {
+ case Top() => Some(FiniteDecs(Nil()))
+ case Bot() => Some(FiniteDecs(Nil()))
+ case Rcd(ds) => Some(FiniteDecs(ds))
+ case TSel(x, l) => lookupInVar(env, x, TypLabel(l)) match {
+ case Some(TDec(l, lo, hi)) => expansion(env, hi)
+ case None() => None()
+ }
+ }
+ }
+
+ def lookupInVar(env: List[(BigInt, Type)], x: BigInt, l: Label): Option[Dec] = {
+ lookupInEnv(x, env) match {
+ case Some(tx) => expansion(env, tx) match {
+ case Some(dsx) => lookupInDecs(l, dsx)
+ case None() => None()
+ }
+ case None() => None()
+ }
+ } ensuring { res => res match {
+ case Some(d) => d.label == l
+ case None() => true
+ }}
+
+}
+