From 95a42a224dff8eae383d93beb37a3da6a28bb0f3 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 28 Aug 2015 20:50:50 -0700 Subject: Suppress many warnings in the test suite. We already have separate tests for those, and we want the output to be the same with and without /autoTriggers. --- Test/wishlist/exists-b-exists-not-b.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Test/wishlist') 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 } -- cgit v1.2.3