Refactored and improved bounds discovery

1 files changed, 4 insertions, 1 deletions

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;

 }