diff options
Diffstat (limited to 'Test/wishlist')
| -rw-r--r-- | Test/wishlist/exists-b-exists-not-b.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
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
}
|