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