BagUnion - as implemented in TLC module override - produces wrong result

s.t. BagUnion({b,b}) = b (+) b. Obviously, BagUnion({b,b}) = b is the
correct result.

[Bug][TLC][Changelog]

tlatools/src/tlc2/module/Bags.java

@@ -237,6 +237,13 @@ public class Bags implements ValueConstants
             throw new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE, new String[] { "BagUnion",
                     "a finite enumerable set", Value.ppr(s.toString()) });
         }
+        // MAK 02/20/2018:
+        // Need to normalize s in cases where it is an unnormalized set of identical
+        // bags, such as h == [ i \in 1..3 |-> 1 ] and BagUnion({h, h}). In other
+        // words, let b be a bag, BagUnion({b,b}) = b and not b (+) b. This
+        // unfortunately degrades performance due to sorting s1's elements.
+        s1.normalize();
+
         ValueVec elems = s1.elems;
         int sz = elems.size();
         if (sz == 0) {

tlatools/test-model/BagsTest.tla

@@ -141,6 +141,14 @@ ASSUME((1:>1) (-) EmptyBag = <<1>>)
 
 \* BagUnion
 ASSUME(BagUnion({a,a}) = a)
+ASSUME(BagUnion({b,b}) = b)
+ASSUME(BagUnion({c,c}) = c)
+ASSUME(BagUnion({d,d}) = d)
+ASSUME(BagUnion({e,e}) = e)
+ASSUME(BagUnion({f,f}) = f)
+ASSUME(BagUnion({g,g}) = g)
+ASSUME(BagUnion({h,h}) = h)
+ASSUME(BagUnion({h,h,[c |-> 3, d |-> 2, e |-> 1]}) = h (+) [c |-> 3, d |-> 2, e |-> 1])
 ASSUME(BagUnion({a,b,c,d}) = <<4,6,8>>)
 ASSUME(BagUnion({EmptyBag, EmptyBag}) = <<>>)
 ASSUME(BagUnion({[a |-> 3, b |-> 2, c |-> 1],[c |-> 3, d |-> 2, e |-> 1]}) = [a |-> 3, b |-> 2, c |-> 4, d |-> 2, e |-> 1])