8 files changed, 39 insertions, 23 deletions
diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy
index c752bd38..f691384c 100644
--- a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy
@@ -117,6 +117,11 @@ class Tree {
     Repr := lft.Repr + {this} + rgt.Repr;
   }
 
+  lemma exists_intro<T>(P: T -> bool, x: T)
+    requires P.requires(x)
+    requires P(x)
+    ensures exists y :: P.requires(y) && P(y) { }
+
   method ComputeMax() returns (mx: int)
     requires Valid() && !IsEmpty();
     ensures forall x :: x in Contents ==> x <= mx;
@@ -124,13 +129,17 @@ class Tree {
     decreases Repr;
   {
     mx := value;
+
     if (!left.IsEmpty()) {
       var m := left.ComputeMax();
       mx := if mx < m  then m else mx;
     }
+
     if (!right.IsEmpty()) {
       var m := right.ComputeMax();
       mx := if mx < m then m else mx;
     }
+
+    exists_intro(x reads this => x in Contents && x == mx, mx);
   }
 }
diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy.expect b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy.expect
index 42fd56a5..c87e2af2 100644
--- a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy.expect
+++ b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 8 verified, 0 errors
+Dafny program verifier finished with 10 verified, 0 errors
diff --git a/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy
index 72a22cfd..4c702674 100644
--- a/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy
@@ -93,8 +93,8 @@ method Search(a: array<int>) returns (p: int, q: int)
     invariant forall j :: 0 <= j < d.Length ==>
                 (d[j] == -1 && forall k :: 0 <= k < i ==> a[k] != j) ||
                 (0 <= d[j] < i && a[d[j]] == j);
-    invariant p == q ==> IsDuplicate(a, p);
-    invariant forall k :: 0 <= k < i && IsPrefixDuplicate(a, i, a[k]) ==> p == q == a[k];
+    invariant p == q ==> IsDuplicate(a, p); //WISH remove the trigger on the next line
+    invariant forall k {:trigger old(a[k])} :: 0 <= k < i && IsPrefixDuplicate(a, i, a[k]) ==> p == q == a[k];
     decreases a.Length - i;
   {
     var k := d[a[i]];
diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
index 2aa14db7..72250f99 100644
--- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
@@ -164,7 +164,7 @@ class Node {
       invariant 0 <= t < h && Nexxxt(t, S) == tortoise && Nexxxt(h, S) == hare;
       // What follows of the invariant is for proving termination:
       invariant h == 1 + 2*t && t <= A + B;
-      invariant forall k :: 0 <= k < t ==> Nexxxt(k, S) != Nexxxt(1+2*k, S);
+      invariant forall k {:nowarn} :: 0 <= k < t ==> Nexxxt(k, S) != Nexxxt(1+2*k, S);
       decreases A + B - t;
     {
       if hare == null || hare.next == null {
@@ -225,7 +225,7 @@ class Node {
     requires 0 <= a && 1 <= b;
     requires forall k,l :: 0 <= k < l < a ==> Nexxxt(k, S) != Nexxxt(l, S);
     requires Nexxxt(a, S) == null || Nexxxt(a, S).Nexxxt(b, S) == Nexxxt(a, S);
-    ensures exists T :: 0 <= T < a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S);
+    ensures exists T {:nowarn} :: 0 <= T < a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S);
   {
     if Nexxxt(a, S) == null {
       Lemma_NullIsTerminal(1+2*a, S);
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
index 8af0afe9..3870490f 100644
--- a/Test/dafny2/Calculations.dfy
+++ b/Test/dafny2/Calculations.dfy
@@ -41,12 +41,12 @@ function qreverse(l: List): List
 
 // Here are two lemmas about the List functions.
 
-ghost method Lemma_ConcatNil(xs : List)
+lemma Lemma_ConcatNil(xs : List)
   ensures concat(xs, Nil) == xs;
 {
 }
 
-ghost method Lemma_RevCatCommute(xs : List)
+lemma Lemma_RevCatCommute(xs : List)
   ensures forall ys, zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs);
 {
 }
@@ -55,7 +55,7 @@ ghost method Lemma_RevCatCommute(xs : List)
 // is given in a calculational style.  The proof is not minimal--some lines can be omitted
 // and Dafny will still fill in the details.
 
-ghost method Theorem_QReverseIsCorrect_Calc(l: List)
+lemma Theorem_QReverseIsCorrect_Calc(l: List)
   ensures qreverse(l) == reverse(l);
 {
   calc {
@@ -69,7 +69,7 @@ ghost method Theorem_QReverseIsCorrect_Calc(l: List)
   }
 }
 
-ghost method Lemma_Revacc_calc(xs: List, ys: List)
+lemma Lemma_Revacc_calc(xs: List, ys: List)
   ensures revacc(xs, ys) == concat(reverse(xs), ys);
 {
   match (xs) {
@@ -93,7 +93,7 @@ ghost method Lemma_Revacc_calc(xs: List, ys: List)
 
 // Here is a version of the same proof, as it was constructed before Dafny's "calc" construct.
 
-ghost method Theorem_QReverseIsCorrect(l: List)
+lemma Theorem_QReverseIsCorrect(l: List)
   ensures qreverse(l) == reverse(l);
 {
   assert qreverse(l)
@@ -105,7 +105,7 @@ ghost method Theorem_QReverseIsCorrect(l: List)
   Lemma_ConcatNil(reverse(l));
 }
 
-ghost method Lemma_Revacc(xs: List, ys: List)
+lemma Lemma_Revacc(xs: List, ys: List)
   ensures revacc(xs, ys) == concat(reverse(xs), ys);
 {
   match (xs) {
@@ -140,7 +140,7 @@ function Fib(n: nat): nat
   if n < 2 then n else Fib(n - 2) + Fib(n - 1)
 }
 
-ghost method Lemma_Fib()
+lemma Lemma_Fib()
   ensures Fib(5) < 6;
 {
   calc {
@@ -160,11 +160,11 @@ ghost method Lemma_Fib()
 /* List length */
 // Here are some proofs that show the use of nested calculations.
 
-ghost method Lemma_Concat_Length(xs: List, ys: List)
+lemma Lemma_Concat_Length(xs: List, ys: List)
   ensures length(concat(xs, ys)) == length(xs) + length(ys);
 {}
 
-ghost method Lemma_Reverse_Length(xs: List)
+lemma Lemma_Reverse_Length(xs: List)
   ensures length(xs) == length(reverse(xs));
 {
   match (xs) {
@@ -193,7 +193,7 @@ ghost method Lemma_Reverse_Length(xs: List)
   }
 }
 
-ghost method Window(xs: List, ys: List)
+lemma Window(xs: List, ys: List)
   ensures length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(ys));
 {
   calc {
@@ -221,11 +221,11 @@ function ith<a>(xs: List, i: nat): a
   case Cons(x, xrest) => if i == 0 then x else ith(xrest, i - 1)
 }
 
-ghost method lemma_zero_length(xs: List)
+lemma lemma_zero_length(xs: List)
   ensures length(xs) == 0 <==> xs.Nil?;
 {}
 
-ghost method lemma_extensionality(xs: List, ys: List)
+lemma lemma_extensionality(xs: List, ys: List)
   requires length(xs) == length(ys); // (0)
   requires forall i: nat | i < length(xs) :: ith(xs, i) == ith(ys, i); // (1)
   ensures xs == ys;
diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy
index 51e5b968..f1c3b485 100644
--- a/Test/dafny2/MajorityVote.dfy
+++ b/Test/dafny2/MajorityVote.dfy
@@ -165,7 +165,7 @@ method SearchForWinner<Candidate(==)>(a: seq<Candidate>, ghost hasWinner: bool,
 
 // Here are two lemmas about Count that are used in the methods above.
 
-ghost method Lemma_Split<T>(a: seq<T>, s: int, t: int, u: int, x: T)
+lemma Lemma_Split<T>(a: seq<T>, s: int, t: int, u: int, x: T)
   requires 0 <= s <= t <= u <= |a|;
   ensures Count(a, s, t, x) + Count(a, t, u, x) == Count(a, s, u, x);
 {
@@ -178,7 +178,7 @@ ghost method Lemma_Split<T>(a: seq<T>, s: int, t: int, u: int, x: T)
   */
 }
 
-ghost method Lemma_Unique<T>(a: seq<T>, s: int, t: int, x: T, y: T)
+lemma Lemma_Unique<T>(a: seq<T>, s: int, t: int, x: T, y: T)
   requires 0 <= s <= t <= |a|;
   ensures x != y ==> Count(a, s, t, x) + Count(a, s, t, y) <= t - s;
 {
diff --git a/Test/dafny2/SnapshotableTrees.dfy b/Test/dafny2/SnapshotableTrees.dfy
index 2bdfb83b..033c5db0 100644
--- a/Test/dafny2/SnapshotableTrees.dfy
+++ b/Test/dafny2/SnapshotableTrees.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:2 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:2 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Rustan Leino, September 2011.
diff --git a/Test/dafny2/SnapshotableTrees.dfy.expect b/Test/dafny2/SnapshotableTrees.dfy.expect
index 849b9e38..68b4ff73 100644
--- a/Test/dafny2/SnapshotableTrees.dfy.expect
+++ b/Test/dafny2/SnapshotableTrees.dfy.expect
@@ -1,8 +1,15 @@
-SnapshotableTrees.dfy(68,24): Error BP5002: A precondition for this call might not hold.
-SnapshotableTrees.dfy(648,16): Related location: This is the precondition that might not hold.
+SnapshotableTrees.dfy(68,23): Error BP5002: A precondition for this call might not hold.
+SnapshotableTrees.dfy(648,15): Related location: This is the precondition that might not hold.
+SnapshotableTrees.dfy(545,15): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Then
+SnapshotableTrees.dfy(68,23): Error BP5002: A precondition for this call might not hold.
+SnapshotableTrees.dfy(648,15): Related location: This is the precondition that might not hold.
+SnapshotableTrees.dfy(548,18): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon3_Then
 
-Dafny program verifier finished with 65 verified, 1 error
+Dafny program verifier finished with 65 verified, 2 errors
 Compiled assembly into SnapshotableTrees.exe