From 871fe2f73e0b9f987d39569087b5ba3d928df92f Mon Sep 17 00:00:00 2001
From: Sandro Stucki <sandro.stucki@gmail.com>
Date: Wed, 19 Aug 2015 09:17:04 +0200
Subject: [PATCH] Adds test case illustrating non-wellfoundedness issues with
proofs.
---
.../verification/proof/NotWellFounded.scala | 22 +++++++++++++++++++
1 file changed, 22 insertions(+)
create mode 100644 testcases/verification/proof/NotWellFounded.scala
diff --git a/testcases/verification/proof/NotWellFounded.scala b/testcases/verification/proof/NotWellFounded.scala
new file mode 100644
index 000000000..f97c16e1b
--- /dev/null
+++ b/testcases/verification/proof/NotWellFounded.scala
@@ -0,0 +1,22 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.testcases.verification.proof
+
+import leon.collection._
+import leon.lang._
+import leon.proof._
+
+object NotWellFounded {
+
+ // This proof is not well-founded. Since Leon doesn't run the
+ // termination checker by default, it will accept the proof as
+ // valid.
+ def allListsAreEmpty[T](xs: List[T]): Boolean = {
+ xs.isEmpty because {
+ xs match {
+ case Nil() => trivial
+ case Cons(x, xs) => allListsAreEmpty(x :: xs)
+ }
+ }
+ }.holds
+}
--
GitLab