From 4fe2619c267b0330dc3ceaca761256794094d3cc Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Fri, 28 Aug 2015 23:13:38 -0700
Subject: Fix some tests by locally disabling auto triggers

---
 Test/dafny1/Rippling.dfy    | 6 +++---
 Test/dafny1/SchorrWaite.dfy | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'Test/dafny1')

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 4d1761b1..d888a5cc 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -550,7 +550,7 @@ lemma P54()
   ensures forall m, n :: minus(add(m, n), n) == m;
 {
   // the proof of this theorem follows from two lemmas:
-  assert forall m, n :: minus(add(n, m), n) == m;
+  assert forall m, n {:autotriggers false} :: minus(add(n, m), n) == m; // FIXME: Why does Autotriggers false make things verify?
   assert forall m, n :: add(m, n) == add(n, m);
 }
 
@@ -559,7 +559,7 @@ lemma P65()
 {
   if (*) {
     // the proof of this theorem follows from two lemmas:
-    assert forall i, m :: less(i, Suc(add(i, m))) == True;
+    assert forall i, m {:autotriggers false} :: less(i, Suc(add(i, m))) == True; // FIXME: Why does Autotriggers false make things verify?
     assert forall m, n :: add(m, n) == add(n, m);
   } else {
     // a different way to prove it uses the following lemma:
@@ -572,7 +572,7 @@ lemma P67()
 {
   if (*) {
     // the proof of this theorem follows from two lemmas:
-    assert forall m, n :: leq(n, add(n, m)) == True;
+    assert forall m, n {:autotriggers false} :: leq(n, add(n, m)) == True; // FIXME: Why does Autotriggers false make things verify?
     assert forall m, n :: add(m, n) == add(n, m);
   } else {
     // a different way to prove it uses the following lemma:
diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index b29a6829..50210eb1 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -180,7 +180,7 @@ class Main {
     ensures forall n :: n in S && n.marked ==>
                 forall ch :: ch in n.children && ch != null ==> ch.marked
     // every marked node was reachable from 'root' in the pre-state:
-    ensures forall n :: n in S && n.marked ==> old(Reachable(root, n, S))
+    ensures forall n {:autotriggers false} :: n in S && n.marked ==> old(Reachable(root, n, S))
     // the structure of the graph has not changed:
     ensures forall n :: n in S ==>
                 n.childrenVisited == old(n.childrenVisited) &&
@@ -207,7 +207,7 @@ class Main {
                   forall j :: 0 <= j < n.childrenVisited ==>
                     n.children[j] == null || n.children[j].marked
       invariant forall n :: n in stackNodes ==> n.childrenVisited < |n.children|
-      invariant forall n :: n in S && n.marked && n !in stackNodes && n != t ==>
+      invariant forall n {:autotriggers false} :: n in S && n.marked && n !in stackNodes && n != t ==>
                   forall ch :: ch in n.children && ch != null ==> ch.marked
       invariant forall n :: n in S && n !in stackNodes && n != t ==>
                   n.childrenVisited == old(n.childrenVisited)
@@ -219,7 +219,7 @@ class Main {
       // every marked node is reachable:
       invariant !fresh(path);  // needed to show 'path' worthy as argument to old(Reachable(...))
       invariant old(ReachableVia(root, path, t, S));
-      invariant forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==> !fresh(pth)
+      invariant forall n, pth {:nowarn} :: n in S && n.marked && pth == n.pathFromRoot ==> !fresh(pth)
       invariant forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==>
                   old(ReachableVia(root, pth, n, S))
       invariant forall n :: n in S && n.marked ==> old(Reachable(root, n, S))
-- 
cgit v1.2.3