diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-28 23:13:38 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-28 23:13:38 -0700 |
| commit | 4fe2619c267b0330dc3ceaca761256794094d3cc (patch) | |
| tree | d6ccb34ea301b01515bc5ae91f873ee61ba1e60e /Test/dafny1 | |
| parent | 6b1085d784e3773ad9ccbae5bd6b158c97095edc (diff) | |
Fix some tests by locally disabling auto triggers
Diffstat (limited to 'Test/dafny1')
| -rw-r--r-- | Test/dafny1/Rippling.dfy | 6 | ||||
| -rw-r--r-- | Test/dafny1/SchorrWaite.dfy | 6 |
2 files changed, 6 insertions, 6 deletions
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))
|