diff options
Diffstat (limited to 'Test/dafny4/Regression0.dfy')
| -rw-r--r-- | Test/dafny4/Regression0.dfy | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/Test/dafny4/Regression0.dfy b/Test/dafny4/Regression0.dfy new file mode 100644 index 00000000..666d9575 --- /dev/null +++ b/Test/dafny4/Regression0.dfy @@ -0,0 +1,13 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This once crashed Dafny
+
+method M() {
+ var s := [1, "2"]; // error: all elements must have the same type
+ if * {
+ assert exists n :: n in s && n != 1; // the type of n is inferred to be int
+ } else {
+ assert "2" in s; // error: since the type of s wasn't determined
+ }
+}
|