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, 27 insertions, 0 deletions

diff --git a/Test/dafny1/ListReverse.dfy b/Test/dafny1/ListReverse.dfy
new file mode 100644
index 00000000..ef029b88
--- /dev/null
+++ b/Test/dafny1/ListReverse.dfy
@@ -0,0 +1,27 @@
+

+class Node {

+  var nxt: Node;

+

+  method ReverseInPlace(x: Node, r: set<Node>) returns (reverse: Node)

+    requires null !in r;

+    requires x == null || x in r;

+    requires (forall y :: y in r ==> y.nxt == null || y.nxt in r);  // region closure

+    modifies r;

+    ensures reverse == null || reverse in r;

+    ensures (forall y :: y in r ==> y.nxt == null || y.nxt in r);  // region closure

+  {

+    var current := x;

+    reverse := null;

+    while (current != null)

+      invariant current == null || current in r;

+      invariant reverse == null || reverse in r;

+      invariant (forall y :: y in r ==> y.nxt == null || y.nxt in r);  // region closure

+      decreases *;  // omit loop termination check

+    {

+      var tmp := current.nxt;

+      current.nxt := reverse;

+      reverse := current;

+      current := tmp;

+    }

+  }

+}