3 files changed, 59 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 7879483d..e1ab158f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1289,6 +1289,15 @@ 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
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 11 verified, 1 error
+
 -------------------- TypeAntecedents.dfy --------------------
 TypeAntecedents.dfy(32,13): Error: assertion violation
 Execution trace:
diff --git a/Test/dafny0/CoPredicates.dfy b/Test/dafny0/CoPredicates.dfy
new file mode 100644
index 00000000..b4da4792
--- /dev/null
+++ b/Test/dafny0/CoPredicates.dfy
@@ -0,0 +1,48 @@
+codatatype Stream<T> = Cons(head: T, tail: Stream);
+
+function Upward(n: int): Stream<int>
+{
+  Cons(n, Upward(n + 1))
+}
+
+copredicate Pos(s: Stream<int>)
+{
+  0 < s.head && Pos(s.tail)
+}
+
+function Doubles(n: int): Stream<int>
+{
+  Cons(2*n, Doubles(n + 1))
+}
+
+copredicate Even(s: Stream<int>)
+{
+  s.head % 2 == 0 && Even(s.tail)
+}
+
+ghost method Lemma0(n: int)
+  ensures Even(Doubles(n));
+{
+}
+
+function UpwardBy2(n: int): Stream<int>
+{
+  Cons(n, UpwardBy2(n + 2))
+}
+
+ghost method Lemma1(n: int)
+  ensures Even(UpwardBy2(2*n));  // error:  this is true, but Dafny can't prove it
+{
+}
+
+function U2(n: int): Stream<int>
+  requires n % 2 == 0;
+{
+  UpwardBy2(n)
+}
+
+ghost method Lemma2(n: int)
+  ensures Even(UpwardBy2(2*n));  // this is true, but Dafny can't prove it
+{
+  assert Even(U2(2*n));  // ... thanks to this lemma
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index d352cf44..60b544c7 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -16,7 +16,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             ModulesCycle.dfy Modules0.dfy Modules1.dfy BadFunction.dfy
             Comprehensions.dfy Basics.dfy ControlStructures.dfy
             Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy
-            TypeParameters.dfy Datatypes.dfy Coinductive.dfy Corecursion.dfy
+            TypeParameters.dfy Datatypes.dfy
+            Coinductive.dfy Corecursion.dfy CoPredicates.dfy
             TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy
             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy
             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy