Added a coinductive/inductive Filter example to the test suite

1 files changed, 3 insertions, 3 deletions

diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy
index 2f8c2a9e..8709a6d8 100644
--- a/Test/dafny3/InductionVsCoinduction.dfy
+++ b/Test/dafny3/InductionVsCoinduction.dfy
@@ -25,7 +25,7 @@ function Up(n: int): Stream<int>
  */

 

 function FivesUp(n: int): Stream<int>

-  decreases (n + 4) / 5 * 5 - n;

+  decreases 4 - (n-1) % 5;

 {

   if n % 5 == 0 then SCons(n, FivesUp(n+1))

   else FivesUp(n+1)

@@ -113,7 +113,7 @@ comethod UpPos_Auto(n:int)
 comethod {:induction false} FivesUpPos(n:int)

   requires n > 0;

   ensures Pos(FivesUp(n));

-  decreases (n + 4) / 5 * 5 - n;

+  decreases 4 - (n-1) % 5;

 {

   if (n % 5 == 0) {

     FivesUpPos#[_k - 1](n + 1);

@@ -127,7 +127,7 @@ comethod {:induction false} FivesUpPos(n:int)
 comethod FivesUpPos_Auto(n:int)

   requires n > 0;

   ensures Pos(FivesUp(n));

-  decreases (n + 4) / 5 * 5 - n;

+  decreases 4 - (n-1) % 5;

 {

 }