From 3d45aa05a023c092167d938a72adf78cf1f76fdf Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Fri, 28 Aug 2015 20:47:42 -0700
Subject: Clarify a comment

---
 Test/wishlist/sequences-s0-in-s.dfy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Test/wishlist')

diff --git a/Test/wishlist/sequences-s0-in-s.dfy b/Test/wishlist/sequences-s0-in-s.dfy
index 20127917..c221dbb2 100644
--- a/Test/wishlist/sequences-s0-in-s.dfy
+++ b/Test/wishlist/sequences-s0-in-s.dfy
@@ -21,5 +21,5 @@ method InSeqTriggers(s: seq<int>, i: nat)
 method InSeqNoAutoTriggers(s: seq<int>, i: nat)
   requires forall x {:autotriggers false} :: x in s ==> x > 0;
   requires |s| > 0 {
-    assert s[0] > 0; // Works
+    assert s[0] > 0; // Works (Z3 matches on $Box above)
 }
-- 
cgit v1.2.3