summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Test/VSComp2010/Problem2-Invert.dfy2
-rw-r--r--Test/dafny1/Rippling.dfy6
-rw-r--r--Test/dafny1/SchorrWaite.dfy6
-rw-r--r--Test/dafny4/NipkowKlein-chapter7.dfy4
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