From 1e156f9e83cb5ace0f74330f2aa49f8ce09d0afe Mon Sep 17 00:00:00 2001 From: rustanleino Date: Tue, 8 Jun 2010 20:09:12 +0000 Subject: Dafny: Fix type bug in SplitExpr translation. --- Test/dafny1/Celebrity.dfy | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'Test/dafny1') diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index fd267c71..eed06bb1 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -72,8 +72,7 @@ method FindCelebrity2(people: set, ghost c: Person) returns (r: method FindCelebrity3(n: int, people: set, ghost c: int) returns (r: int) requires 0 < n; requires (forall p :: p in people <==> 0 <= p && p < n); - // requires IsCelebrity(c, people); // see next line: - requires c in people && (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p)); // hack to work around bug in Dafny-to-Boogie translator + requires IsCelebrity(c, people); ensures r == c; { r := 0; -- cgit v1.2.3