Merge pull request #714 from viperproject/fix-test-triggers

Fix test triggers

src/test/resources/all/third_party/stefan_recent/testTreeWandE1.vpr

@@ -1,6 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 //:: IgnoreFile(/Carbon/issue/253/)
 field Wand_state_contains_for_state_contains__lemma: Int
 
@@ -76,9 +76,14 @@ function Tree__tolist(t: Ref): Seq[Int]
   (t == null ? Seq[Int]() : (unfolding acc(Tree__state(t), write) in Tree__tolist(t.Tree__left) ++ Seq(t.Tree__data) ++ Tree__tolist(t.Tree__right)))
 }
 
+/*function Tree__sorted_list(s: Seq[Int]): Bool
+{
+  (forall i: Int :: (1 < i) && (i < |s|) ==> (s[i - 1] <= s[i])) // clear matching loop :(
+}*/
+
 function Tree__sorted_list(s: Seq[Int]): Bool
 {
-  (forall i: Int :: (1 < i) && (i < |s|) ==> (s[i - 1] <= s[i]))
+  (forall i: Int, j: Int :: {s[i],s[j]} (1 <= i) && (i < j) && (j < |s|) ==> (s[i] <= s[j]))
 }
 
 function Tree__sorted(t: Ref): Bool

src/test/resources/examples/quickselect/arrays_quickselect_rec.vpr

@@ -37,7 +37,7 @@ method swap(a: IArray, i: Int, j: Int)
  * axiom again, causing a matching loop.
  */
 define permuted(a, left, right, pw)
-  forall i: Int :: {old(pw[i])} left <= i && i <= right ==> loc(a, i).val == old(loc(a, pw[i]).val)
+  forall i: Int :: {pw[i]} left <= i && i <= right ==> loc(a, i).val == old(loc(a, pw[i]).val)
 
 method partition(a: IArray, left: Int, right: Int, pivotIndex: Int) returns (storeIndex: Int, pw: Seq[Int])
   /* All indices are valid and their relative order is satisfied */
@@ -150,7 +150,6 @@ method select_rec(a: IArray, left: Int, right: Int, n: Int) returns (storeIndex:
 {
   var pwPar: Seq[Int]
   var pwRec: Seq[Int]
-
   if (left == right) {
     /* If the list contains only one element, return it */
     storeIndex := left