From 6dfa82655aa7cb35bae6904e05887cdf960c6319 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Mon, 13 Jul 2015 11:55:06 -0700
Subject: Fix multiple tests that relied on z3 triggering on $Box

Found by enabling auto-generated triggers and looking for failing tests
---
 Test/dafny0/DeterministicPick.dfy | 1 +
 1 file changed, 1 insertion(+)

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

diff --git a/Test/dafny0/DeterministicPick.dfy b/Test/dafny0/DeterministicPick.dfy
index a7ec55fa..13db1bfc 100644
--- a/Test/dafny0/DeterministicPick.dfy
+++ b/Test/dafny0/DeterministicPick.dfy
@@ -29,6 +29,7 @@ module Attempt_Smallest refines Specification {
     var z :| z in s;
     if s != {z} {
       var s' := s - {z};
+      assert forall y :: y in s ==> y in s' || y == z;
       ASmallestToPick(s');
     }
   }
-- 
cgit v1.2.3