From 47c23bd0d7e71722a94b8df660c0314381b4263a Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Fri, 15 Jul 2011 17:42:55 -0700
Subject: Fixed regression test failures due to removal of bodiless methods and
 functions.

---
 Test/dafny1/UltraFilter.dfy | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'Test/dafny1/UltraFilter.dfy')

diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index c8419890..0dfb6683 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -31,6 +31,9 @@ class UltraFilter<G> {
   // Dafny currently does not have a set comprehension expression, so this method stub will have to do
   method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>)
     ensures (forall X :: X in h <==> M + X in f);
+  {
+    assume false;
+  }
 
   method Lemma_HIsFilter(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
     requires IsFilter(f, S);
-- 
cgit v1.2.3