From 0d94c8f5795b092372df5a06d6d0f9306d696d9b Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Tue, 21 Jul 2015 11:38:51 -0700
Subject: Update z3 to 4.4. One test had to be edited.

---
 Test/VerifyThis2015/Problem3.dfy        | 20 +++++++++++++++++++-
 Test/VerifyThis2015/Problem3.dfy.expect |  2 +-
 2 files changed, 20 insertions(+), 2 deletions(-)

(limited to 'Test/VerifyThis2015')

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...
 
-- 
cgit v1.2.3