Fix issue 5554 soundness (#5874)

### Description
This PR updates the Dafny CS runtime to use BigIntegers instead of int32
when retrieving the number of elements in a multiset. As this number may
be over INT_MAX, this change avoids potential overflows. This is similar
to what is done in the Java runtime.

### How has this been tested?
A test was added:
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyRuntime/DafnyRuntime.cs

@@ -547,7 +547,9 @@ public override string ToString() {
       return s + "}";
     }
     public static bool IsProperSubsetOf(IMultiSet<T> th, IMultiSet<T> other) {
-      return th.Count < other.Count && IsSubsetOf(th, other);
+      // Be sure to use ElementCount to avoid casting into 32 bits
+      // integers that could lead to overflows (see https://github.com/dafny-lang/dafny/issues/5554)
+      return th.ElementCount < other.ElementCount && IsSubsetOf(th, other);
     }
     public static bool IsSubsetOf(IMultiSet<T> th, IMultiSet<T> other) {
       var a = FromIMultiSet(th);

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy

@@ -0,0 +1,13 @@
+// RUN:  %dafny -compile:4 -compileTarget:cs "%s"
+
+datatype MultisetContainer = EmptySet | BooleanMultiset(containerSet: multiset<bool>)
+
+method Main() {
+    var initialMultiset := multiset{false};
+
+    for iteration := 0 to 31 {
+        var multisetInstance := BooleanMultiset(initialMultiset); 
+        initialMultiset := initialMultiset + multisetInstance.containerSet;  
+    }
+    print initialMultiset > initialMultiset;
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy.expect

@@ -0,0 +1 @@
+false