diff options
Diffstat (limited to 'Test')
62 files changed, 412 insertions, 244 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/VerifyThis2015/Problem2.dfy b/Test/VerifyThis2015/Problem2.dfy index 1c7deffd..86b4a019 100644 --- a/Test/VerifyThis2015/Problem2.dfy +++ b/Test/VerifyThis2015/Problem2.dfy @@ -315,7 +315,7 @@ lemma GcdDecrease(a: int, b: int) ensures Gcd(a, b) == Gcd(a - b, b)
{
var k := Gcd(a - b, b);
- assert DividesBoth(k, a-b, b) && forall m :: DividesBoth(m, a-b, b) ==> m <= k;
+ assert DividesBoth(k, a-b, b) && forall m, mm :: mm == a - b ==> DividesBoth(m, mm, b) ==> m <= k; // WISH: auto-generate 'mm'
var n := DividesProperty(k, a-b);
assert n*k == a-b;
var p := DividesProperty(k, b);
diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy index 391ca5f7..309e9248 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class A {
@@ -327,3 +327,5 @@ module DtypeRegression { }
}
}
+
+// WISH: autoTriggers disabled because of induction
diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy index d0436815..dd83e46c 100644 --- a/Test/dafny0/Comprehensions.dfy +++ b/Test/dafny0/Comprehensions.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
method M()
@@ -19,18 +19,18 @@ datatype D = A | B // have to run the resulting program to check that the compiler is doing the right thing.
method Main()
{
- var q := set i,j | 0 <= i && i < 10 && 0 <= j && j < 3 :: i+j;
+ var q := set i,j | 0 <= i < 10 && 0 <= j < 3 :: i+j;
PrintSet(q);
q := set b: bool | true :: if b then 3 else 7;
var d := set b:D | true;
- var test := forall d:D :: d == A || d == B;
+ var test := forall d:D {:nowarn} :: d == A || d == B; // Ignoring the warning as we're only compiling here
PrintSet(q);
var m := set k | k in q :: 2*k;
PrintSet(m);
PrintSet(set k | k in q && k % 2 == 0);
var sq := [30, 40, 20];
- PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);
- var bb := forall k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i == 17;
+ PrintSet(set k, i | k in sq && 0 <= i < k && i % 7 == 0 :: k + i);
+ var bb := forall k, i {:nowarn} | k in sq && 0 <= i < k && i % 7 == 0 :: k + i == 17; // Ignoring the warning as we're only compiling here
}
method PrintSet<T>(s: set<T>) {
diff --git a/Test/dafny0/ComputationsNeg.dfy b/Test/dafny0/ComputationsNeg.dfy index 0c539117..b9425d64 100644 --- a/Test/dafny0/ComputationsNeg.dfy +++ b/Test/dafny0/ComputationsNeg.dfy @@ -16,7 +16,7 @@ predicate ThProperty(step: nat, t: Nat, r: nat) {
match t
case Zero => true
- case Succ(o) => step>0 && exists ro:nat :: ThProperty(step-1, o, ro)
+ case Succ(o) => step>0 && exists ro:nat, ss :: ss == step-1 ==> ThProperty(ss, o, ro) // WISH: auto-generate ss
}
ghost method test_ThProperty()
ensures ThProperty(10, Succ(Zero), 0);
diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy index c8c893a0..9e36e64c 100644 --- a/Test/dafny0/DTypes.dfy +++ b/Test/dafny0/DTypes.dfy @@ -5,7 +5,7 @@ class C { var n: set<Node>;
method M(v: Stack)
- requires v != null;
+ requires v != null
{
var o: object := v;
assert o !in n; // should be known from the types involved
@@ -28,12 +28,12 @@ class C { method A1(a: CP<int,C>)
{
var x: object := a;
- assert (forall b: CP<int,Stack> :: x == b ==> b == null); // follows from type antecedents
+ assert (forall b: CP<int,Stack> {:nowarn} :: x == b ==> b == null); // follows from type antecedents
}
var a2x: set<CP<C,Node>>;
method A2(b: set<CP<Node,C>>)
- requires null !in b;
+ requires null !in b
{
var x: set<object> := a2x;
var y: set<object> := b;
@@ -81,7 +81,7 @@ class CP<T,U> { datatype Data = Lemon | Kiwi(int)
function G(d: Data): int
- requires d != Data.Lemon;
+ requires d != Data.Lemon
{
match d
case Lemon => G(d)
@@ -101,28 +101,28 @@ class DatatypeInduction<T> { }
method Theorem0(tree: Tree<T>)
- ensures 1 <= LeafCount(tree);
+ ensures 1 <= LeafCount(tree)
{
assert (forall t: Tree<T> :: 1 <= LeafCount(t));
}
// also make sure it works for an instantiated generic datatype
method Theorem1(bt: Tree<bool>, it: Tree<int>)
- ensures 1 <= LeafCount(bt);
- ensures 1 <= LeafCount(it);
+ ensures 1 <= LeafCount(bt)
+ ensures 1 <= LeafCount(it)
{
assert (forall t: Tree<bool> :: 1 <= LeafCount(t));
assert (forall t: Tree<int> :: 1 <= LeafCount(t));
}
method NotATheorem0(tree: Tree<T>)
- ensures LeafCount(tree) % 2 == 1;
+ ensures LeafCount(tree) % 2 == 1
{
assert (forall t: Tree<T> :: LeafCount(t) % 2 == 1); // error: fails for Branch case
}
method NotATheorem1(tree: Tree<T>)
- ensures 2 <= LeafCount(tree);
+ ensures 2 <= LeafCount(tree)
{
assert (forall t: Tree<T> :: 2 <= LeafCount(t)); // error: fails for Leaf case
}
@@ -140,22 +140,22 @@ class DatatypeInduction<T> { // ----- here is a test for induction over integers
method IntegerInduction_Succeeds(a: array<int>)
- requires a != null;
- requires a.Length == 0 || a[0] == 0;
- requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;
+ requires a != null
+ requires a.Length == 0 || a[0] == 0
+ requires forall j {:nowarn} :: 1 <= j < a.Length ==> a[j] == a[j-1]+2*j-1 // WISH: If induction was more powerful, we wouldn't need to rely on the quantifier to produce the j-1 term.
{
// The following assertion can be proved by induction:
- assert forall n {:induction} :: 0 <= n && n < a.Length ==> a[n] == n*n;
+ assert forall n {:induction} :: 0 <= n < a.Length ==> a[n] == n*n;
}
method IntegerInduction_Fails(a: array<int>)
- requires a != null;
- requires a.Length == 0 || a[0] == 0;
- requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;
+ requires a != null
+ requires a.Length == 0 || a[0] == 0
+ requires forall j {:nowarn} :: 1 <= j < a.Length ==> a[j] == a[j-1]+2*j-1 // WISH: Same as above
{
// ...but the induction heuristics don't recognize the situation as one where
// applying induction would be profitable:
- assert forall n :: 0 <= n && n < a.Length ==> a[n] == n*n; // error reported
+ assert forall n :: 0 <= n < a.Length ==> a[n] == n*n; // error reported
}
}
@@ -171,7 +171,7 @@ abstract module OpaqueTypesWithParameters { }
method DifferentTypes(a: array<P<int>>, b: array<P<bool>>)
- requires a != null && b != null;
+ requires a != null && b != null
// If P were a known type, then it would also be known that P<int> and P<bool>
// would be different types, and then the types of 'a' and 'b' would be different,
// which would imply that the following postcondition would hold.
diff --git a/Test/dafny0/Matrix-OOB.dfy b/Test/dafny0/Matrix-OOB.dfy index 2e5c0366..d7aacd79 100644 --- a/Test/dafny0/Matrix-OOB.dfy +++ b/Test/dafny0/Matrix-OOB.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" /printTooltips "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This is a regression test: OOB errors for matrices used to be reported on the
diff --git a/Test/dafny0/Matrix-OOB.dfy.expect b/Test/dafny0/Matrix-OOB.dfy.expect index 94e77aa4..e2920445 100644 --- a/Test/dafny0/Matrix-OOB.dfy.expect +++ b/Test/dafny0/Matrix-OOB.dfy.expect @@ -1,3 +1,4 @@ +Matrix-OOB.dfy(12,10): Info: Selected triggers: {m[i, j]}
Matrix-OOB.dfy(12,26): Error: index 0 out of range
Execution trace:
(0,0): anon0
@@ -6,6 +7,7 @@ Execution trace: (0,0): anon0
Matrix-OOB.dfy(13,0): Error BP5003: A postcondition might not hold on this return path.
Matrix-OOB.dfy(12,10): Related location: This is the postcondition that might not hold.
+Matrix-OOB.dfy(12,33): Related location
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy index 505d9b74..3ffa5a23 100644 --- a/Test/dafny0/Modules1.dfy +++ b/Test/dafny0/Modules1.dfy @@ -125,7 +125,7 @@ abstract module Regression { predicate p<c,d>(m: map<c,d>)
lemma m<a,b>(m: map<a,b>)
- ensures exists m :: p(var m : map<a,b> := m; m);
+ ensures exists m {:nowarn} :: p(var m : map<a,b> := m; m) // WISH: Zeta-expanding the let binding would provide a good trigger
}
abstract module B
diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy index 3535f857..ba075fc3 100644 --- a/Test/dafny0/MultiSets.dfy +++ b/Test/dafny0/MultiSets.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
method test1()
@@ -295,3 +295,6 @@ lemma Set_and_Multiset_Cardinalities(x: int, y: int) assert |multiset{x,y}| == 2;
}
}
+
+// AutoTriggers explicitly removed, as simplifications of set expressions such
+// as x in {1,2} cause invalid terms to appear in the triggers
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index e0d6491b..93a16475 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.dfy @@ -210,7 +210,7 @@ class TwoState_C { ghost var data: int } // contexts are not allowed to allocate state. Callers of this ghost method will know
// that the postcondition is tantamount to 'false'.
ghost method TwoState0(y: int)
- ensures exists o: TwoState_C :: o != null && fresh(o)
+ ensures exists o: TwoState_C {:nowarn} :: o != null && fresh(o)
method TwoState_Main0() {
forall x { TwoState0(x); }
@@ -236,7 +236,7 @@ method X_Legit(c: TwoState_C) method TwoState_Main2()
{
forall x: int
- ensures exists o: TwoState_C :: o != null && fresh(o)
+ ensures exists o: TwoState_C {:nowarn} :: o != null && fresh(o)
{
TwoState0(x);
}
@@ -252,7 +252,7 @@ method TwoState_Main2() method TwoState_Main3()
{
forall x: int
- ensures exists o: TwoState_C :: o != null && fresh(o)
+ ensures exists o: TwoState_C {:nowarn} :: o != null && fresh(o)
{
assume false; // (there's no other way to achieve this forall-statement postcondition)
}
@@ -309,12 +309,12 @@ predicate ThProperty(step: nat, t: Nat, r: nat) {
match t
case Zero => true
- case Succ(o) => step>0 && exists ro:nat :: ThProperty(step-1, o, ro)
+ case Succ(o) => step>0 && exists ro:nat, ss | ss == step-1 :: ThProperty(ss, o, ro) //WISH: ss should be autogrnerated. Note that step is not a bound variable.
}
lemma Th(step: nat, t: Nat, r: nat)
requires t.Succ? && ThProperty(step, t, r)
// the next line follows from the precondition and the definition of ThProperty
- ensures exists ro:nat :: ThProperty(step-1, t.tail, ro)
+ ensures exists ro:nat, ss | ss == step-1 :: ThProperty(ss, t.tail, ro) //WISH same as above
{
}
diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy index 737dacd2..f8b3355d 100644 --- a/Test/dafny0/Predicates.dfy +++ b/Test/dafny0/Predicates.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
module A {
diff --git a/Test/dafny0/Predicates.dfy.expect b/Test/dafny0/Predicates.dfy.expect index 2d7ea6f1..36c9dfdd 100644 --- a/Test/dafny0/Predicates.dfy.expect +++ b/Test/dafny0/Predicates.dfy.expect @@ -17,10 +17,12 @@ Execution trace: (0,0): anon0
Predicates.dfy(164,4): Error BP5003: A postcondition might not hold on this return path.
Predicates.dfy(163,14): Related location: This is the postcondition that might not hold.
+Predicates.dfy(163,42): Related location
Execution trace:
(0,0): anon0
Predicates.dfy[Q1](154,4): Error BP5003: A postcondition might not hold on this return path.
Predicates.dfy[Q1](153,14): Related location: This is the postcondition that might not hold.
+Predicates.dfy[Q1](153,45): Related location
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/SeqFromArray.dfy b/Test/dafny0/SeqFromArray.dfy index 629c5045..cf889804 100644 --- a/Test/dafny0/SeqFromArray.dfy +++ b/Test/dafny0/SeqFromArray.dfy @@ -53,7 +53,7 @@ method L(a: array<int>, c: array<int>, n: nat) case A == C =>
assert forall i :: 0 <= i < h ==> A[i] == C[i];
case A == C =>
- assert forall i :: 0 <= i < h ==> a[n+i] == c[n+i];
+ assert forall i :: n <= i < n + h ==> a[i] == c[i];
case true =>
}
}
@@ -73,13 +73,13 @@ method M(a: array<int>, c: array<int>, m: nat, n: nat, k: nat, l: nat) } else if * {
assert forall i :: 0 <= i < n ==> A[i] == C[i];
} else if * {
- assert forall i :: k <= i < k+n ==> A[i-k] == C[i-k];
+ assert forall i {:nowarn} :: k <= i < k+n ==> A[i-k] == C[i-k];
} else if * {
assert forall i :: 0 <= i < n ==> A[i] == a[k+i];
} else if * {
assert forall i :: 0 <= i < n ==> C[i] == c[l+i];
} else if * {
- assert forall i :: 0 <= i < n ==> a[k+i] == c[l+i];
+ assert forall i {:nowarn} :: 0 <= i < n ==> a[k+i] == c[l+i];
}
}
case l+m <= c.Length && forall i :: 0 <= i < m ==> a[i] == c[l+i] =>
diff --git a/Test/dafny0/SeqFromArray.dfy.expect b/Test/dafny0/SeqFromArray.dfy.expect index 5395e298..af845d3e 100644 --- a/Test/dafny0/SeqFromArray.dfy.expect +++ b/Test/dafny0/SeqFromArray.dfy.expect @@ -1,6 +1,3 @@ -SeqFromArray.dfy(56,13): Warning: (!) No terms found to trigger on.
-SeqFromArray.dfy(76,17): Warning: (!) No terms found to trigger on.
-SeqFromArray.dfy(82,17): Warning: (!) No terms found to trigger on.
Dafny program verifier finished with 10 verified, 0 errors
Program compiled successfully
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index e9c2beb4..ba009b83 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" /autoTriggers:1 "%s" > "%t"
// RUN: %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"
// RUN: %diff "%s.expect" "%t"
@@ -35,11 +35,11 @@ class Node { }
method Sequence(s: seq<bool>, j: int, b: bool, c: bool) returns (t: seq<bool>)
- requires 10 <= |s|;
- requires 8 <= j && j < |s|;
- ensures |t| == |s|;
- ensures t[8] == s[8] || t[9] == s[9];
- ensures t[j] == b;
+ requires 10 <= |s|
+ requires 8 <= j < |s|
+ ensures |t| == |s|
+ ensures t[8] == s[8] || t[9] == s[9]
+ ensures t[j] == b
{
if (c) {
t := s[j := b];
@@ -49,14 +49,14 @@ class Node { }
method Max0(x: int, y: int) returns (r: int)
- ensures r == (if x < y then y else x);
+ ensures r == (if x < y then y else x)
{
if (x < y) { r := y; } else { r := x; }
}
method Max1(x: int, y: int) returns (r: int)
- ensures r == x || r == y;
- ensures x <= r && y <= r;
+ ensures r == x || r == y
+ ensures x <= r && y <= r
{
r := if x < y then y else x;
}
@@ -122,12 +122,12 @@ class Modifies { method C(b: bool)
modifies this;
- ensures !b ==> x == old(x) && next == old(next);
+ ensures !b ==> x == old(x) && next == old(next)
{
}
method D(p: Modifies, y: int)
- requires p != null;
+ requires p != null
{
if (y == 3) {
p.C(true); // error: may violate modifies clause
@@ -230,15 +230,15 @@ class InitCalls { method Init(y: int)
modifies this;
- ensures z == y;
+ ensures z == y
{
z := y;
}
method InitFromReference(q: InitCalls)
- requires q != null && 15 <= q.z;
+ requires q != null && 15 <= q.z
modifies this;
- ensures p == q;
+ ensures p == q
{
p := q;
}
@@ -265,35 +265,35 @@ class InitCalls { // --------------- some tests with quantifiers and ranges ----------------------
method QuantifierRange0<T>(a: seq<T>, x: T, y: T, N: int)
- requires 0 <= N && N <= |a|;
- requires forall k | 0 <= k && k < N :: a[k] != x;
- requires exists k | 0 <= k && k < N :: a[k] == y;
- ensures forall k :: 0 <= k && k < N ==> a[k] != x; // same as the precondition, but using ==> instead of |
- ensures exists k :: 0 <= k && k < N && a[k] == y; // same as the precondition, but using && instead of |
+ requires 0 <= N <= |a|
+ requires forall k | 0 <= k < N :: a[k] != x
+ requires exists k | 0 <= k < N :: a[k] == y
+ ensures forall k :: 0 <= k < N ==> a[k] != x; // same as the precondition, but using ==> instead of |
+ ensures exists k :: 0 <= k < N && a[k] == y; // same as the precondition, but using && instead of |
{
assert x != y;
}
method QuantifierRange1<T>(a: seq<T>, x: T, y: T, N: int)
- requires 0 <= N && N <= |a|;
- requires forall k :: 0 <= k && k < N ==> a[k] != x;
- requires exists k :: 0 <= k && k < N && a[k] == y;
- ensures forall k | 0 <= k && k < N :: a[k] != x; // same as the precondition, but using | instead of ==>
- ensures exists k | 0 <= k && k < N :: a[k] == y; // same as the precondition, but using | instead of &&
+ requires 0 <= N <= |a|
+ requires forall k :: 0 <= k < N ==> a[k] != x
+ requires exists k :: 0 <= k < N && a[k] == y
+ ensures forall k | 0 <= k < N :: a[k] != x; // same as the precondition, but using | instead of ==>
+ ensures exists k | 0 <= k < N :: a[k] == y; // same as the precondition, but using | instead of &&
{
assert x != y;
}
method QuantifierRange2<T(==)>(a: seq<T>, x: T, y: T, N: int)
- requires 0 <= N && N <= |a|;
- requires exists k | 0 <= k && k < N :: a[k] == y;
- ensures forall k | 0 <= k && k < N :: a[k] == y; // error
+ requires 0 <= N <= |a|
+ requires exists k | 0 <= k < N :: a[k] == y
+ ensures forall k | 0 <= k < N :: a[k] == y; // error
{
assert N != 0;
if (N == 1) {
- assert forall k | a[if 0 <= k && k < N then k else 0] != y :: k < 0 || N <= k; // in this case, the precondition holds trivially
+ assert forall k {:nowarn} | a[if 0 <= k < N then k else 0] != y :: k < 0 || N <= k; // in this case, the precondition holds trivially
}
- if (forall k | 0 <= k && k < N :: a[k] == x) {
+ if (forall k | 0 <= k < N :: a[k] == x) {
assert x == y;
}
}
@@ -301,8 +301,8 @@ method QuantifierRange2<T(==)>(a: seq<T>, x: T, y: T, N: int) // ----------------------- tests that involve sequences of boxes --------
ghost method M(zeros: seq<bool>, Z: bool)
- requires 1 <= |zeros| && Z == false;
- requires forall k :: 0 <= k && k < |zeros| ==> zeros[k] == Z;
+ requires 1 <= |zeros| && Z == false
+ requires forall k :: 0 <= k < |zeros| ==> zeros[k] == Z
{
var x := [Z];
assert zeros[0..1] == [Z];
@@ -312,7 +312,7 @@ class SomeType {
var x: int;
method DoIt(stack: seq<SomeType>)
- requires null !in stack;
+ requires null !in stack
modifies stack;
{
forall n | n in stack {
@@ -333,7 +333,7 @@ method TestSequences0() } else {
assert 2 in s;
assert 0 in s;
- assert exists n :: n in s && -3 <= n && n < 2;
+ assert exists n :: n in s && -3 <= n < 2;
}
assert 7 in s; // error
}
@@ -399,7 +399,7 @@ class Test { function F(b: bool): int
// The if-then-else in the following line was once translated incorrectly,
// incorrectly causing the postcondition to verify
- ensures if b then F(b) == 5 else F(b) == 6;
+ ensures if b then F(b) == 5 else F(b) == 6
{
5
}
@@ -430,10 +430,10 @@ class AttributeTests { }
method testAttributes0() returns (r: AttributeTests)
- ensures {:boolAttr true} true;
- ensures {:boolAttr false} true;
- ensures {:intAttr 0} true;
- ensures {:intAttr 1} true;
+ ensures {:boolAttr true} true
+ ensures {:boolAttr false} true
+ ensures {:intAttr 0} true
+ ensures {:intAttr 1} true
modifies {:boolAttr true} this`f;
modifies {:boolAttr false} this`f;
modifies {:intAttr 0} this`f;
@@ -541,7 +541,7 @@ method TestNotNot() // ----------------------- Assign-such-that statements -------
method AssignSuchThat0(a: int, b: int) returns (x: int, y: int)
- ensures x == a && y == b;
+ ensures x == a && y == b
{
if (*) {
x, y :| a <= x < a + 1 && b + a <= y + a && y <= b;
@@ -635,7 +635,7 @@ method AssignSuchThat9() returns (q: QuiteFinite) function method LetSuchThat_P(x: int): bool
method LetSuchThat0(ghost g: int)
- requires LetSuchThat_P(g);
+ requires LetSuchThat_P(g)
{
var t :| LetSuchThat_P(t); // assign-such-that statement
ghost var u := var q :| LetSuchThat_P(q); q + 1; // let-such-that expression
@@ -710,10 +710,10 @@ class GT { {
if (*) {
P0();
- assert forall x: GT :: x != null ==> !fresh(x); // error: method P2 may have allocated stuff
+ assert forall x: GT {:nowarn} :: x != null ==> !fresh(x); // error: method P2 may have allocated stuff
} else {
P1();
- assert forall x: GT :: x != null ==> !fresh(x); // fine, because the ghost method does not allocate anything
+ assert forall x: GT {:nowarn} :: x != null ==> !fresh(x); // fine, because the ghost method does not allocate anything
}
}
}
@@ -777,20 +777,20 @@ module GenericPick { var x :| x in s; x
}
function SeqPick3<U>(s: seq<U>): U
- requires exists i :: 0 <= i < |s|
+ requires exists i {:nowarn} :: 0 <= i < |s|
{
EquivalentWaysOfSayingSequenceIsNonempty(s); // I wish this wasn't needed; see comment near Seq#Length axioms in DafnyPrelude.bpl
var x :| x in s; x
}
function SeqPick4<U>(s: seq<U>): U
- requires exists i :: 0 <= i < |s|
+ requires exists i {:nowarn} :: 0 <= i < |s|
{
var i :| 0 <= i < |s|; s[i]
}
lemma EquivalentWaysOfSayingSequenceIsNonempty<U>(s: seq<U>)
requires s != []
|| |s| != 0
- || exists i :: 0 <= i < |s|
+ || exists i {:nowarn} :: 0 <= i < |s|
ensures exists x :: x in s
{
assert s[0] in s;
diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index eee0d4f1..4bd12096 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -107,6 +107,7 @@ Execution trace: (0,0): anon3
SmallTests.dfy(296,2): Error BP5003: A postcondition might not hold on this return path.
SmallTests.dfy(290,10): Related location: This is the postcondition that might not hold.
+SmallTests.dfy(290,40): Related location
Execution trace:
(0,0): anon0
(0,0): anon18_Else
@@ -117,8 +118,8 @@ Execution trace: SmallTests.dfy(338,11): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon8_Then
- (0,0): anon7
+ (0,0): anon7_Then
+ (0,0): anon6
SmallTests.dfy(345,9): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/TriggerInPredicate.dfy.expect b/Test/dafny0/TriggerInPredicate.dfy.expect index 1cbd4034..b3fb9cc0 100644 --- a/Test/dafny0/TriggerInPredicate.dfy.expect +++ b/Test/dafny0/TriggerInPredicate.dfy.expect @@ -1,5 +1,5 @@ -TriggerInPredicate.dfy(6,32): Info: Not generating triggers for {A(x, y)}.
-TriggerInPredicate.dfy(6,32): Info: Not generating triggers for {z}.
+TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "A(x, y)".
+TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "z".
TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.
TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.
diff --git a/Test/dafny0/columns.dfy b/Test/dafny0/columns.dfy index e36142be..72c9ab81 100644 --- a/Test/dafny0/columns.dfy +++ b/Test/dafny0/columns.dfy @@ -3,8 +3,10 @@ // Dafny counts columns from 0, but Boogie from one, so for a while there were small bugs with that.
+predicate P(x: int)
+
static method A(x:int) requires x > 0 { // error os 's'
- assert (forall y :: y > x ==> y > 100); // error on '('
+ assert (forall y: int :: P(y)); // error on '('
assert x != 1; // error on '!'
assert x in {}; // error on 'i'
}
diff --git a/Test/dafny0/columns.dfy.expect b/Test/dafny0/columns.dfy.expect index 295ca351..0a99be69 100644 --- a/Test/dafny0/columns.dfy.expect +++ b/Test/dafny0/columns.dfy.expect @@ -1,18 +1,12 @@ -columns.dfy(6,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
-columns.dfy(7,9): Error: assertion violation
+columns.dfy(8,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+columns.dfy(9,9): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon3_Then
- (0,0): anon2
-columns.dfy(8,11): Error: assertion violation
+columns.dfy(10,11): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon3_Then
- (0,0): anon2
-columns.dfy(9,11): Error: assertion violation
+columns.dfy(11,11): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon3_Then
- (0,0): anon2
-Dafny program verifier finished with 1 verified, 3 errors
+Dafny program verifier finished with 2 verified, 3 errors
diff --git a/Test/dafny0/fun-with-slices.dfy b/Test/dafny0/fun-with-slices.dfy new file mode 100644 index 00000000..3d8da242 --- /dev/null +++ b/Test/dafny0/fun-with-slices.dfy @@ -0,0 +1,19 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This test was contributed by Bryan. It has shown some instabilities in the past.
+
+method seqIntoArray<A>(s: seq<A>, a: array<A>, index: nat)
+ requires a != null
+ requires index + |s| <= a.Length
+ modifies a
+ ensures a[..] == old(a[0..index]) + s + old(a[index + |s|..]) {
+ var i := index;
+
+ while i < index + |s|
+ invariant index <= i <= index + |s| <= a.Length
+ invariant a[..] == old(a[0..index]) + s[0..(i-index)] + old(a[i..]) {
+ a[i] := s[i - index];
+ i := i + 1;
+ }
+}
diff --git a/Test/dafny0/fun-with-slices.dfy.expect b/Test/dafny0/fun-with-slices.dfy.expect new file mode 100644 index 00000000..069e7767 --- /dev/null +++ b/Test/dafny0/fun-with-slices.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy b/Test/dafny0/snapshots/Snapshots5.run.dfy index e0f3b16b..096df53c 100644 --- a/Test/dafny0/snapshots/Snapshots5.run.dfy +++ b/Test/dafny0/snapshots/Snapshots5.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots5.dfy" > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots5.dfy" /autoTriggers:1 > "%t"
// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy.expect b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect index 8148a8cf..8cc44882 100644 --- a/Test/dafny0/snapshots/Snapshots5.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect @@ -1,3 +1,7 @@ +Snapshots5.v0.dfy(10,12): Warning: /!\ No terms found to trigger on.
+Snapshots5.v0.dfy(13,10): Warning: /!\ No terms found to trigger on.
+Snapshots5.v0.dfy(20,12): Warning: /!\ No terms found to trigger on.
+Snapshots5.v0.dfy(26,11): Warning: /!\ No terms found to trigger on.
Processing command (at Snapshots5.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
@@ -10,6 +14,11 @@ Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: tru >>> DoNothingToAssert
Dafny program verifier finished with 3 verified, 0 errors
+Snapshots5.v1.dfy(10,12): Warning: /!\ No terms found to trigger on.
+Snapshots5.v1.dfy(13,10): Warning: /!\ No terms found to trigger on.
+Snapshots5.v1.dfy(20,12): Warning: /!\ No terms found to trigger on.
+Snapshots5.v1.dfy(22,10): Warning: /!\ No terms found to trigger on.
+Snapshots5.v1.dfy(27,11): Warning: /!\ No terms found to trigger on.
Processing command (at Snapshots5.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy index 0940d9e7..374555b0 100644 --- a/Test/dafny1/FindZero.dfy +++ b/Test/dafny1/FindZero.dfy @@ -3,7 +3,7 @@ method FindZero(a: array<int>) returns (r: int)
requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+ requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
ensures 0 <= r ==> r < a.Length && a[r] == 0;
ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
{
@@ -20,7 +20,7 @@ method FindZero(a: array<int>) returns (r: int) lemma Lemma(a: array<int>, k: int, m: int)
requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+ requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
requires 0 <= k;
requires k < a.Length ==> m <= a[k];
ensures forall i :: k <= i < k+m && i < a.Length ==> a[i] != 0;
@@ -36,7 +36,7 @@ lemma Lemma(a: array<int>, k: int, m: int) method FindZero_GhostLoop(a: array<int>) returns (r: int)
requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+ requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
ensures 0 <= r ==> r < a.Length && a[r] == 0;
ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
{
@@ -63,7 +63,7 @@ method FindZero_GhostLoop(a: array<int>) returns (r: int) method FindZero_Assert(a: array<int>) returns (r: int)
requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i-1 && i < a.Length ==> a[i-1]-1 <= a[i];
+ requires forall i {:nowarn} :: 0 <= i-1 && i < a.Length ==> a[i-1]-1 <= a[i];
ensures 0 <= r ==> r < a.Length && a[r] == 0;
ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
{
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index 3445dab9..e2cd4ade 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -53,7 +53,7 @@ class IntegerInduction { }
lemma DoItAllInOneGo()
- ensures (forall n :: 0 <= n ==>
+ ensures (forall n {:split false} :: 0 <= n ==> // WISH reenable quantifier splitting here. This will only work once we generate induction hypotheses at the Dafny level.
SumOfCubes(n) == Gauss(n) * Gauss(n) &&
2 * Gauss(n) == n*(n+1));
{
@@ -148,11 +148,11 @@ class IntegerInduction { // Proving the "<==" case is simple; it's the "==>" case that requires induction.
// The example uses an attribute that requests induction on just "j". However, the proof also
// goes through by applying induction on both bound variables.
- function method IsSorted(s: seq<int>): bool
- ensures IsSorted(s) ==> (forall i,j {:induction j} :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]);
+ function method IsSorted(s: seq<int>): bool //WISH remove autotriggers false
+ ensures IsSorted(s) ==> (forall i,j {:induction j} {:autotriggers false} :: 0 <= i < j < |s| ==> s[i] <= s[j]);
ensures (forall i,j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) ==> IsSorted(s);
{
- (forall i :: 1 <= i && i < |s| ==> s[i-1] <= s[i])
+ (forall i {:nowarn} :: 1 <= i && i < |s| ==> s[i-1] <= s[i])
}
}
diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy index 319bb8d0..bd654db5 100644 --- a/Test/dafny1/MoreInduction.dfy +++ b/Test/dafny1/MoreInduction.dfy @@ -83,12 +83,12 @@ lemma LemmaOne(n: int) {
}
-lemma LemmaAll_Neg()
- ensures forall n :: NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
+lemma LemmaAll_Neg() //FIXME I don't understand the comment below; what trigger?
+ ensures forall n {:nowarn} :: NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
{
}
-lemma LemmaOne_Neg(n: int)
+lemma LemmaOne_Neg(n: int) //FIXME What trigger?
ensures NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
{
}
diff --git a/Test/dafny1/MoreInduction.dfy.expect b/Test/dafny1/MoreInduction.dfy.expect index 5de0ace6..7da5e2ec 100644 --- a/Test/dafny1/MoreInduction.dfy.expect +++ b/Test/dafny1/MoreInduction.dfy.expect @@ -1,5 +1,6 @@ MoreInduction.dfy(78,0): Error BP5003: A postcondition might not hold on this return path.
MoreInduction.dfy(77,10): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(77,32): Related location
Execution trace:
(0,0): anon0
MoreInduction.dfy(83,0): Error BP5003: A postcondition might not hold on this return path.
@@ -8,6 +9,7 @@ Execution trace: (0,0): anon0
MoreInduction.dfy(88,0): Error BP5003: A postcondition might not hold on this return path.
MoreInduction.dfy(87,10): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(87,43): Related location
Execution trace:
(0,0): anon0
MoreInduction.dfy(93,0): Error BP5003: A postcondition might not hold on this return path.
diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy index 94223cba..3d2a5d78 100644 --- a/Test/dafny1/PriorityQueue.dfy +++ b/Test/dafny1/PriorityQueue.dfy @@ -12,7 +12,7 @@ class PriorityQueue { reads this, Repr;
{
MostlyValid() &&
- (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])
+ (forall j {:nowarn} :: 2 <= j && j <= n ==> a[j/2] <= a[j])
}
predicate MostlyValid()
@@ -50,8 +50,8 @@ class PriorityQueue { method SiftUp(k: int)
requires 1 <= k && k <= n;
requires MostlyValid();
- requires (forall j :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);
- requires (forall j :: 1 <= j && j <= n ==> j/2 != k); // k is a leaf
+ requires (forall j {:nowarn} :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);
+ requires (forall j {:nowarn} :: 1 <= j && j <= n ==> j/2 != k); // k is a leaf
modifies a;
ensures Valid();
{
@@ -59,8 +59,8 @@ class PriorityQueue { assert MostlyValid();
while (1 < i)
invariant i <= k && MostlyValid();
- invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
- invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
+ invariant (forall j {:nowarn} :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
+ invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
{
if (a[i/2] <= a[i]) {
return;
@@ -85,8 +85,8 @@ class PriorityQueue { method SiftDown(k: int)
requires 1 <= k;
requires MostlyValid();
- requires (forall j :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);
- requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);
+ requires (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);
+ requires (forall j {:nowarn} :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);
// Alternatively, the line above can be expressed as:
// requires (forall j :: 1 <= k/2 && j/2 == k && j <= n ==> a[j/2/2] <= a[j]);
modifies a;
@@ -95,8 +95,8 @@ class PriorityQueue { var i := k;
while (2*i <= n) // while i is not a leaf
invariant 1 <= i && MostlyValid();
- invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
- invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);
+ invariant (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
+ invariant (forall j {:nowarn} :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);
{
var smallestChild;
if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {
@@ -127,7 +127,7 @@ class PriorityQueue_Alternative { reads this, Repr;
{
MostlyValid() &&
- (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])
+ (forall j {:nowarn} :: 2 <= j && j <= n ==> a[j/2] <= a[j])
}
predicate MostlyValid()
@@ -164,7 +164,7 @@ class PriorityQueue_Alternative { method SiftUp()
requires MostlyValid();
- requires (forall j :: 2 <= j && j <= n && j != n ==> a[j/2] <= a[j]);
+ requires (forall j {:nowarn} :: 2 <= j && j <= n && j != n ==> a[j/2] <= a[j]);
modifies a;
ensures Valid();
{
@@ -172,8 +172,8 @@ class PriorityQueue_Alternative { assert MostlyValid();
while (1 < i)
invariant i <= n && MostlyValid();
- invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
- invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
+ invariant (forall j {:nowarn} :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
+ invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
{
if (a[i/2] <= a[i]) {
return;
@@ -197,15 +197,15 @@ class PriorityQueue_Alternative { method SiftDown()
requires MostlyValid();
- requires (forall j :: 4 <= j && j <= n ==> a[j/2] <= a[j]);
+ requires (forall j {:nowarn} :: 4 <= j && j <= n ==> a[j/2] <= a[j]);
modifies a;
ensures Valid();
{
var i := 1;
while (2*i <= n) // while i is not a leaf
invariant 1 <= i && MostlyValid();
- invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
- invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
+ invariant (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
+ invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
{
var smallestChild;
if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {
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/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy index 72a22cfd..4c702674 100644 --- a/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy +++ b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy @@ -93,8 +93,8 @@ method Search(a: array<int>) returns (p: int, q: int) invariant forall j :: 0 <= j < d.Length ==>
(d[j] == -1 && forall k :: 0 <= k < i ==> a[k] != j) ||
(0 <= d[j] < i && a[d[j]] == j);
- invariant p == q ==> IsDuplicate(a, p);
- invariant forall k :: 0 <= k < i && IsPrefixDuplicate(a, i, a[k]) ==> p == q == a[k];
+ invariant p == q ==> IsDuplicate(a, p); //WISH remove the trigger on the next line
+ invariant forall k {:trigger old(a[k])} :: 0 <= k < i && IsPrefixDuplicate(a, i, a[k]) ==> p == q == a[k];
decreases a.Length - i;
{
var k := d[a[i]];
diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy index 2aa14db7..72250f99 100644 --- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy +++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy @@ -164,7 +164,7 @@ class Node { invariant 0 <= t < h && Nexxxt(t, S) == tortoise && Nexxxt(h, S) == hare;
// What follows of the invariant is for proving termination:
invariant h == 1 + 2*t && t <= A + B;
- invariant forall k :: 0 <= k < t ==> Nexxxt(k, S) != Nexxxt(1+2*k, S);
+ invariant forall k {:nowarn} :: 0 <= k < t ==> Nexxxt(k, S) != Nexxxt(1+2*k, S);
decreases A + B - t;
{
if hare == null || hare.next == null {
@@ -225,7 +225,7 @@ class Node { requires 0 <= a && 1 <= b;
requires forall k,l :: 0 <= k < l < a ==> Nexxxt(k, S) != Nexxxt(l, S);
requires Nexxxt(a, S) == null || Nexxxt(a, S).Nexxxt(b, S) == Nexxxt(a, S);
- ensures exists T :: 0 <= T < a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S);
+ ensures exists T {:nowarn} :: 0 <= T < a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S);
{
if Nexxxt(a, S) == null {
Lemma_NullIsTerminal(1+2*a, S);
diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy index 6bd06965..ea75c196 100644 --- a/Test/dafny3/GenericSort.dfy +++ b/Test/dafny3/GenericSort.dfy @@ -36,7 +36,7 @@ abstract module Sort { requires a != null && 0 <= low <= high <= a.Length
reads a
{
- forall i :: low < i < high ==> O.Leq(a[i-1], a[i])
+ forall i {:nowarn} :: low < i < high ==> O.Leq(a[i-1], a[i])
}
// ...but we show that property to imply all pairs to be sorted. The proof of this
// lemma uses the transitivity property.
diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy index 89fa6cc8..0074b742 100644 --- a/Test/dafny3/InductionVsCoinduction.dfy +++ b/Test/dafny3/InductionVsCoinduction.dfy @@ -80,7 +80,7 @@ lemma SAppendIsAssociative(a:Stream, b:Stream, c:Stream) {
forall k:nat { SAppendIsAssociativeK(k, a, b, c); }
// assert for clarity only, postcondition follows directly from it
- assert (forall k:nat :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c)));
+ assert (forall k:nat {:autotriggers false} :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c))); //FIXME: Should Dafny generate a trigger here? If so then which one?
}
// Equivalent proof using the colemma syntax.
diff --git a/Test/dafny4/Bug60.dfy b/Test/dafny4/Bug60.dfy index 5340ad6b..c433451c 100644 --- a/Test/dafny4/Bug60.dfy +++ b/Test/dafny4/Bug60.dfy @@ -9,5 +9,5 @@ method Main() print (s, m), "\n";
print (|s|, |m|), "\n";
print(set s | s in m), "\n";
- print (forall x :: x in (map [1:=10, 2:=20]) ==> x > 0), "\n";
-}
\ No newline at end of file + print (forall x {:nowarn} :: x in (map [1:=10, 2:=20]) ==> x > 0), "\n";
+}
diff --git a/Test/dafny4/Bug63.dfy b/Test/dafny4/Bug63.dfy index 86aad232..39cbae1b 100644 --- a/Test/dafny4/Bug63.dfy +++ b/Test/dafny4/Bug63.dfy @@ -8,6 +8,6 @@ method M() method Client()
{
- assume forall o: object :: o != null ==> false;
+ assume forall o: object {:nowarn} :: o != null ==> false;
M();
-}
\ No newline at end of file +}
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
diff --git a/Test/dafny4/Primes.dfy b/Test/dafny4/Primes.dfy index b0bb7527..fd64b45e 100644 --- a/Test/dafny4/Primes.dfy +++ b/Test/dafny4/Primes.dfy @@ -3,7 +3,7 @@ predicate IsPrime(n: int)
{
- 2 <= n && forall m :: 2 <= m < n ==> n % m != 0
+ 2 <= n && forall m {:nowarn} :: 2 <= m < n ==> n % m != 0 // WISH It would be great to think about the status of modulo as a trigger
}
// The following theorem shows that there is an infinite number of primes
@@ -167,8 +167,8 @@ lemma Composite(c: int) returns (a: int, b: int) calc {
true;
!IsPrime(c);
- !(2 <= c && forall m :: 2 <= m < c ==> c % m != 0);
- exists m :: 2 <= m < c && c % m == 0;
+ !(2 <= c && forall m {:nowarn} :: 2 <= m < c ==> c % m != 0);
+ exists m {:nowarn} :: 2 <= m < c && c % m == 0;
}
a :| 2 <= a < c && c % a == 0;
b := c / a;
@@ -194,7 +194,7 @@ lemma LargestElementExists(s: set<int>) var s' := s;
while true
invariant s' != {} && s' <= s;
- invariant forall x,y :: x in s' && y in s - s' ==> y <= x;
+ invariant forall x,y {:nowarn} :: x in s' && y in s - s' ==> y <= x;
decreases s';
{
var x :| x in s'; // pick something
diff --git a/Test/triggers/constructors-cause-matching-loops.dfy b/Test/triggers/constructors-cause-matching-loops.dfy new file mode 100644 index 00000000..61e6a66b --- /dev/null +++ b/Test/triggers/constructors-cause-matching-loops.dfy @@ -0,0 +1,11 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file is just a small test to check that constructors do cause loops
+
+datatype Nat = Zero | Succ(x: Nat)
+function f(n: Nat): Nat
+
+method M() {
+ assert forall s :: true || f(Succ(s)) == f(s);
+}
diff --git a/Test/triggers/constructors-cause-matching-loops.dfy.expect b/Test/triggers/constructors-cause-matching-loops.dfy.expect new file mode 100644 index 00000000..e7a671ab --- /dev/null +++ b/Test/triggers/constructors-cause-matching-loops.dfy.expect @@ -0,0 +1,6 @@ +constructors-cause-matching-loops.dfy(10,9): Info: Selected triggers: {Succ(s)}
+ Rejected triggers:
+ {f(s)} (may loop with "f(Succ(s))")
+ {f(Succ(s))} (more specific than {Succ(s)})
+
+Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect index 501cfa51..1214536d 100644 --- a/Test/triggers/function-applications-are-triggers.dfy.expect +++ b/Test/triggers/function-applications-are-triggers.dfy.expect @@ -1,8 +1,8 @@ function-applications-are-triggers.dfy(9,9): Info: Selected triggers: {P.requires(f)}
-function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f.requires(10)}:
+function-applications-are-triggers.dfy(10,9): Info: For expression "P(f) ==> f.requires(10)":
Selected triggers:
{f(10)}, {f.requires(10)}, {P(f)}
-function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f(10) == 0}:
+function-applications-are-triggers.dfy(10,9): Info: For expression "P(f) ==> f(10) == 0":
Selected triggers:
{f(10)}, {f.requires(10)}, {P(f)}
function-applications-are-triggers.dfy(11,9): Info: Selected triggers:
diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect index 705c2a8c..65ea0d79 100644 --- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect +++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect @@ -2,16 +2,16 @@ loop-detection-is-not-too-strict.dfy(15,9): Info: Selected triggers: {P(y, x)}, {P(x, y)}
loop-detection-is-not-too-strict.dfy(18,9): Info: Selected triggers:
{P(y, x)}, {P(x, y)}
-loop-detection-is-not-too-strict.dfy(21,9): Warning: Selected triggers: {P(x, y)} (may loop with {P(x, y + 1)})
- (!) Suppressing loops would leave this expression without triggers.
+loop-detection-is-not-too-strict.dfy(21,9): Warning: Selected triggers: {P(x, y)} (may loop with "P(x, y + 1)")
+ /!\ Suppressing loops would leave this expression without triggers.
loop-detection-is-not-too-strict.dfy(26,9): Info: Selected triggers: {Q(x)}
loop-detection-is-not-too-strict.dfy(27,9): Info: Selected triggers: {Q(x)}
loop-detection-is-not-too-strict.dfy(28,9): Info: Selected triggers:
{P(x, z)}, {P(x, 1)}
loop-detection-is-not-too-strict.dfy(33,9): Info: Selected triggers: {Q(x)}
loop-detection-is-not-too-strict.dfy(34,9): Info: Selected triggers: {Q(x)}
-loop-detection-is-not-too-strict.dfy(36,9): Warning: Selected triggers: {Q(x)} (may loop with {Q(if z > 1 then x else 3 * z + 1)})
- (!) Suppressing loops would leave this expression without triggers.
+loop-detection-is-not-too-strict.dfy(36,9): Warning: Selected triggers: {Q(x)} (may loop with "Q(if z > 1 then x else 3 * z + 1)")
+ /!\ Suppressing loops would leave this expression without triggers.
loop-detection-is-not-too-strict.dfy(39,9): Info: Selected triggers: {Q(x)}
Dafny program verifier finished with 4 verified, 0 errors
diff --git a/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect index ce62d868..a32e4a60 100644 --- a/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect +++ b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect @@ -1,6 +1,6 @@ -loop-detection-looks-at-ranges-too.dfy(11,17): Warning: Selected triggers: {P(x)} (may loop with {P(x + 1)})
- (!) Suppressing loops would leave this expression without triggers.
-loop-detection-looks-at-ranges-too.dfy(13,17): Warning: Selected triggers: {P(x)} (may loop with {P(x + 1)})
- (!) Suppressing loops would leave this expression without triggers.
+loop-detection-looks-at-ranges-too.dfy(11,17): Warning: Selected triggers: {P(x)} (may loop with "P(x + 1)")
+ /!\ Suppressing loops would leave this expression without triggers.
+loop-detection-looks-at-ranges-too.dfy(13,17): Warning: Selected triggers: {P(x)} (may loop with "P(x + 1)")
+ /!\ Suppressing loops would leave this expression without triggers.
Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect index 804a0116..eba8c179 100644 --- a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect +++ b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect @@ -1,37 +1,37 @@ loop-detection-messages--unit-tests.dfy(11,9): Info: Selected triggers: {f(f(i))}
- Rejected triggers: {f(i)} (may loop with {f(f(i))})
-loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (may loop with {f(i + 1)})
- (!) Suppressing loops would leave this expression without triggers.
-loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(i)} (may loop with {f(i + 1)})
-loop-detection-messages--unit-tests.dfy(15,9): Info: For expression {false ==> f(i) == f(i + 1)}:
+ Rejected triggers: {f(i)} (may loop with "f(f(i))")
+loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (may loop with "f(i + 1)")
+ /!\ Suppressing loops would leave this expression without triggers.
+loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(i)} (may loop with "f(i + 1)")
+loop-detection-messages--unit-tests.dfy(15,9): Info: For expression "false ==> f(i) == f(i + 1)":
Selected triggers: {g(i)}
- Rejected triggers: {f(i)} (may loop with {f(i + 1)})
-loop-detection-messages--unit-tests.dfy(15,9): Info: For expression {false ==> f(i) == g(i)}:
+ Rejected triggers: {f(i)} (may loop with "f(i + 1)")
+loop-detection-messages--unit-tests.dfy(15,9): Info: For expression "false ==> f(i) == g(i)":
Selected triggers:
{g(i)}, {f(i)}
-loop-detection-messages--unit-tests.dfy(16,9): Warning: For expression {false ==> f(i) == f(i + 1)}:
- Selected triggers: {f(i)} (may loop with {f(i + 1)})
- (!) Suppressing loops would leave this expression without triggers.
-loop-detection-messages--unit-tests.dfy(16,9): Info: For expression {false ==> f(i) == f(i)}:
+loop-detection-messages--unit-tests.dfy(16,9): Warning: For expression "false ==> f(i) == f(i + 1)":
+ Selected triggers: {f(i)} (may loop with "f(i + 1)")
+ /!\ Suppressing loops would leave this expression without triggers.
+loop-detection-messages--unit-tests.dfy(16,9): Info: For expression "false ==> f(i) == f(i)":
Selected triggers: {f(i)}
-loop-detection-messages--unit-tests.dfy(17,9): Info: For expression {false ==> f(i) == f(i + 1)}:
- Selected triggers: {f(i)} (may loop with {f(i + 1)})
-loop-detection-messages--unit-tests.dfy(17,9): Info: For expression {false ==> f(i) == f(i)}:
+loop-detection-messages--unit-tests.dfy(17,9): Info: For expression "false ==> f(i) == f(i + 1)":
+ Selected triggers: {f(i)} (may loop with "f(i + 1)")
+loop-detection-messages--unit-tests.dfy(17,9): Info: For expression "false ==> f(i) == f(i)":
Selected triggers: {f(i)}
loop-detection-messages--unit-tests.dfy(19,9): Info: Selected triggers: {f(i)}
-loop-detection-messages--unit-tests.dfy(20,9): Warning: (!) No terms found to trigger on.
-loop-detection-messages--unit-tests.dfy(21,9): Info: Not generating triggers for {false ==> f(i + 1) == 0}.
+loop-detection-messages--unit-tests.dfy(20,9): Warning: /!\ No terms found to trigger on.
+loop-detection-messages--unit-tests.dfy(21,9): Info: Not generating triggers for "false ==> f(i + 1) == 0". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.
loop-detection-messages--unit-tests.dfy(23,9): Info: Selected triggers: {f(j), f(i)}
-loop-detection-messages--unit-tests.dfy(24,9): Warning: (!) No trigger covering all quantified variables found.
-loop-detection-messages--unit-tests.dfy(25,9): Info: For expression {false ==> f(i) == f(i)}:
+loop-detection-messages--unit-tests.dfy(24,9): Warning: /!\ No trigger covering all quantified variables found.
+loop-detection-messages--unit-tests.dfy(25,9): Info: For expression "false ==> f(i) == f(i)":
Selected triggers: {g(j), f(i)}
-loop-detection-messages--unit-tests.dfy(25,9): Info: For expression {false ==> g(j) == 0}:
+loop-detection-messages--unit-tests.dfy(25,9): Info: For expression "false ==> g(j) == 0":
Selected triggers: {g(j), f(i)}
-loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression {false ==> f(i) == f(i)}:
- (!) No trigger covering all quantified variables found.
-loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression {false ==> g(j + 1) == 0}:
- (!) No trigger covering all quantified variables found.
-loop-detection-messages--unit-tests.dfy(27,9): Info: Not generating triggers for {false ==> f(i) == f(i)}.
-loop-detection-messages--unit-tests.dfy(28,9): Info: Not generating triggers for {false ==> f(i) == f(i)}.
+loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression "false ==> f(i) == f(i)":
+ /!\ No trigger covering all quantified variables found.
+loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression "false ==> g(j + 1) == 0":
+ /!\ No trigger covering all quantified variables found.
+loop-detection-messages--unit-tests.dfy(27,9): Info: Not generating triggers for "false ==> f(i) == f(i)". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.
+loop-detection-messages--unit-tests.dfy(28,9): Info: Not generating triggers for "false ==> f(i) == f(i)".
Dafny program verifier finished with 4 verified, 0 errors
diff --git a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect index 58094110..e900c1f9 100644 --- a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect +++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect @@ -1,10 +1,10 @@ looping-is-hard-to-decide-modulo-equality.dfy(21,9): Info: Selected triggers:
{h(h(c, j), j)}, {h(c, i)}, {c in sc}
- Rejected triggers: {h(c, j)} (may loop with {h(h(c, j), j)})
+ Rejected triggers: {h(c, j)} (may loop with "h(h(c, j), j)")
looping-is-hard-to-decide-modulo-equality.dfy(26,9): Info: Selected triggers: {f(x)}
Rejected triggers: {g(f(x))} (more specific than {f(x)})
looping-is-hard-to-decide-modulo-equality.dfy(31,9): Info: Selected triggers:
{old(f(f(c)))}, {f(c)}, {c in sc}
- Rejected triggers: {old(f(c))} (may loop with {old(f(f(c)))})
+ Rejected triggers: {old(f(c))} (may loop with "old(f(f(c)))")
Dafny program verifier finished with 9 verified, 0 errors
diff --git a/Test/triggers/matrix-accesses-are-triggers.dfy.expect b/Test/triggers/matrix-accesses-are-triggers.dfy.expect index 35df02f5..572fc41f 100644 --- a/Test/triggers/matrix-accesses-are-triggers.dfy.expect +++ b/Test/triggers/matrix-accesses-are-triggers.dfy.expect @@ -1,5 +1,5 @@ -matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (may loop with {m[j, i + 1]})
- (!) Suppressing loops would leave this expression without triggers.
+matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (may loop with "m[j, i + 1]")
+ /!\ Suppressing loops would leave this expression without triggers.
matrix-accesses-are-triggers.dfy(8,81): Error: index 0 out of range
Execution trace:
(0,0): anon0
diff --git a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect index 313d7c16..7388a911 100644 --- a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect +++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect @@ -2,14 +2,14 @@ old-is-a-special-case-for-triggers.dfy(15,10): Info: Selected triggers: {old(f(c))}, {c in sc}
old-is-a-special-case-for-triggers.dfy(20,10): Info: Selected triggers:
{old(f(f(c)))}, {f(c)}, {c in sc}
- Rejected triggers: {old(f(c))} (may loop with {old(f(f(c)))})
+ Rejected triggers: {old(f(c))} (may loop with "old(f(f(c)))")
old-is-a-special-case-for-triggers.dfy(21,10): Info: Selected triggers:
{f(g(c))}, {g(f(c))}, {old(f(g(c)))}, {old(g(f(c)))}, {old(f(f(c)))}, {c in sc}
Rejected triggers:
- {g(c)} (may loop with {g(f(c))})
- {f(c)} (may loop with {f(g(c))})
- {old(g(c))} (may loop with {old(g(f(c)))})
- {old(f(c))} (may loop with {old(f(f(c)))}, {old(f(g(c)))})
+ {g(c)} (may loop with "g(f(c))")
+ {f(c)} (may loop with "f(g(c))")
+ {old(g(c))} (may loop with "old(g(f(c)))")
+ {old(f(c))} (may loop with "old(f(f(c)))", "old(f(g(c)))")
old-is-a-special-case-for-triggers.dfy(25,10): Info: Selected triggers:
{old(f(c))}, {f(c)}, {c in sc}
Rejected triggers: {old(g(f(c)))} (more specific than {old(f(c))})
diff --git a/Test/triggers/regression-tests.dfy.expect b/Test/triggers/regression-tests.dfy.expect index a03810fb..e780e966 100644 --- a/Test/triggers/regression-tests.dfy.expect +++ b/Test/triggers/regression-tests.dfy.expect @@ -1,3 +1,3 @@ -regression-tests.dfy(16,5): Warning: (!) No terms found to trigger on.
+regression-tests.dfy(16,5): Warning: /!\ No terms found to trigger on.
Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy new file mode 100644 index 00000000..98cea392 --- /dev/null +++ b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy @@ -0,0 +1,48 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// The examples below work nicely with /autoTriggers:0, but break when we ass
+// /autoTriggers.
+
+// The issue is that the axioms for sequences are missing a number of facts,
+// which was not a problem before /autoTriggers and /stricterTriggers, but has
+// become one. Here are examples of things that Dafny won’t prove with
+// /autoTriggers (I would expect it wouldn’t with stricterTriggers either,
+// though the second example is trickier than the first):
+
+method M(a: seq<int>) {
+ if * {
+ // This fails; it needs the following axiom:
+ // axiom (forall<T> s: Seq T ::
+ // { Seq#Take(s, Seq#Length(s)) }
+ // Seq#Take(s, Seq#Length(s)) == s);
+ assume forall x :: x in a ==> x > 0;
+ assert forall x :: x in a[..|a|] ==> x > 0;
+ } else if * {
+ // This fails; it needs the following axiom:
+ // axiom (forall<T> s: Seq T, i: int ::
+ // { Seq#Index(s, i) }
+ // 0 <= i && i < Seq#Length(s) ==>
+ // Seq#Contains(s, Seq#Index(s, i)));
+ assume forall x :: x in a ==> x > 0;
+ assert forall i | 0 <= i < |a| :: a[i] > 0;
+ } else if * {
+ assume |a| > 3;
+ assume forall x | x in a[..3] :: x > 1;
+ // This fails, but here it's a lot harder to know what a good axiom would be.
+ assert forall x | x in a[..2] :: x > 1;
+ }
+}
+
+
+// In the first case, the Boogie version is
+//
+// Seq#Contains(Seq#Take(a#0, Seq#Length(a#0)), $Box(x#0_1)) ⟹ x#0_1 > 0
+//
+// And of course Z3 picks $Box(x#0_1). The third case is similar.
+//
+// The problem is of course that knowing that x ∈ a[..2] doesn’t magically give
+// you a term that matches x ∈ a[..3]. One could imagine introducing an extra
+// symbol in the translation to put x and a together for triggering purposes,
+// but that would have the same sort of issues as adding symbols for arithmetic
+// operators.
diff --git a/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy.expect b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy.expect new file mode 100644 index 00000000..d48840b8 --- /dev/null +++ b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy.expect @@ -0,0 +1,31 @@ +some-proofs-only-work-without-autoTriggers.dfy(19,11): Info: Selected triggers: {x in a}
+some-proofs-only-work-without-autoTriggers.dfy(20,11): Info: Selected triggers: {x in a[..|a|]}
+some-proofs-only-work-without-autoTriggers.dfy(27,11): Info: Selected triggers: {x in a}
+some-proofs-only-work-without-autoTriggers.dfy(28,11): Info: Selected triggers: {a[i]}
+some-proofs-only-work-without-autoTriggers.dfy(31,11): Info: Selected triggers: {x in a[..3]}
+some-proofs-only-work-without-autoTriggers.dfy(33,11): Info: Selected triggers: {x in a[..2]}
+some-proofs-only-work-without-autoTriggers.dfy(20,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon22_Then
+ (0,0): anon3
+ (0,0): anon23_Then
+ (0,0): anon5
+some-proofs-only-work-without-autoTriggers.dfy(28,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon25_Then
+ (0,0): anon9
+ (0,0): anon26_Then
+ (0,0): anon27_Then
+ (0,0): anon13
+some-proofs-only-work-without-autoTriggers.dfy(33,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon28_Then
+ (0,0): anon29_Then
+ (0,0): anon17
+ (0,0): anon30_Then
+ (0,0): anon19
+
+Dafny program verifier finished with 1 verified, 3 errors
diff --git a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect index f5e47454..1a143edb 100644 --- a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect +++ b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect @@ -1,10 +1,10 @@ -some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (may loop with {s[x + 1]})
- (!) Suppressing loops would leave this expression without triggers.
-some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> s[x + 1] > 0}:
- Selected triggers: {s[x]} (may loop with {s[x + 1]})
- (!) Suppressing loops would leave this expression without triggers.
-some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> x + 2 !in s}:
- Selected triggers: {s[x]} (may loop with {x + 2 !in s})
- (!) Suppressing loops would leave this expression without triggers.
+some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (may loop with "s[x + 1]")
+ /!\ Suppressing loops would leave this expression without triggers.
+some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression "x in s ==> s[x + 1] > 0":
+ Selected triggers: {s[x]} (may loop with "s[x + 1]")
+ /!\ Suppressing loops would leave this expression without triggers.
+some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression "x in s ==> x + 2 !in s":
+ Selected triggers: {s[x]} (may loop with "x + 2 !in s")
+ /!\ Suppressing loops would leave this expression without triggers.
Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/triggers/splitting-picks-the-right-tokens.dfy.expect b/Test/triggers/splitting-picks-the-right-tokens.dfy.expect index af274e75..f01ed1a0 100644 --- a/Test/triggers/splitting-picks-the-right-tokens.dfy.expect +++ b/Test/triggers/splitting-picks-the-right-tokens.dfy.expect @@ -1,14 +1,14 @@ -splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {Id(x) > 1}:
+splitting-picks-the-right-tokens.dfy(9,11): Info: For expression "Id(x) > 1":
Selected triggers: {Id(x)}
-splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {x > 2}:
+splitting-picks-the-right-tokens.dfy(9,11): Info: For expression "x > 2":
Selected triggers: {Id(x)}
-splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {x > -1}:
+splitting-picks-the-right-tokens.dfy(9,11): Info: For expression "x > -1":
Selected triggers: {Id(x)}
-splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> Id(x) > 1}:
+splitting-picks-the-right-tokens.dfy(16,11): Info: For expression "x > 0 ==> Id(x) > 1":
Selected triggers: {Id(x)}
-splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> x > 2}:
+splitting-picks-the-right-tokens.dfy(16,11): Info: For expression "x > 0 ==> x > 2":
Selected triggers: {Id(x)}
-splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> x > -1}:
+splitting-picks-the-right-tokens.dfy(16,11): Info: For expression "x > 0 ==> x > -1":
Selected triggers: {Id(x)}
splitting-picks-the-right-tokens.dfy(20,12): Error BP5002: A precondition for this call might not hold.
splitting-picks-the-right-tokens.dfy(16,11): Related location: This is the precondition that might not hold.
diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect index 58c8dd2b..a8bb2345 100644 --- a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect +++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect @@ -1,32 +1,32 @@ splitting-triggers-recovers-expressivity.dfy(12,10): Info: Selected triggers: {Q(i)}
- Rejected triggers: {P(i)} (may loop with {P(i + 1)})
+ Rejected triggers: {P(i)} (may loop with "P(i + 1)")
splitting-triggers-recovers-expressivity.dfy(17,11): Info: Selected triggers: {Q(j)}
- Rejected triggers: {P(j)} (may loop with {P(j + 1)})
+ Rejected triggers: {P(j)} (may loop with "P(j + 1)")
splitting-triggers-recovers-expressivity.dfy(26,10): Info: Selected triggers: {Q(i)}
- Rejected triggers: {P(i)} (may loop with {P(i + 1)})
+ Rejected triggers: {P(i)} (may loop with "P(i + 1)")
splitting-triggers-recovers-expressivity.dfy(33,11): Info: Selected triggers: {Q(j)}
- Rejected triggers: {P(j)} (may loop with {P(j + 1)})
-splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i)}:
+ Rejected triggers: {P(j)} (may loop with "P(j + 1)")
+splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression "P(i)":
Selected triggers:
{Q(i)}, {P(i)}
-splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {!Q(i)}:
+splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression "!Q(i)":
Selected triggers:
{Q(i)}, {P(i)}
-splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i + 1)}:
+splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression "P(i + 1)":
Selected triggers: {Q(i)}
- Rejected triggers: {P(i)} (may loop with {P(i + 1)})
-splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> P(j)}:
+ Rejected triggers: {P(i)} (may loop with "P(i + 1)")
+splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression "j >= 0 ==> P(j)":
Selected triggers:
{Q(j)}, {P(j)}
-splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> Q(j) ==> P(j + 1)}:
+splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression "j >= 0 ==> Q(j) ==> P(j + 1)":
Selected triggers: {Q(j)}
- Rejected triggers: {P(j)} (may loop with {P(j + 1)})
-splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> Q(i)}:
+ Rejected triggers: {P(j)} (may loop with "P(j + 1)")
+splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression "i >= 0 ==> Q(i)":
Selected triggers:
{P(i)}, {Q(i)}
-splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> P(i) ==> P(i + 1)}:
+splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression "i >= 0 ==> P(i) ==> P(i + 1)":
Selected triggers:
- {P(i)} (may loop with {P(i + 1)}), {Q(i)}
+ {P(i)} (may loop with "P(i + 1)"), {Q(i)}
splitting-triggers-recovers-expressivity.dfy(12,63): Error BP5003: A postcondition might not hold on this return path.
splitting-triggers-recovers-expressivity.dfy(12,10): Related location: This is the postcondition that might not hold.
Execution trace:
diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect index c8e1a5fa..27548ac9 100644 --- a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect +++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect @@ -1,11 +1,11 @@ -splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression {y > 0}:
- (!) No terms found to trigger on.
-splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression {y < 0}:
- (!) No terms found to trigger on.
-splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression {y > 0}:
- (!) No terms found to trigger on.
-splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression {y < 0}:
- (!) No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression "y > 0":
+ /!\ No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression "y < 0":
+ /!\ No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression "y > 0":
+ /!\ No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression "y < 0":
+ /!\ No terms found to trigger on.
splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error BP5002: A precondition for this call might not hold.
splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: This is the precondition that might not hold.
splitting-triggers-yields-better-precondition-related-errors.dfy(7,34): Related location
diff --git a/Test/triggers/suppressing-warnings-behaves-properly.dfy b/Test/triggers/suppressing-warnings-behaves-properly.dfy new file mode 100644 index 00000000..237269e5 --- /dev/null +++ b/Test/triggers/suppressing-warnings-behaves-properly.dfy @@ -0,0 +1,21 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file checks that suppressing warnings works properly
+
+predicate f(x: int)
+predicate g(x: int)
+
+method M() {
+ assert forall n :: n >= 0 || n < 0;
+ assert forall n {:nowarn} :: n >= 0 || n < 0;
+ assert forall n {:autotriggers false} :: n >= 0 || n < 0;
+
+ assert forall n: nat :: (n != 0) == f(n) || true;
+ assert forall n: nat {:nowarn} :: (n != 0) == f(n) || true;
+ assert forall n: nat {:autotriggers false} :: (n != 0) == f(n) || true;
+
+ assert forall n: nat :: f(n) == f(n+1) || g(n) || true;
+ assert forall n: nat {:nowarn} :: (n != 0) == f(n) || true;
+ assert forall n: nat {:autotriggers false} :: (n != 0) == f(n) || true;
+}
diff --git a/Test/triggers/suppressing-warnings-behaves-properly.dfy.expect b/Test/triggers/suppressing-warnings-behaves-properly.dfy.expect new file mode 100644 index 00000000..124984b1 --- /dev/null +++ b/Test/triggers/suppressing-warnings-behaves-properly.dfy.expect @@ -0,0 +1,14 @@ +suppressing-warnings-behaves-properly.dfy(10,9): Warning: /!\ No terms found to trigger on.
+suppressing-warnings-behaves-properly.dfy(11,9): Info: (Suppressed warning) No terms found to trigger on.
+suppressing-warnings-behaves-properly.dfy(12,9): Info: Not generating triggers for "n >= 0 || n < 0". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.
+suppressing-warnings-behaves-properly.dfy(14,9): Info: Selected triggers: {f(n)}
+suppressing-warnings-behaves-properly.dfy(15,9): Warning: Selected triggers: {f(n)}
+ /!\ There is no warning here to suppress.
+suppressing-warnings-behaves-properly.dfy(16,9): Info: Not generating triggers for "(n != 0) == f(n) || true". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.
+suppressing-warnings-behaves-properly.dfy(18,9): Info: Selected triggers: {g(n)}
+ Rejected triggers: {f(n)} (may loop with "f(n + 1)")
+suppressing-warnings-behaves-properly.dfy(19,9): Warning: Selected triggers: {f(n)}
+ /!\ There is no warning here to suppress.
+suppressing-warnings-behaves-properly.dfy(20,9): Info: Not generating triggers for "(n != 0) == f(n) || true". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.
+
+Dafny program verifier finished with 4 verified, 0 errors
diff --git a/Test/triggers/useless-triggers-are-removed.dfy.expect b/Test/triggers/useless-triggers-are-removed.dfy.expect index 2e9bbedf..d6b49a9e 100644 --- a/Test/triggers/useless-triggers-are-removed.dfy.expect +++ b/Test/triggers/useless-triggers-are-removed.dfy.expect @@ -5,11 +5,11 @@ useless-triggers-are-removed.dfy(16,11): Info: Selected triggers: {f(x)} {h(f(x))} (more specific than {f(x)})
{g(f(x))} (more specific than {f(x)})
useless-triggers-are-removed.dfy(20,11): Info: Selected triggers: {f(f(x))}
- Rejected triggers: {f(x)} (may loop with {f(f(x))})
+ Rejected triggers: {f(x)} (may loop with "f(f(x))")
useless-triggers-are-removed.dfy(23,11): Info: Selected triggers:
{g(f(x)), g(y)}, {f(y), f(x)}
Rejected triggers:
- {g(y), f(x)} (may loop with {g(f(y))}, {g(f(x))})
+ {g(y), f(x)} (may loop with "g(f(y))", "g(f(x))")
{g(f(x)), g(f(y))} (more specific than {g(f(x)), f(y)}, {g(f(y)), f(x)}, {f(y), f(x)})
{g(f(x)), f(y)} (more specific than {f(y), f(x)})
{g(f(y)), f(x)} (more specific than {f(y), f(x)})
diff --git a/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect index 6b152262..6c3e4853 100644 --- a/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect +++ b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect @@ -1,16 +1,16 @@ -wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression {0 <= f(n)}:
+wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression "0 <= f(n)":
Selected triggers: {f(n)}
Rejected triggers: {P(f(n))} (more specific than {f(n)})
-wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression {P(f(n))}:
+wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression "P(f(n))":
Selected triggers: {f(n)}
Rejected triggers: {P(f(n))} (more specific than {f(n)})
-wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c != null}:
+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression "c != null":
Selected triggers:
{c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}
-wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c' != null}:
+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression "c' != null":
Selected triggers:
{c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}
-wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c.x == c'.x}:
+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression "c.x == c'.x":
Selected triggers:
{c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}
diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy index d5551d82..bc3b5baf 100644 --- a/Test/vacid0/Composite.dfy +++ b/Test/vacid0/Composite.dfy @@ -68,7 +68,7 @@ class Composite { // sets child.parent to this:
ensures child.parent == this;
// leaves everything in S+U valid:
- ensures (forall c :: c in S+U ==> c.Valid(S+U));
+ ensures (forall c {:autotriggers false} :: c in S+U ==> c.Valid(S+U)); // We can't generate a trigger for this at the moment; if we did, we would still need to prevent TrSplitExpr from translating c in S+U to S[c] || U[c].
{
if (left == null) {
left := child;
diff --git a/Test/wishlist/exists-b-exists-not-b.dfy b/Test/wishlist/exists-b-exists-not-b.dfy index 711c5611..2573b2f2 100644 --- a/Test/wishlist/exists-b-exists-not-b.dfy +++ b/Test/wishlist/exists-b-exists-not-b.dfy @@ -5,6 +5,6 @@ // otherwise, trigger splitting prevents `exists b :: b || not b` from verifying
method M() {
- assert exists b: bool :: b; // WISH
- assert exists b: bool :: !b; // WISH
+ assert exists b : bool {:nowarn} :: b; // WISH
+ assert exists b : bool {:nowarn} :: !b; // WISH
}
diff --git a/Test/wishlist/sequences-s0-in-s.dfy b/Test/wishlist/sequences-s0-in-s.dfy index 20127917..c221dbb2 100644 --- a/Test/wishlist/sequences-s0-in-s.dfy +++ b/Test/wishlist/sequences-s0-in-s.dfy @@ -21,5 +21,5 @@ method InSeqTriggers(s: seq<int>, i: nat) method InSeqNoAutoTriggers(s: seq<int>, i: nat)
requires forall x {:autotriggers false} :: x in s ==> x > 0;
requires |s| > 0 {
- assert s[0] > 0; // Works
+ assert s[0] > 0; // Works (Z3 matches on $Box above)
}
|