Fix issue #60

4 files changed, 29 insertions, 2 deletions

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index dbeb6d0f..726731e3 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -28,7 +28,9 @@ namespace Dafny
         d[t] = true;

       return new Set<T>(d);

     }

-

+    public int Length {

+      get { return dict.Count; }

+    }

     public IEnumerable<T> Elements {

       get {

         return dict.Keys;

@@ -357,6 +359,9 @@ namespace Dafny
       }

       return new Map<U, V>(d);

     }

+    public int Length {

+      get { return dict.Count; }

+    }

     public bool Equals(Map<U, V> other) {

       foreach (U u in dict.Keys) {

         V v1, v2;

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index e1d8c95f..f95084be 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -8537,7 +8537,7 @@ namespace Microsoft.Dafny
                 break;

               case BinaryExpr.ResolvedOpcode.InMap:

                 if (whereIsBv == 0 && e1.Type.AsMapType.Finite) {

-                  bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));

+                  bounds.Add(new ComprehensionExpr.MapBoundedPool(e1));

                   foundBoundsForBv = true;

                   if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

                 }

diff --git a/Test/dafny4/Bug60.dfy b/Test/dafny4/Bug60.dfy
new file mode 100644
index 00000000..5340ad6b
--- /dev/null
+++ b/Test/dafny4/Bug60.dfy
@@ -0,0 +1,13 @@
+// RUN: %dafny /compile:3  "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This method can be used to test compilation.

+method Main()

+{

+    var s := {2, 3};

+    var m := map[2 := 20, 3 := 30];

+    print (s, m), "\n";

+    print (|s|, |m|), "\n";

+    print(set s | s in m), "\n";

+    print (forall x :: x in (map [1:=10, 2:=20]) ==> x > 0), "\n";

+}
\ No newline at end of file
diff --git a/Test/dafny4/Bug60.dfy.expect b/Test/dafny4/Bug60.dfy.expect
new file mode 100644
index 00000000..3dccafa1
--- /dev/null
+++ b/Test/dafny4/Bug60.dfy.expect
@@ -0,0 +1,9 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

+Program compiled successfully

+Running...

+

+({2, 3}, map[2 := 20, 3 := 30])
+(2, 2)
+{2, 3}
+True