diff options
| -rw-r--r-- | Test/wishlist/sequences-s0-in-s.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
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)
}
|