From 9447617aefbe9706b0d74a827181976e4b9e9d26 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Thu, 17 Dec 2009 01:17:59 +0000
Subject: Allow ":" in addition to "returns" in function definitions. Make the
 pretty-printer use ":" not "returns". Allow foo(x,y,z:int,p,q:ptr) kind of
 syntax in function definitions. Consequently foo(int,y:bool) is no longer
 allowed. Update the testsuite to match that.

---
 Test/test21/InterestingExamples4.bpl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Test/test21/InterestingExamples4.bpl')

diff --git a/Test/test21/InterestingExamples4.bpl b/Test/test21/InterestingExamples4.bpl
index 371724f5..67636af1 100644
--- a/Test/test21/InterestingExamples4.bpl
+++ b/Test/test21/InterestingExamples4.bpl
@@ -14,7 +14,7 @@ axiom (forall<a,b> x:a, y:b :: sameType(x,y) == (exists z:a :: y==z));
 // b = C^n(a)
 function rel<a,b>(x:a, y:b) returns (bool);
 
-function relHelp<a,b>(x:a, y:b, int) returns (bool);
+function relHelp<a,b>(x:a, y:b, z:int) returns (bool);
 
 axiom (forall<a, b> x:a, y:b :: relHelp(x, y, 0) == sameType(x, y));
 axiom (forall<a, b> n:int, x:a, y:b ::
-- 
cgit v1.2.3