Update z3 to 4.4. One test had to be edited.

2 files changed, 20 insertions, 2 deletions

diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy
index 4205035d..21bdd4ed 100644
--- a/Test/VerifyThis2015/Problem3.dfy
+++ b/Test/VerifyThis2015/Problem3.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:5 "%s" > "%t"

+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 // Rustan Leino

@@ -92,6 +92,21 @@ class DoublyLinkedList {
     }

     Nodes := nodes;

   }

+

+  function PopMiddle<T>(s: seq<T>, k: nat) : seq<T>

+    requires k < |s| {

+      s[..k] + s[k+1..]

+  }

+

+  predicate Injective<T>(s: seq<T>) {

+    forall j, k :: 0 <= j < k < |s| ==> s[j] != s[k]

+  }

+

+  lemma InjectiveAfterPop<T>(s: seq<T>, k: nat)

+    requires k < |s|

+    requires Injective(s)

+    ensures  Injective(PopMiddle(s, k)) { }

+

   method Remove(x: Node) returns (ghost k: int)

     requires Valid()

     requires x in Nodes && x != Nodes[0] && x != Nodes[|Nodes|-1]  // not allowed to remove end nodes; you may think of them as a sentinel nodes

@@ -103,8 +118,11 @@ class DoublyLinkedList {
     k :| 1 <= k < |Nodes|-1 && Nodes[k] == x;

     x.R.L := x.L;

     x.L.R := x.R;

+

+    InjectiveAfterPop(Nodes, k);

     Nodes := Nodes[..k] + Nodes[k+1..];

   }

+

   // One might consider have a precondition that says there exists a "k" with the properties given here.

   // However, we want to be able to refer to "k" in the postcondition as well, so it's convenient to

   // burden the client with having to pass in "k" as a ghost parameter.  This, however, is really no

diff --git a/Test/VerifyThis2015/Problem3.dfy.expect b/Test/VerifyThis2015/Problem3.dfy.expect
index 4035605c..d3a9554b 100644
--- a/Test/VerifyThis2015/Problem3.dfy.expect
+++ b/Test/VerifyThis2015/Problem3.dfy.expect
@@ -1,5 +1,5 @@
 

-Dafny program verifier finished with 15 verified, 0 errors

+Dafny program verifier finished with 19 verified, 0 errors

 Program compiled successfully

 Running...