From 95a42a224dff8eae383d93beb37a3da6a28bb0f3 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
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/dafny4/Bug60.dfy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Test/dafny4/Bug60.dfy')

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";
+}
-- 
cgit v1.2.3