diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs
index 675bd4155e..a8023c7886 100755
--- a/Source/DafnyRuntime/DafnyRuntime.cs
+++ b/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);
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy
new file mode 100644
index 0000000000..95b3830b33
--- /dev/null
+++ b/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;
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy.expect
new file mode 100644
index 0000000000..c508d5366f
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy.expect
@@ -0,0 +1 @@
+false