diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-28 20:47:42 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-28 20:47:42 -0700 |
| commit | 3d45aa05a023c092167d938a72adf78cf1f76fdf (patch) | |
| tree | 75cad7c290c6ec2c5136ce49b5ac79b67245ea4c /Test/wishlist | |
| parent | 2db858bf6e72e521b49aa0ae3a993dc943b8c875 (diff) | |
Clarify a comment
Diffstat (limited to 'Test/wishlist')
| -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)
}
|