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/dafny0/Comprehensions.dfy | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'Test/dafny0/Comprehensions.dfy')

diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy
index d0436815..dd83e46c 100644
--- a/Test/dafny0/Comprehensions.dfy
+++ b/Test/dafny0/Comprehensions.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method M()
@@ -19,18 +19,18 @@ datatype D = A | B
 // have to run the resulting program to check that the compiler is doing the right thing.
 method Main()
 {
-  var q := set i,j | 0 <= i && i < 10 && 0 <= j && j < 3 :: i+j;
+  var q := set i,j | 0 <= i < 10 && 0 <= j < 3 :: i+j;
   PrintSet(q);
   q := set b: bool | true :: if b then 3 else 7;
   var d := set b:D | true;
-  var test := forall d:D :: d == A || d == B;
+  var test := forall d:D {:nowarn} :: d == A || d == B; // Ignoring the warning as we're only compiling here
   PrintSet(q);
   var m := set k | k in q :: 2*k;
   PrintSet(m);
   PrintSet(set k | k in q && k % 2 == 0);
   var sq := [30, 40, 20];
-  PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);
-  var bb := forall k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i == 17;
+  PrintSet(set k, i | k in sq && 0 <= i < k && i % 7 == 0 :: k + i);
+  var bb := forall k, i {:nowarn} | k in sq && 0 <= i < k && i % 7 == 0 :: k + i == 17; // Ignoring the warning as we're only compiling here
 }
 
 method PrintSet<T>(s: set<T>) {
-- 
cgit v1.2.3