2 files changed, 51 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 64c43c87..78982f01 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -96,5 +96,11 @@ Execution trace:
 Dafny program verifier finished with 5 verified, 3 errors
 
 -------------------- TypeParameters.dfy --------------------
+TypeParameters.dfy(41,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    (0,0): anon0
+TypeParameters.dfy(63,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    (0,0): anon0
 
-Dafny program verifier finished with 3 verified, 0 errors
+Dafny program verifier finished with 7 verified, 2 errors
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index 3f57f369..794f2f95 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -19,3 +19,47 @@ class C<U> {
 
   function G<Y>(): Y;
 }
+
+class SetTest {
+  method Add<T>(s: set<T>, x: T) returns (t: set<T>)
+    ensures t == s + {x};
+  {
+    t := s + {x};
+  }
+
+  method Good()
+  {
+    var s := {2, 5, 3};
+    call t := Add(s, 7);
+    assert {5,7,2,3} == t;
+  }
+
+  method Bad()
+  {
+    var s := {2, 50, 3};
+    call t := Add(s, 7);
+    assert {5,7,2,3} == t;  // error
+  }
+}
+
+class SequenceTest {
+  method Add<T>(s: seq<T>, x: T) returns (t: seq<T>)
+    ensures t == s + [x];
+  {
+    t := s + [x];
+  }
+
+  method Good()
+  {
+    var s := [2, 5, 3];
+    call t := Add(s, 7);
+    assert [2,5,3,7] == t;
+  }
+
+  method Bad()
+  {
+    var s := [2, 5, 3];
+    call t := Add(s, 7);
+    assert [2,5,7,3] == t || [2,5,3] == t;
+  }
+}