Refactored code for dealing with SCCs in the call graph.

Fixed bug.

1 files changed, 41 insertions, 0 deletions

diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy
index d8eb296d..e22bbf84 100644
--- a/Test/dafny0/Corecursion.dfy
+++ b/Test/dafny0/Corecursion.dfy
@@ -124,3 +124,44 @@ module MixRecursiveAndCorecursive {
     X(n-1)

   }

 }

+

+// --------------------------------------------------

+

+module FunctionSCCsWithMethods {

+  codatatype Stream<T> = Cons(head: T, tail: Stream)

+

+  lemma M(n: nat)

+    decreases n, 0;

+  {

+    if n != 0 {

+      var p := Cons(10, F(n-1));

+    }

+  }

+

+  function F(n: nat): Stream<int>

+    decreases n;

+  {

+    M(n);

+    // the following call to F is not considered co-recursive, because the SCC contains a method

+    Cons(5, F(n))  // error: cannot prove termination

+  }

+

+  function G(): Stream<int>

+  {

+    Lemma();

+    H()

+  }

+

+  function H(): Stream<int>

+    decreases 0;

+  {

+    // the following call to G is not considered co-recursive, because the SCC contains a method

+    Cons(5, G())  // error: cannot prove termination

+  }

+

+  lemma Lemma()

+    decreases 1;

+  {

+    var h := H();

+  }

+}