diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy
index 99f590a5..d0e35c70 100644
--- a/examples/MutableMap/MutableMapExamples.dfy
+++ b/examples/MutableMap/MutableMapExamples.dfy
@@ -27,7 +27,7 @@ module {:options "-functionSyntax:4"} MutableMapExamples {
   }
 
   method Main() {
-    var m := new MutableMap<string,string>();
+    var m := new MutableMap((k: string, v: string) => true, false);
     AssertAndExpect(m.Keys() == {});
     AssertAndExpect(m.Values() == {});
     AssertAndExpect(m.Items() == {});
diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy
index 94487a13..3233c35d 100644
--- a/src/MutableMap/MutableMap.dfy
+++ b/src/MutableMap/MutableMap.dfy
@@ -62,8 +62,13 @@ module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} DafnyLibraries
   }
 
   class {:extern} MutableMap<K(==),V(==)> extends MutableMapTrait<K,V> {
-    constructor {:extern} ()
+
+    // Invariant on key-value pairs this map may hold
+    ghost const inv: (K, V) -> bool
+
+    constructor {:extern} (ghost inv: (K, V) -> bool, bytesKeys: bool := false)
       ensures this.content() == map[]
+      ensures this.inv == inv
 
     function {:extern} content(): map<K, V>
       reads this
diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java
index 9a3e06be..ff49a44b 100644
--- a/src/MutableMap/MutableMap.java
+++ b/src/MutableMap/MutableMap.java
@@ -18,10 +18,16 @@
 public class MutableMap<K, V> implements DafnyLibraries.MutableMapTrait<K, V> {
   private ConcurrentHashMap<K,V> m;
 
-  public MutableMap(dafny.TypeDescriptor<K> _td_K, dafny.TypeDescriptor<V> _td_V) {
+  // TODO: remove bytesKeys boolean https://github.com/dafny-lang/dafny/issues/6333
+  public MutableMap(
+    dafny.TypeDescriptor<K> _td_K, 
+    dafny.TypeDescriptor<V> _td_V,
+    boolean bytesKeys) {
     m = new ConcurrentHashMap<K,V>();
   }
 
+  public void __ctor(boolean bytesKeys) {}
+
   @Override 
   public DafnyMap<K,V> content() {
     return new DafnyMap<K,V>(m);