diff --git a/tests/bench/rbmap.library.lean b/tests/bench/rbmap.library.lean
index 22f8d0cdf6..a3afa97e92 100644
--- a/tests/bench/rbmap.library.lean
+++ b/tests/bench/rbmap.library.lean
@@ -1,14 +1,17 @@
-@[reducible] def Map : Type := RBMap Nat Bool (fun a b => a < b)
+import Lean.Data.RBMap
 
-def mkMapAux : Nat → Map → Map
-| 0, m => m
-| n+1,   m => mkMapAux n (m.insert n (n % 10 = 0))
+open Std
+
+abbrev Tree : Type := RBMap Nat Bool compare
+
+def mkMapAux : Nat → Tree → Tree
+  | 0,   m => m
+  | n+1, m => mkMapAux n (m.insert n (n % 10 = 0))
 
 def mkMap (n : Nat) :=
-mkMapAux n {}
+  mkMapAux n {}
 
-def main (xs : List String) : IO UInt32 :=
-let m := mkMap xs.head.toNat;
-let v := m.fold (fun (r : Nat) (k : Nat) (v : Bool) => if v then r + 1 else r) 0;
-IO.println (toString v) *>
-pure 0
+def main (xs : List String) : IO Unit :=
+  let m := mkMap xs.head!.toNat!
+  let v := m.fold (fun _ r v => if v then r + 1 else r) 0
+  IO.println (toString v)
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index 509a42fd4c..ad7b6774ac 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -136,6 +136,14 @@
     cmd: ./rbmap_checkpoint.lean.out 2000000 10
   build_config:
     cmd: ./compile.sh rbmap_checkpoint.lean
+- attributes:
+    description: rbmap_library
+    tags: [fast, suite]
+  run_config:
+    <<: *time
+    cmd: ./rbmap.library.lean.out 2000000
+  build_config:
+    cmd: ./compile.sh rbmap.library.lean
 - attributes:
     description: unionfind
     tags: [fast, suite]