Boogie:

* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it).
* Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it).

Dafny:
* Split off some tests from Test/dafny0 into Test/dafny1.
* Added Test/dafny1/UltraFilter.dfy.

19 files changed, 437 insertions, 308 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index e1b83c87..0c152d6e 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -64,10 +64,6 @@ class C {
 

 Dafny program verifier finished with 0 verified, 0 errors

 

--------------------- BQueue.bpl --------------------

-

-Boogie program verifier finished with 8 verified, 0 errors

-

 -------------------- TypeTests.dfy --------------------

 TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)

 TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)

@@ -338,30 +334,6 @@ Execution trace:
 

 Dafny program verifier finished with 2 verified, 1 error

 

--------------------- Queue.dfy --------------------

-

-Dafny program verifier finished with 22 verified, 0 errors

-

--------------------- ListCopy.dfy --------------------

-

-Dafny program verifier finished with 4 verified, 0 errors

-

--------------------- BinaryTree.dfy --------------------

-

-Dafny program verifier finished with 24 verified, 0 errors

-

--------------------- ListReverse.dfy --------------------

-

-Dafny program verifier finished with 2 verified, 0 errors

-

--------------------- ListContents.dfy --------------------

-

-Dafny program verifier finished with 9 verified, 0 errors

-

--------------------- SchorrWaite.dfy --------------------

-

-Dafny program verifier finished with 10 verified, 0 errors

-

 -------------------- Termination.dfy --------------------

 

 Dafny program verifier finished with 13 verified, 0 errors

@@ -423,27 +395,3 @@ Dafny program verifier finished with 24 verified, 2 errors
 -------------------- Datatypes.dfy --------------------

 

 Dafny program verifier finished with 10 verified, 0 errors

-

--------------------- UnboundedStack.dfy --------------------

-

-Dafny program verifier finished with 12 verified, 0 errors

-

--------------------- SumOfCubes.dfy --------------------

-

-Dafny program verifier finished with 17 verified, 0 errors

-

--------------------- TerminationDemos.dfy --------------------

-

-Dafny program verifier finished with 10 verified, 0 errors

-

--------------------- Substitution.dfy --------------------

-

-Dafny program verifier finished with 12 verified, 0 errors

-

--------------------- Tree.dfy --------------------

-

-Dafny program verifier finished with 6 verified, 0 errors

-

--------------------- Celebrity.dfy --------------------

-

-Dafny program verifier finished with 11 verified, 0 errors

diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
deleted file mode 100644
index 8b4892dd..00000000
--- a/Test/dafny0/BinaryTree.dfy
+++ /dev/null
@@ -1,244 +0,0 @@
-class IntSet {

-  ghost var contents: set<int>;

-  ghost var footprint: set<object>;

-

-  var root: Node;

-

-  function Valid(): bool

-    reads this, footprint;

-  {

-    this in footprint &&

-    (root == null ==> contents == {}) &&

-    (root != null ==>

-       root in footprint && root.footprint <= footprint && this !in root.footprint &&

-       root.Valid() &&

-       contents == root.contents)

-  }

-

-  method Init()

-    modifies this;

-    ensures Valid() && fresh(footprint - {this});

-    ensures contents == {};

-  {

-    root := null;

-    footprint := {this};

-    contents := {};

-  }

-

-  method Find(x: int) returns (present: bool)

-    requires Valid();

-    ensures present <==> x in contents;

-  {

-    if (root == null) {

-      present := false;

-    } else {

-      call present := root.Find(x);

-    }

-  }

-

-  method Insert(x: int)

-    requires Valid();

-    modifies footprint;

-    ensures Valid() && fresh(footprint - old(footprint));

-    ensures contents == old(contents) + {x};

-  { 

-    call t := InsertHelper(x, root);

-    root := t;

-    contents := root.contents;

-    footprint := root.footprint + {this};

-  }

-

-  static method InsertHelper(x: int, n: Node) returns (m: Node)

-    requires n == null || n.Valid();

-    modifies n.footprint;

-    ensures m != null && m.Valid();

-    ensures n == null ==> fresh(m.footprint) && m.contents == {x};

-    ensures n != null ==> m == n && n.contents == old(n.contents) + {x};

-    ensures n != null ==> fresh(n.footprint - old(n.footprint));

-    decreases if n == null then {} else n.footprint;

-  {

-    if (n == null) {

-      m := new Node;

-      call m.Init(x);

-    } else if (x == n.data) {

-      m := n;

-    } else {

-      if (x < n.data) {

-        assert n.right == null || n.right.Valid();

-        call t := InsertHelper(x, n.left);

-        n.left := t;

-        n.footprint := n.footprint + n.left.footprint;

-      } else {

-        assert n.left == null || n.left.Valid();

-        call t := InsertHelper(x, n.right);

-        n.right := t;

-        n.footprint := n.footprint + n.right.footprint;

-      }

-      n.contents := n.contents + {x};

-      m := n;

-    }

-  }

-

-  method Remove(x: int)

-    requires Valid();

-    modifies footprint;

-    ensures Valid() && fresh(footprint - old(footprint));

-    ensures contents == old(contents) - {x};

-  {

-    if (root != null) {

-      call newRoot := root.Remove(x);

-      root := newRoot;

-      if (root == null) {

-        contents := {};

-        footprint := {this};

-      } else {

-        contents := root.contents;

-        footprint := root.footprint + {this};

-      }

-    }

-  }

-}

-

-class Node {

-  ghost var contents: set<int>;

-  ghost var footprint: set<object>;

-

-  var data: int;

-  var left: Node;

-  var right: Node;

-

-  function Valid(): bool

-    reads this, footprint;

-  {

-    this in footprint &&

-    null !in footprint &&

-    (left != null ==>

-      left in footprint &&

-      left.footprint <= footprint && this !in left.footprint &&

-      left.Valid() &&

-      (forall y :: y in left.contents ==> y < data)) &&

-    (right != null ==>

-      right in footprint &&

-      right.footprint <= footprint && this !in right.footprint &&

-      right.Valid() &&

-      (forall y :: y in right.contents ==> data < y)) &&

-    (left == null && right == null ==>

-      contents == {data}) &&

-    (left != null && right == null ==>

-      contents == left.contents + {data}) &&

-    (left == null && right != null ==>

-      contents == {data} + right.contents) &&

-    (left != null && right != null ==>

-      left.footprint !! right.footprint &&

-      contents == left.contents + {data} + right.contents)

-  }

-

-  method Init(x: int)

-    modifies this;

-    ensures Valid() && fresh(footprint - {this});

-    ensures contents == {x};

-  {

-    data := x;

-    left := null;

-    right := null;

-    contents := {x};

-    footprint := {this};

-  }

-

-  method Find(x: int) returns (present: bool)

-    requires Valid();

-    ensures present <==> x in contents;

-    decreases footprint;

-  {

-    if (x == data) {

-      present := true;

-    } else if (left != null && x < data) {

-      call present := left.Find(x);

-    } else if (right != null && data < x) {

-      call present := right.Find(x);

-    } else {

-      present := false;

-    }

-  }

-

-  method Remove(x: int) returns (node: Node)

-    requires Valid();

-    modifies footprint;

-    ensures fresh(footprint - old(footprint));

-    ensures node != null ==> node.Valid();

-    ensures node == null ==> old(contents) <= {x};

-    ensures node != null ==> node.footprint <= footprint && node.contents == old(contents) - {x};

-    decreases footprint;

-  {

-    node := this;

-    if (left != null && x < data) {

-      call t := left.Remove(x);

-      left := t;

-      contents := contents - {x};

-      if (left != null) { footprint := footprint + left.footprint; }

-    } else if (right != null && data < x) {

-      call t := right.Remove(x);

-      right := t;

-      contents := contents - {x};

-      if (right != null) { footprint := footprint + right.footprint; }

-    } else if (x == data) {

-      if (left == null && right == null) {

-        node := null;

-      } else if (left == null) {

-        node := right;

-      } else if (right == null) {

-        node := left;

-      } else {

-        // rotate

-        call min, r := right.RemoveMin();

-        data := min;  right := r;

-        contents := contents - {x};

-        if (right != null) { footprint := footprint + right.footprint; }

-      }

-    }

-  }

-

-  method RemoveMin() returns (min: int, node: Node)

-    requires Valid();

-    modifies footprint;

-    ensures fresh(footprint - old(footprint));

-    ensures node != null ==> node.Valid();

-    ensures node == null ==> old(contents) == {min};

-    ensures node != null ==> node.footprint <= footprint && node.contents == old(contents) - {min};

-    ensures min in old(contents) && (forall x :: x in old(contents) ==> min <= x);

-    decreases footprint;

-  {

-    if (left == null) {

-      min := data;

-      node := right;

-    } else {

-      call min, t := left.RemoveMin();

-      left := t;

-      node := this;

-      contents := contents - {min};

-      if (left != null) { footprint := footprint + left.footprint; }

-    }

-  }

-}

-

-class Main {

-  method Client0(x: int)

-  {

-    var s := new IntSet;

-    call s.Init();

-

-    call s.Insert(12);

-    call s.Insert(24);

-    call present := s.Find(x);

-    assert present <==> x == 12 || x == 24;

-  }

-

-  method Client1(s: IntSet, x: int)

-    requires s != null && s.Valid();

-    modifies s.footprint;

-  {

-    call s.Insert(x);

-    call s.Insert(24);

-    assert old(s.contents) - {x,24} == s.contents - {x,24};

-  }

-}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index eb7ea4f7..aa45ca05 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -11,19 +11,10 @@ for %%f in (Simple.dfy) do (
   %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f

 )

 

-for %%f in (BQueue.bpl) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %BPLEXE% %* %%f

-)

-

 for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy

-            Modules0.dfy Modules1.dfy BadFunction.dfy Queue.dfy ListCopy.dfy

-            BinaryTree.dfy ListReverse.dfy ListContents.dfy

-            SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy

-            TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy

-            SumOfCubes.dfy TerminationDemos.dfy Substitution.dfy

-            Tree.dfy Celebrity.dfy) do (

+            Modules0.dfy Modules1.dfy BadFunction.dfy

+            Termination.dfy Use.dfy DTypes.dfy

+            TypeParameters.dfy Datatypes.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 %* %%f

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
new file mode 100644
index 00000000..cf593abf
--- /dev/null
+++ b/Test/dafny1/Answer
@@ -0,0 +1,56 @@
+

+-------------------- BQueue.bpl --------------------

+

+Boogie program verifier finished with 8 verified, 0 errors

+

+-------------------- Queue.dfy --------------------

+

+Dafny program verifier finished with 22 verified, 0 errors

+

+-------------------- BinaryTree.dfy --------------------

+

+Dafny program verifier finished with 24 verified, 0 errors

+

+-------------------- UnboundedStack.dfy --------------------

+

+Dafny program verifier finished with 12 verified, 0 errors

+

+-------------------- ListCopy.dfy --------------------

+

+Dafny program verifier finished with 4 verified, 0 errors

+

+-------------------- ListReverse.dfy --------------------

+

+Dafny program verifier finished with 2 verified, 0 errors

+

+-------------------- ListContents.dfy --------------------

+

+Dafny program verifier finished with 9 verified, 0 errors

+

+-------------------- SchorrWaite.dfy --------------------

+

+Dafny program verifier finished with 10 verified, 0 errors

+

+-------------------- SumOfCubes.dfy --------------------

+

+Dafny program verifier finished with 17 verified, 0 errors

+

+-------------------- TerminationDemos.dfy --------------------

+

+Dafny program verifier finished with 10 verified, 0 errors

+

+-------------------- Substitution.dfy --------------------

+

+Dafny program verifier finished with 12 verified, 0 errors

+

+-------------------- TreeDatatype.dfy --------------------

+

+Dafny program verifier finished with 6 verified, 0 errors

+

+-------------------- Celebrity.dfy --------------------

+

+Dafny program verifier finished with 11 verified, 0 errors

+

+-------------------- UltraFilter.dfy --------------------

+

+Dafny program verifier finished with 19 verified, 0 errors

diff --git a/Test/dafny0/BQueue.bpl b/Test/dafny1/BQueue.bpl
index 77f1efb3..77f1efb3 100644
--- a/Test/dafny0/BQueue.bpl
+++ b/Test/dafny1/BQueue.bpl
diff --git a/Test/dafny1/BinaryTree.dfy b/Test/dafny1/BinaryTree.dfy
new file mode 100644
index 00000000..fbda3ecb
--- /dev/null
+++ b/Test/dafny1/BinaryTree.dfy
@@ -0,0 +1,244 @@
+class IntSet {

+  ghost var Contents: set<int>;

+  ghost var Repr: set<object>;

+

+  var root: Node;

+

+  function Valid(): bool

+    reads this, Repr;

+  {

+    this in Repr &&

+    (root == null ==> Contents == {}) &&

+    (root != null ==>

+       root in Repr && root.Repr <= Repr && this !in root.Repr &&

+       root.Valid() &&

+       Contents == root.Contents)

+  }

+

+  method Init()

+    modifies this;

+    ensures Valid() && fresh(Repr - {this});

+    ensures Contents == {};

+  {

+    root := null;

+    Repr := {this};

+    Contents := {};

+  }

+

+  method Find(x: int) returns (present: bool)

+    requires Valid();

+    ensures present <==> x in Contents;

+  {

+    if (root == null) {

+      present := false;

+    } else {

+      call present := root.Find(x);

+    }

+  }

+

+  method Insert(x: int)

+    requires Valid();

+    modifies Repr;

+    ensures Valid() && fresh(Repr - old(Repr));

+    ensures Contents == old(Contents) + {x};

+  { 

+    call t := InsertHelper(x, root);

+    root := t;

+    Contents := root.Contents;

+    Repr := root.Repr + {this};

+  }

+

+  static method InsertHelper(x: int, n: Node) returns (m: Node)

+    requires n == null || n.Valid();

+    modifies n.Repr;

+    ensures m != null && m.Valid();

+    ensures n == null ==> fresh(m.Repr) && m.Contents == {x};

+    ensures n != null ==> m == n && n.Contents == old(n.Contents) + {x};

+    ensures n != null ==> fresh(n.Repr - old(n.Repr));

+    decreases if n == null then {} else n.Repr;

+  {

+    if (n == null) {

+      m := new Node;

+      call m.Init(x);

+    } else if (x == n.data) {

+      m := n;

+    } else {

+      if (x < n.data) {

+        assert n.right == null || n.right.Valid();

+        call t := InsertHelper(x, n.left);

+        n.left := t;

+        n.Repr := n.Repr + n.left.Repr;

+      } else {

+        assert n.left == null || n.left.Valid();

+        call t := InsertHelper(x, n.right);

+        n.right := t;

+        n.Repr := n.Repr + n.right.Repr;

+      }

+      n.Contents := n.Contents + {x};

+      m := n;

+    }

+  }

+

+  method Remove(x: int)

+    requires Valid();

+    modifies Repr;

+    ensures Valid() && fresh(Repr - old(Repr));

+    ensures Contents == old(Contents) - {x};

+  {

+    if (root != null) {

+      call newRoot := root.Remove(x);

+      root := newRoot;

+      if (root == null) {

+        Contents := {};

+        Repr := {this};

+      } else {

+        Contents := root.Contents;

+        Repr := root.Repr + {this};

+      }

+    }

+  }

+}

+

+class Node {

+  ghost var Contents: set<int>;

+  ghost var Repr: set<object>;

+

+  var data: int;

+  var left: Node;

+  var right: Node;

+

+  function Valid(): bool

+    reads this, Repr;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (left != null ==>

+      left in Repr &&

+      left.Repr <= Repr && this !in left.Repr &&

+      left.Valid() &&

+      (forall y :: y in left.Contents ==> y < data)) &&

+    (right != null ==>

+      right in Repr &&

+      right.Repr <= Repr && this !in right.Repr &&

+      right.Valid() &&

+      (forall y :: y in right.Contents ==> data < y)) &&

+    (left == null && right == null ==>

+      Contents == {data}) &&

+    (left != null && right == null ==>

+      Contents == left.Contents + {data}) &&

+    (left == null && right != null ==>

+      Contents == {data} + right.Contents) &&

+    (left != null && right != null ==>

+      left.Repr !! right.Repr &&

+      Contents == left.Contents + {data} + right.Contents)

+  }

+

+  method Init(x: int)

+    modifies this;

+    ensures Valid() && fresh(Repr - {this});

+    ensures Contents == {x};

+  {

+    data := x;

+    left := null;

+    right := null;

+    Contents := {x};

+    Repr := {this};

+  }

+

+  method Find(x: int) returns (present: bool)

+    requires Valid();

+    ensures present <==> x in Contents;

+    decreases Repr;

+  {

+    if (x == data) {

+      present := true;

+    } else if (left != null && x < data) {

+      call present := left.Find(x);

+    } else if (right != null && data < x) {

+      call present := right.Find(x);

+    } else {

+      present := false;

+    }

+  }

+

+  method Remove(x: int) returns (node: Node)

+    requires Valid();

+    modifies Repr;

+    ensures fresh(Repr - old(Repr));

+    ensures node != null ==> node.Valid();

+    ensures node == null ==> old(Contents) <= {x};

+    ensures node != null ==> node.Repr <= Repr && node.Contents == old(Contents) - {x};

+    decreases Repr;

+  {

+    node := this;

+    if (left != null && x < data) {

+      call t := left.Remove(x);

+      left := t;

+      Contents := Contents - {x};

+      if (left != null) { Repr := Repr + left.Repr; }

+    } else if (right != null && data < x) {

+      call t := right.Remove(x);

+      right := t;

+      Contents := Contents - {x};

+      if (right != null) { Repr := Repr + right.Repr; }

+    } else if (x == data) {

+      if (left == null && right == null) {

+        node := null;

+      } else if (left == null) {

+        node := right;

+      } else if (right == null) {

+        node := left;

+      } else {

+        // rotate

+        call min, r := right.RemoveMin();

+        data := min;  right := r;

+        Contents := Contents - {x};

+        if (right != null) { Repr := Repr + right.Repr; }

+      }

+    }

+  }

+

+  method RemoveMin() returns (min: int, node: Node)

+    requires Valid();

+    modifies Repr;

+    ensures fresh(Repr - old(Repr));

+    ensures node != null ==> node.Valid();

+    ensures node == null ==> old(Contents) == {min};

+    ensures node != null ==> node.Repr <= Repr && node.Contents == old(Contents) - {min};

+    ensures min in old(Contents) && (forall x :: x in old(Contents) ==> min <= x);

+    decreases Repr;

+  {

+    if (left == null) {

+      min := data;

+      node := right;

+    } else {

+      call min, t := left.RemoveMin();

+      left := t;

+      node := this;

+      Contents := Contents - {min};

+      if (left != null) { Repr := Repr + left.Repr; }

+    }

+  }

+}

+

+class Main {

+  method Client0(x: int)

+  {

+    var s := new IntSet;

+    call s.Init();

+

+    call s.Insert(12);

+    call s.Insert(24);

+    call present := s.Find(x);

+    assert present <==> x == 12 || x == 24;

+  }

+

+  method Client1(s: IntSet, x: int)

+    requires s != null && s.Valid();

+    modifies s.Repr;

+  {

+    call s.Insert(x);

+    call s.Insert(24);

+    assert old(s.Contents) - {x,24} == s.Contents - {x,24};

+  }

+}

diff --git a/Test/dafny0/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index fd267c71..fd267c71 100644
--- a/Test/dafny0/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny1/ListContents.dfy
index 62636ce5..62636ce5 100644
--- a/Test/dafny0/ListContents.dfy
+++ b/Test/dafny1/ListContents.dfy
diff --git a/Test/dafny0/ListCopy.dfy b/Test/dafny1/ListCopy.dfy
index 52f5cf76..52f5cf76 100644
--- a/Test/dafny0/ListCopy.dfy
+++ b/Test/dafny1/ListCopy.dfy
diff --git a/Test/dafny0/ListReverse.dfy b/Test/dafny1/ListReverse.dfy
index ef029b88..ef029b88 100644
--- a/Test/dafny0/ListReverse.dfy
+++ b/Test/dafny1/ListReverse.dfy
diff --git a/Test/dafny0/Queue.dfy b/Test/dafny1/Queue.dfy
index 42b7dd64..42b7dd64 100644
--- a/Test/dafny0/Queue.dfy
+++ b/Test/dafny1/Queue.dfy
diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index a46e83a3..a46e83a3 100644
--- a/Test/dafny0/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
diff --git a/Test/dafny0/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 72415fea..72415fea 100644
--- a/Test/dafny0/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
diff --git a/Test/dafny0/SumOfCubes.dfy b/Test/dafny1/SumOfCubes.dfy
index b4fab490..b4fab490 100644
--- a/Test/dafny0/SumOfCubes.dfy
+++ b/Test/dafny1/SumOfCubes.dfy
diff --git a/Test/dafny0/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy
index 6b63bfec..6b63bfec 100644
--- a/Test/dafny0/TerminationDemos.dfy
+++ b/Test/dafny1/TerminationDemos.dfy
diff --git a/Test/dafny0/Tree.dfy b/Test/dafny1/TreeDatatype.dfy
index 58124171..58124171 100644
--- a/Test/dafny0/Tree.dfy
+++ b/Test/dafny1/TreeDatatype.dfy
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
new file mode 100644
index 00000000..61e86836
--- /dev/null
+++ b/Test/dafny1/UltraFilter.dfy
@@ -0,0 +1,108 @@
+// ultra filter

+

+class UltraFilter<G> {

+  static function IsFilter(f: set<set<G>>, S: set<G>): bool

+  {

+    (forall A, B :: A in f && A <= B ==> B in f) &&

+    (forall C, D :: C in f && D in f ==> C * D in f) &&

+    S in f &&

+    {} !in f

+  }

+

+  static function IsUltraFilter(f: set<set<G>>, S: set<G>): bool

+  {

+    IsFilter(f, S) &&

+    (forall g :: IsFilter(g, S) && f <= g ==> f == g)

+  }

+

+  method Theorem(f: set<set<G>>, S: set<G>, M: set<G>, N: set<G>)

+    requires IsUltraFilter(f, S);

+    requires M + N in f;

+    ensures M in f || N in f;

+  {

+    if (M !in f) {

+      // instantiate 'g' with the following 'h'

+      call h := H(f, S, M);

+      call Lemma_HIsFilter(h, f, S, M);

+      call Lemma_FHOrdering0(h, f, S, M);

+    }

+  }

+

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

+

+  method Lemma_HIsFilter(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)

+    requires IsFilter(f, S);

+    requires (forall X :: X in h <==> M + X in f);

+    requires M !in f;

+    ensures IsFilter(h, S);

+  {

+    // call Lemma_H0(h, f, S, M, *, *);

+    assume (forall A, B :: A in h && A <= B ==> B in h);

+

+    // call Lemma_H1(h, f, S, M, *, *);

+    assume (forall C, D :: C in h && D in h ==> C * D in h);

+

+    call Lemma_H2(h, f, S, M);

+

+    call Lemma_H3(h, f, S, M);

+  }

+

+  method Lemma_H0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, A: set<G>, B: set<G>)

+    requires IsFilter(f, S);

+    requires (forall X :: X in h <==> M + X in f);

+    requires A in h && A <= B;

+    ensures B in h;

+  {

+    assert M + A <= M + B;

+  }

+

+  method Lemma_H1(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, C: set<G>, D: set<G>)

+    requires IsFilter(f, S);

+    requires (forall X :: X in h <==> M + X in f);

+    requires C in h && D in h;

+    ensures C * D in h;

+  {

+    assert (M + C) * (M + D) == M + (C * D);

+  }

+

+  method Lemma_H2(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)

+    requires IsFilter(f, S);

+    requires (forall X :: X in h <==> M + X in f);

+    ensures S in h;

+  {

+    // S is intended to stand for the universal set, but this is the only place where that plays a role

+    assume M <= S;

+

+    assert M + S == S;

+  }

+

+  method Lemma_H3(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)

+    requires IsFilter(f, S);

+    requires (forall X :: X in h <==> M + X in f);

+    requires M !in f;

+    ensures {} !in h;

+  {

+    assert M + {} == M;

+  }

+

+  method Lemma_FHOrdering0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)

+    requires IsFilter(f, S);

+    requires (forall X :: X in h <==> M + X in f);

+    requires IsFilter(h, S);

+    ensures f <= h;

+  {

+    // call Lemma_FHOrdering1(h, f, S, M, *);

+    assume (forall Y :: Y in f ==> Y in h);

+    assume f <= h;  // hickup in boxing

+  }

+

+  method Lemma_FHOrdering1(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, Y: set<G>)

+    requires IsFilter(f, S);

+    requires (forall X :: X in h <==> M + X in f);

+    ensures Y in f ==> Y in h;

+  {

+    assert Y <= M + Y;

+  }

+}

diff --git a/Test/dafny0/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy
index 4c3b095a..4c3b095a 100644
--- a/Test/dafny0/UnboundedStack.dfy
+++ b/Test/dafny1/UnboundedStack.dfy
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
new file mode 100644
index 00000000..aab76ff9
--- /dev/null
+++ b/Test/dafny1/runtest.bat
@@ -0,0 +1,26 @@
+@echo off

+setlocal

+

+set BOOGIEDIR=..\..\Binaries

+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

+set BPLEXE=%BOOGIEDIR%\Boogie.exe

+

+for %%f in (BQueue.bpl) do (

+  echo.

+  echo -------------------- %%f --------------------

+  %BPLEXE% %* %%f

+)

+

+for %%f in (Queue.dfy

+            BinaryTree.dfy

+            UnboundedStack.dfy

+            ListCopy.dfy ListReverse.dfy ListContents.dfy

+            SchorrWaite.dfy

+            SumOfCubes.dfy

+            TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy

+            Celebrity.dfy

+            UltraFilter.dfy) do (

+  echo.

+  echo -------------------- %%f --------------------

+  %DAFNY_EXE% /compile:0 %* %%f

+)