diff --git a/bench/ce/map.mlw b/bench/ce/map.mlw
index 2d1787595839c363e21f514b950b72ed20d0993b..6c8873bd33b3b5d385ccfa332841dc5fc8b55a2a 100644
--- a/bench/ce/map.mlw
+++ b/bench/ce/map.mlw
@@ -42,3 +42,11 @@ goal t1 : forall t:map int int, i : int.
    get (set t 0 42) i = get t i
 
 end
+
+module OtherIndices
+
+use map.Map
+
+  goal g : forall m: map real real. m 0.1 = 0.0 \/ m 0.2 = m 0.1 
+
+end
\ No newline at end of file
diff --git a/bench/ce/oracles/map_CVC4,1.5_SP.oracle b/bench/ce/oracles/map_CVC4,1.5_SP.oracle
index 925c814cc40042e1193f9396ed816d9369652760..064b49f690dd6da5f37b198e21d6c79caf8498be 100644
--- a/bench/ce/oracles/map_CVC4,1.5_SP.oracle
+++ b/bench/ce/oracles/map_CVC4,1.5_SP.oracle
@@ -174,3 +174,4 @@ t, [[@introduced]] = {"type" : "Array" ,
 {"others" : {"type" : "Integer" ,
 "val" : "0" } }] }
 
+bench/ce/map.mlw OtherIndices g: Unknown (sat)
diff --git a/bench/ce/oracles/map_CVC4,1.5_WP.oracle b/bench/ce/oracles/map_CVC4,1.5_WP.oracle
index 5bcfe2e7719d5b719926b14b7e6e046882f10a35..ab04aa87b4b896afe49f8e5978165b9847344ab2 100644
--- a/bench/ce/oracles/map_CVC4,1.5_WP.oracle
+++ b/bench/ce/oracles/map_CVC4,1.5_WP.oracle
@@ -174,3 +174,4 @@ t, [[@introduced]] = {"type" : "Array" ,
 {"others" : {"type" : "Integer" ,
 "val" : "0" } }] }
 
+bench/ce/map.mlw OtherIndices g: Unknown (sat)
diff --git a/bench/ce/oracles/map_Z3,4.6.0_SP.oracle b/bench/ce/oracles/map_Z3,4.6.0_SP.oracle
index f3ed8f591c8f1cd347595f3a0d953199586f2b3c..f81db741ce83b731a1da3a13c7e62fc93aac96d6 100644
--- a/bench/ce/oracles/map_Z3,4.6.0_SP.oracle
+++ b/bench/ce/oracles/map_Z3,4.6.0_SP.oracle
@@ -195,3 +195,4 @@ t, [[@introduced]] = {"type" : "Array" ,
 {"others" : {"type" : "Integer" ,
 "val" : "1" } }] }
 
+bench/ce/map.mlw OtherIndices g: Unknown (sat)
diff --git a/bench/ce/oracles/map_Z3,4.6.0_WP.oracle b/bench/ce/oracles/map_Z3,4.6.0_WP.oracle
index 782ac6149f8444d8ce0c5b47a889ed05e9c94eb6..dd9d61589c6e91f622c68b11c91cf87c447d9ce5 100644
--- a/bench/ce/oracles/map_Z3,4.6.0_WP.oracle
+++ b/bench/ce/oracles/map_Z3,4.6.0_WP.oracle
@@ -195,3 +195,4 @@ t, [[@introduced]] = {"type" : "Array" ,
 {"others" : {"type" : "Integer" ,
 "val" : "1" } }] }
 
+bench/ce/map.mlw OtherIndices g: Unknown (sat)