From 69c320b225825eb2adf2ae899f88588a10fd27fe Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 19 Aug 2015 20:05:47 -0700
Subject: Refactored and improved bounds discovery

---
 Test/dafny0/ISets.dfy | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'Test/dafny0')

diff --git a/Test/dafny0/ISets.dfy b/Test/dafny0/ISets.dfy
index bb0230f4..703039c8 100644
--- a/Test/dafny0/ISets.dfy
+++ b/Test/dafny0/ISets.dfy
@@ -4,7 +4,7 @@
 ghost method M()
 {
    ghost var s := iset{2};
-   // test "in
+   // test "in"
    if(2 in s)
    {
    }
@@ -35,6 +35,9 @@ ghost method m1() {
  assert s2 - s3 == iset{3}; // set difference
 
  assert (iset x | x in s2 :: x+1) == iset{2,3,4}; // set comprehension
+ assert 17 in (iset x: int | true :: x); // set comprehension
+
+ assert (imap x: int | true :: x+1)[14] == 15;
 }
 
 
-- 
cgit v1.2.3