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.

1 files changed, 1 insertions, 1 deletions

diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy
index d5551d82..bc3b5baf 100644
--- a/Test/vacid0/Composite.dfy
+++ b/Test/vacid0/Composite.dfy
@@ -68,7 +68,7 @@ class Composite {
     // sets child.parent to this:

     ensures child.parent == this;

     // leaves everything in S+U valid:

-    ensures (forall c :: c in S+U ==> c.Valid(S+U));

+    ensures (forall c {:autotriggers false} :: c in S+U ==> c.Valid(S+U)); // We can't generate a trigger for this at the moment; if we did, we would still need to prevent TrSplitExpr from translating c in S+U to S[c] || U[c].

   {

     if (left == null) {

       left := child;