Merge.

3 files changed, 21 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;

 }

 

 

diff --git a/Test/dafny4/Regression0.dfy b/Test/dafny4/Regression0.dfy
new file mode 100644
index 00000000..be092261
--- /dev/null
+++ b/Test/dafny4/Regression0.dfy
@@ -0,0 +1,13 @@
+// RUN: %dafny /compile:0  "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This once crashed Dafny

+

+method M() {

+  var s := [1, "2"];

+  if * {

+    assert exists n :: n in s && n != 1;

+  } else {

+    assert "2" in s;

+  }

+}

diff --git a/Test/dafny4/Regression0.dfy.expect b/Test/dafny4/Regression0.dfy.expect
new file mode 100644
index 00000000..9d1e3019
--- /dev/null
+++ b/Test/dafny4/Regression0.dfy.expect
@@ -0,0 +1,4 @@
+Regression0.dfy(7,15): Error: All elements of display must be of the same type (got string, but type of previous elements is int)

+Regression0.dfy(9,28): Error: the type of this variable is underspecified

+Regression0.dfy(11,15): Error: second argument to "in" must be a set, multiset, or sequence with elements of type string, or a map with domain string (instead got ?)

+3 resolution/type errors detected in Regression0.dfy