Fixed bug in type unification

2 files changed, 17 insertions, 0 deletions

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