From e2f9a3153a2e80c055f9a6d1a2abf8ba9c787009 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Sun, 23 Feb 2014 22:06:56 -0800
Subject: Added another colemma-calls-function-recursively test

---
 Test/dafny0/Answer           |  3 ++-
 Test/dafny0/CoResolution.dfy | 10 ++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 78d6c126..7b546c36 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1404,7 +1404,8 @@ CoResolution.dfy(132,17): Error: a recursive call from a copredicate can go only
 CoResolution.dfy(138,17): Error: a recursive call from a copredicate can go only to other copredicates
 CoResolution.dfy(146,4): Error: a recursive call from a copredicate can go only to other copredicates
 CoResolution.dfy(148,4): Error: a recursive call from a copredicate can go only to other copredicates
-20 resolution/type errors detected in CoResolution.dfy
+CoResolution.dfy(164,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+21 resolution/type errors detected in CoResolution.dfy
 
 -------------------- CoPrefix.dfy --------------------
 CoPrefix.dfy(161,3): Error BP5003: A postcondition might not hold on this return path.
diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy
index bf224f25..1219db90 100644
--- a/Test/dafny0/CoResolution.dfy
+++ b/Test/dafny0/CoResolution.dfy
@@ -158,4 +158,14 @@ module CallGraph {
     calc { true; { assert P#[n](n); } }
     101
   }
+
+  colemma J()
+  {
+    var f := JF();  // error: cannot call non-colemma recursively from colemma
+  }
+  function JF(): int
+  {
+    J();
+    5
+  }
 }
-- 
cgit v1.2.3