diff --git a/hax-bounded-integers/src/lib.rs b/hax-bounded-integers/src/lib.rs
index db974d68d..ac43d139a 100644
--- a/hax-bounded-integers/src/lib.rs
+++ b/hax-bounded-integers/src/lib.rs
@@ -241,8 +241,8 @@ const _: () = {
 fn tests() {
     use hax_lib::*;
 
-    let x: BoundedU8<0, 5> = 2.refine();
-    let y: BoundedU8<5, 10> = (x + x).refine();
+    let x: BoundedU8<0, 5> = 2.check();
+    let y: BoundedU8<5, 10> = (x + x).check();
 
     let _ = x >> 3;
     let _ = x >> BoundedU8::<0, 5>::new(3);