2 files changed, 50 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 7b546c36..1521376e 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1380,8 +1380,16 @@ Execution trace:
     (0,0): anon0
     (0,0): anon5_Else
     (0,0): anon6_Then
+Corecursion.dfy(146,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Else
+Corecursion.dfy(159,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Else
 
-Dafny program verifier finished with 10 verified, 6 errors
+Dafny program verifier finished with 15 verified, 8 errors
 
 -------------------- CoResolution.dfy --------------------
 CoResolution.dfy(14,9): Error: member Undeclared# does not exist in class _default
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();
+  }
+}