1 files changed, 16 insertions, 0 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 696a583f..60314836 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -626,3 +626,19 @@ module GhostAllocationTests {
   {
   }
 }
+
+// ------------------------- underspecified types ------------------------------
+
+module UnderspecifiedTypes {
+  method M(S: set<int>) {
+    var n, p, T0 :| 12 <= n && n in T0 && 10 <= p && p in T0 && T0 <= S && p % 2 != n % 2;
+    var T1 :| 12 in T1 && T1 <= S;
+    var T2 :| T2 <= S && 12 in T2;
+    var T3 :| 120 in T3;  // error: underspecified type
+    var T3'0: set<int> :| 120 in T3'0;
+    var T3'1: multiset<int> :| 120 in T3'1;
+    var T3'2: map<int,bool> :| 120 in T3'2;
+    var T3'3: seq<int> :| 120 in T3'3;
+    var T4 :| T4 <= S;
+  }
+}