From e7fc963667a6cfbf9f8516f49ea1dcb9d6779f2d Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 20 May 2010 08:15:06 +0000
Subject: fixed guard check with commutative cuts

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13022 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/complexity/guard.v | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/complexity/guard.v b/test-suite/complexity/guard.v
index 387263e2f3..ceb7835a6b 100644
--- a/test-suite/complexity/guard.v
+++ b/test-suite/complexity/guard.v
@@ -1,4 +1,4 @@
-(* Examples to check that the guard condition does not unfold
+(* Examples to check that the guard condition does not evaluate
    irrelevant subterms *)
 (* Expected time < 1.00s *)
 Require Import Bool.
@@ -15,3 +15,16 @@ Timeout 5 Time Fixpoint F n :=
   | S k =>
     if slow 100 then F k else 0
   end.
+
+Fixpoint slow2 n :=
+ match n with
+ | 0 => 0
+ | S k => slow2 k + slow2 k
+ end.
+
+Timeout 5 Time Fixpoint F' n :=
+  match n with
+  | 0 => 0
+  | S k =>
+    if slow2 100 then F' k else 0
+  end.
-- 
cgit v1.2.3