Fixed regression test failures due to removal of bodiless methods and functions.

1 files changed, 3 insertions, 0 deletions

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);