Merge commit 'df5c5f5'

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

+  }

+}