2 files changed, 21 insertions, 8 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 48b242ac..07efab03 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -180,10 +180,10 @@ Execution trace:
 Definedness.dfy(86,5): Error: possible violation of function precondition
 Execution trace:
     (0,0): anon0
-Definedness.dfy(86,10): Error: target object may be null
+Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause
 Execution trace:
     (0,0): anon0
-Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause
+Definedness.dfy(86,10): Error: target object may be null
 Execution trace:
     (0,0): anon0
 Definedness.dfy(87,10): Error: possible violation of function precondition
@@ -749,22 +749,22 @@ Basics.dfy(235,10): Error: when left-hand sides 0 and 1 refer to the same locati
 Execution trace:
     (0,0): anon0
 
-Dafny program verifier finished with 34 verified, 11 errors
+Dafny program verifier finished with 37 verified, 11 errors
 
 -------------------- ControlStructures.dfy --------------------
-ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
+ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
 Execution trace:
     (0,0): anon0
     (0,0): anon6_Else
     (0,0): anon7_Else
-    (0,0): anon8_Then
-ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
+    (0,0): anon8_Else
+    (0,0): anon9_Then
+ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
 Execution trace:
     (0,0): anon0
     (0,0): anon6_Else
     (0,0): anon7_Else
-    (0,0): anon8_Else
-    (0,0): anon9_Then
+    (0,0): anon8_Then
 ControlStructures.dfy(14,3): Error: missing case in case statement: Purple
 Execution trace:
     (0,0): anon0
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index b451cdf1..6b1b366d 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -249,3 +249,16 @@ method notQuiteSwap3(c: CC, d: CC)
   c.x, d.x := 4, c.y;
   c.x, c.y := 3, c.y;
 }
+
+// ---------------------------
+// regression tests of things that were once errors
+
+method InlineMultisetFormingExpr(s: seq<int>)
+  ensures MSFE(s);
+predicate MSFE(s: seq<int>)
+{
+  multiset(s) == multiset(s)
+}
+
+copredicate CoPredTypeCheck(n: int)
+  requires n != 0;