Fixed bugs in co-call checks

1 files changed, 16 insertions, 0 deletions

diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy
index 1219db90..14da4493 100644
--- a/Test/dafny0/CoResolution.dfy
+++ b/Test/dafny0/CoResolution.dfy
@@ -169,3 +169,19 @@ module CallGraph {
     5

   }

 }

+

+module CrashRegression {

+  codatatype Stream<T> = Cons(T, Stream)

+

+  // The following functions (where A ends up being the representative in the

+  // SCC and B, which is also in the same SCC, has no body) once crashed the

+  // resolver.

+  function A(): Stream

+  {

+    B()

+  }

+  function B(): Stream

+    ensures A() == S();

+

+  function S(): Stream

+}