Fix some tests by locally disabling auto triggers

4 files changed, 10 insertions, 8 deletions

diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy
index 274d86de..0cf93061 100644
--- a/Test/VSComp2010/Problem2-Invert.dfy
+++ b/Test/VSComp2010/Problem2-Invert.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %dafny /compile:0 /autoTriggers:0 "%s" > "%t"

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

 

 // VSComp 2010, problem 2, compute the inverse 'B' of a permutation 'A' and prove that 'B' is

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))

diff --git a/Test/dafny4/NipkowKlein-chapter7.dfy b/Test/dafny4/NipkowKlein-chapter7.dfy
index e694fc4b..aae94550 100644
--- a/Test/dafny4/NipkowKlein-chapter7.dfy
+++ b/Test/dafny4/NipkowKlein-chapter7.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t"

+// RUN: %dafny /compile:0 /rprint:"%t.rprint" /autoTriggers:0 "%s" > "%t"

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

 

 // This file is a Dafny encoding of chapter 7 from "Concrete Semantics: With Isabelle/HOL" by

@@ -360,3 +360,5 @@ lemma lemma_7_18(c: com, s: state)
     BigStep_SmallStepStar_Same(c, s, s');

   }

 }

+

+// Autotriggers:0 added as this file relies on proving a property of the form body(f) == f