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.

1 files changed, 55 insertions, 0 deletions

diff --git a/Test/dafny1/ListCopy.dfy b/Test/dafny1/ListCopy.dfy
new file mode 100644
index 00000000..52f5cf76
--- /dev/null
+++ b/Test/dafny1/ListCopy.dfy
@@ -0,0 +1,55 @@
+class Node {

+  var nxt: Node;

+

+  method Init()

+    modifies this;

+    ensures nxt == null;

+  {

+    nxt := null;

+  }

+

+  method Copy(root: Node) returns (result: Node)

+  {

+    var existingRegion: set<Node>;

+    assume root == null || root in existingRegion;

+    assume (forall o: Node :: o != null && o in existingRegion && o.nxt != null ==> o.nxt in existingRegion);

+

+    var newRoot := null;

+    var oldListPtr := root;

+    var newRegion: set<Node> := {};

+

+    if (oldListPtr != null) {

+      newRoot := new Node;

+      call newRoot.Init();

+      newRegion := newRegion + {newRoot};

+      var prev := newRoot;

+

+      while (oldListPtr != null)

+        invariant newRoot in newRegion;

+        invariant (forall o: Node :: o in newRegion ==> o != null);

+        invariant (forall o: Node :: o in newRegion && o.nxt != null ==> o.nxt in newRegion);

+        invariant prev in newRegion;

+        invariant fresh(newRegion);

+        invariant newRegion !! existingRegion;

+        decreases *;  // omit loop termination check

+      {

+        var tmp := new Node;

+        call tmp.Init();

+

+        newRegion := newRegion + {tmp};

+        prev.nxt := tmp;

+

+        prev := tmp;

+        oldListPtr := oldListPtr.nxt;

+      }

+    } 

+    result := newRoot;

+    assert result == null || result in newRegion;

+    

+    // everything in newRegion is fresh

+    assert fresh(newRegion);

+

+    // newRegion # exisitingRegion

+    assert newRegion !! existingRegion; 

+  }

+}