Merge

3 files changed, 27 insertions, 1 deletions

diff --git a/Test/dafny0/DisplayExpressions.dfy b/Test/dafny0/DisplayExpressions.dfy
new file mode 100644
index 00000000..767cfcdb
--- /dev/null
+++ b/Test/dafny0/DisplayExpressions.dfy
@@ -0,0 +1,21 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

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

+method M()

+{

+  var m := map[];

+}

+

+method N()

+{

+  var n := multiset{};

+}

+

+method O()

+{

+  var o := [];

+}

+

+method P()

+{

+  var p := {};

+}

diff --git a/Test/dafny0/DisplayExpressions.dfy.expect b/Test/dafny0/DisplayExpressions.dfy.expect
new file mode 100644
index 00000000..1867ff3a
--- /dev/null
+++ b/Test/dafny0/DisplayExpressions.dfy.expect
@@ -0,0 +1,5 @@
+DisplayExpressions.dfy(5,11): Error: the type of this map constructor is underspecified, but it cannot be an arbitrary type.
+DisplayExpressions.dfy(10,11): Error: the type of this collection constructor is underspecified, but it cannot be an arbitrary type.
+DisplayExpressions.dfy(15,11): Error: the type of this collection constructor is underspecified, but it cannot be an arbitrary type.
+DisplayExpressions.dfy(20,11): Error: the type of this collection constructor is underspecified, but it cannot be an arbitrary type.
+4 resolution/type errors detected in DisplayExpressions.dfy
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 4c4d01d8..703cbaf1 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -669,7 +669,7 @@ ghost method LetSuchThat3(n: int) returns (xx: int, yy: Lindgren) {
   xx := var x :| x in multiset{3, 3, 2, 3}; x+10;

   xx := var x :| x in map[5 := 10, 6 := 12]; x+10;

   xx := var x :| x in [n, n, 2]; x+10;

-  xx := var x :| x in map[]; x+10;  // error

+  xx := var x :| x in (var m : map<int,int> := map[]; m); x+10;  // error

 }

 

 // ------------- ghost loops only modify ghost fields