Fixed some checking of recursive method/copredicate calls

1 files changed, 4 insertions, 4 deletions

diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy
index a7111a09..bf224f25 100644
--- a/Test/dafny0/CoResolution.dfy
+++ b/Test/dafny0/CoResolution.dfy
@@ -109,13 +109,13 @@ module CallGraph {
 

   copredicate Q(n: nat)

   {

-    calc { 87; { CoLemma(n); } }

+    calc { 87; { CoLemma(n); } }  // error: this recursive call not allowed

     false

   }

 

   copredicate R(n: nat)

   {

-    calc { 87; { CoLemma#[n](n); } }

+    calc { 87; { CoLemma#[n](n); } }  // error: this recursive call not allowed

     false

   }

 

@@ -129,13 +129,13 @@ module CallGraph {
 

   copredicate Q_D(n: nat)

   {

-    calc { 88; { CoLemma_D(n); } }

+    calc { 88; { CoLemma_D(n); } }  // error: this recursive call not allowed

     false

   }

 

   copredicate R_D(n: nat)

   {

-    calc { 89; { CoLemma_D#[n](n); } }

+    calc { 89; { CoLemma_D#[n](n); } }  // error: this recursive call not allowed

     false

   }