diff options
| -rw-r--r-- | Source/Dafny/Resolver.cs | 7 | ||||
| -rw-r--r-- | Test/dafny4/Regression0.dfy | 13 | ||||
| -rw-r--r-- | Test/dafny4/Regression0.dfy.expect | 4 |
3 files changed, 22 insertions, 2 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 58984b9b..2f2b5a54 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4574,8 +4574,11 @@ namespace Microsoft.Dafny } else if (a is CollectionTypeProxy) {
if (b is CollectionTypeProxy) {
- a.T = b;
- return UnifyTypes(((CollectionTypeProxy)a).Arg, ((CollectionTypeProxy)b).Arg);
+ var argUnificationSuccess = UnifyTypes(((CollectionTypeProxy)a).Arg, ((CollectionTypeProxy)b).Arg);
+ if (argUnificationSuccess) {
+ a.T = b;
+ }
+ return argUnificationSuccess;
} else if (b is OperationTypeProxy) {
var proxy = (OperationTypeProxy)b;
if (proxy.AllowSeq && proxy.AllowSetVarieties && proxy.AllowISet) {
diff --git a/Test/dafny4/Regression0.dfy b/Test/dafny4/Regression0.dfy new file mode 100644 index 00000000..be092261 --- /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"];
+ if * {
+ assert exists n :: n in s && n != 1;
+ } else {
+ assert "2" in s;
+ }
+}
diff --git a/Test/dafny4/Regression0.dfy.expect b/Test/dafny4/Regression0.dfy.expect new file mode 100644 index 00000000..9d1e3019 --- /dev/null +++ b/Test/dafny4/Regression0.dfy.expect @@ -0,0 +1,4 @@ +Regression0.dfy(7,15): Error: All elements of display must be of the same type (got string, but type of previous elements is int)
+Regression0.dfy(9,28): Error: the type of this variable is underspecified
+Regression0.dfy(11,15): Error: second argument to "in" must be a set, multiset, or sequence with elements of type string, or a map with domain string (instead got ?)
+3 resolution/type errors detected in Regression0.dfy
|