Removed specContextOnly parameter from ResolveStatement.

Moved all bounds discovery to resolution pass 1.

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

   }

 }