1 files changed, 14 insertions, 1 deletions
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index b4dc6599..ac7286e9 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -308,7 +308,7 @@ method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int)
   }
 }
 
-// ----------------------- tests that involve sequences of boxed booleans --------
+// ----------------------- tests that involve sequences of boxes --------
 
 ghost method M(zeros: seq<bool>, Z: bool)
   requires 1 <= |zeros| && Z == false;
@@ -317,3 +317,16 @@ ghost method M(zeros: seq<bool>, Z: bool)
   var x := [Z];
   assert zeros[0..1] == [Z];
 }
+
+class SomeType
+{
+  var x: int;
+  method DoIt(stack: seq<SomeType>)
+    modifies stack;
+  {
+    // the following line once gave rise to a crash in the translation
+    foreach (n in stack) {
+      n.x := 10;
+    }
+  }
+}