From cdb0a97bc55194c6d9fb3e49fcc45aeb602e2536 Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Wed, 11 Jul 2012 11:55:49 -0700
Subject: Dafny: added a copredicate test case

---
 Test/dafny0/Answer           |  8 ++++----
 Test/dafny0/CoPredicates.dfy | 10 ++++++++++
 2 files changed, 14 insertions(+), 4 deletions(-)

(limited to 'Test')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 6b7a1079..258f67e0 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1290,13 +1290,13 @@ Execution trace:
 Dafny program verifier finished with 5 verified, 2 errors
 
 -------------------- CoPredicates.dfy --------------------
-CoPredicates.dfy(35,1): Error BP5003: A postcondition might not hold on this return path.
-CoPredicates.dfy(34,11): Related location: This is the postcondition that might not hold.
-CoPredicates.dfy(20,22): Related location: Related location
+CoPredicates.dfy(45,1): Error BP5003: A postcondition might not hold on this return path.
+CoPredicates.dfy(44,11): Related location: This is the postcondition that might not hold.
+CoPredicates.dfy(30,22): Related location: Related location
 Execution trace:
     (0,0): anon0
 
-Dafny program verifier finished with 11 verified, 1 error
+Dafny program verifier finished with 14 verified, 1 error
 
 -------------------- TypeAntecedents.dfy --------------------
 TypeAntecedents.dfy(32,13): Error: assertion violation
diff --git a/Test/dafny0/CoPredicates.dfy b/Test/dafny0/CoPredicates.dfy
index b4da4792..67dff91b 100644
--- a/Test/dafny0/CoPredicates.dfy
+++ b/Test/dafny0/CoPredicates.dfy
@@ -10,6 +10,16 @@ copredicate Pos(s: Stream<int>)
   0 < s.head && Pos(s.tail)
 }
 
+copredicate X(s: Stream)
+{
+  X(s)
+}
+
+ghost method AlwaysLemma(s: Stream)
+  ensures X(s);
+{
+}
+
 function Doubles(n: int): Stream<int>
 {
   Cons(2*n, Doubles(n + 1))
-- 
cgit v1.2.3