diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs
index 8c44b97373..5792ddf29e 100644
--- a/creusot/src/backend/program.rs
+++ b/creusot/src/backend/program.rs
@@ -1,4 +1,4 @@
-use self::ty::{concret_intty, concret_uintty, slice_create_qname};
+use self::ty::{concret_intty, concret_uintty, slice_create_qname, slice_length_qname};
 
 use crate::{
     backend::{
@@ -337,7 +337,7 @@ impl<'tcx> RValue<'tcx> {
                     // right operand must be converted to integer
                     BinOp::Shl | BinOp::ShlUnchecked | BinOp::Shr | BinOp::ShrUnchecked => {
                         let r_ty = r.ty(lower.ctx.tcx, lower.locals);
-
+                        
                         // rust allows shifting by a value of any integer type
                         // so we need to import the prelude for the right operand
                         let prelude: PreludeModule = match r_ty.kind() {
@@ -492,7 +492,7 @@ impl<'tcx> RValue<'tcx> {
             }
             RValue::Len(pl) => {
                 let len_call =
-                    Exp::qvar(QName::from_string("Slice.length")).app_to(pl.to_why(lower, istmts));
+                    Exp::qvar(slice_length_qname()).app_to(pl.to_why(lower, istmts));
                 len_call
             }
             RValue::Array(fields) => {
diff --git a/creusot/src/backend/ty.rs b/creusot/src/backend/ty.rs
index 7021d42302..8daaf9bb43 100644
--- a/creusot/src/backend/ty.rs
+++ b/creusot/src/backend/ty.rs
@@ -574,4 +574,13 @@ pub(crate) fn slice_set_qname() -> QName {
     return QName::from_string("Slice32.set");
     #[cfg(target_pointer_width = "16")]
     return QName::from_string("Slice16.set");
+}
+
+pub(crate) fn slice_length_qname() -> QName {
+    #[cfg(target_pointer_width = "64")]
+    return QName::from_string("Slice64.length");
+    #[cfg(target_pointer_width = "32")]
+    return QName::from_string("Slice32.length");
+    #[cfg(target_pointer_width = "16")]
+    return QName::from_string("Slice16.length");
 }
\ No newline at end of file