diff --git a/engine/lib/phases/phase_specialize.ml b/engine/lib/phases/phase_specialize.ml
index e3defa774..07b0891ab 100644
--- a/engine/lib/phases/phase_specialize.ml
+++ b/engine/lib/phases/phase_specialize.ml
@@ -174,6 +174,8 @@ module Make (F : Features.T) =
             rint_rint_any Core__cmp__PartialEq__eq Rust_primitives__hax__int__eq;
             any_int Hax_lib__abstraction__Abstraction__lift
               Rust_primitives__hax__int__from_machine;
+            any_int Hax_lib__int__ToInt__to_int
+              Rust_primitives__hax__int__from_machine;
             int_any Hax_lib__abstraction__Concretization__concretize
               Rust_primitives__hax__int__into_machine;
           ]
diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs
index 88eff705d..718c534df 100644
--- a/engine/names/src/lib.rs
+++ b/engine/names/src/lib.rs
@@ -82,6 +82,7 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mu
     {
         use hax_lib::*;
         let a: Int = 3u8.lift();
+        let _: Int = 3u8.to_int();
         let _ = a.clone().pow2();
         let _ = Int::_unsafe_from_str("1");
         let _: u32 = a.concretize();