diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs
index 4f762dabaf..cd236ab760 100644
--- a/source/rust_verify/src/lifetime_generate.rs
+++ b/source/rust_verify/src/lifetime_generate.rs
@@ -829,7 +829,7 @@ fn erase_expr<'tcx>(
                         mk_exp(ExpX::Op(vec![], typ))
                     }
                 }
-                Res::Def(DefKind::Const | DefKind::Fn, id) => {
+                Res::Def(DefKind::Const | DefKind::Fn | DefKind::AssocFn, id) => {
                     let vir_path = def_id_to_vir_path(ctxt.tcx, id);
                     let fun_name = Arc::new(FunX { path: vir_path });
                     return mk_exp(ExpX::Var(state.fun_name(&fun_name)));
diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs
index 19ea813add..11ef52e95b 100644
--- a/source/rust_verify/src/rust_to_vir_expr.rs
+++ b/source/rust_verify/src/rust_to_vir_expr.rs
@@ -2636,7 +2636,7 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
                     let fun = FunX { path };
                     mk_expr(ExprX::ConstVar(Arc::new(fun)))
                 }
-                Res::Def(DefKind::Fn, id) => {
+                Res::Def(DefKind::Fn, id) | Res::Def(DefKind::AssocFn, id) => {
                     let path = def_id_to_vir_path(tcx, id);
                     let fun = Arc::new(vir::ast::FunX { path });
                     mk_expr(ExprX::ExecFnByName(fun))
diff --git a/source/rust_verify_test/tests/fndef_types.rs b/source/rust_verify_test/tests/fndef_types.rs
index 7e92dbc02f..cd97c986be 100644
--- a/source/rust_verify_test/tests/fndef_types.rs
+++ b/source/rust_verify_test/tests/fndef_types.rs
@@ -174,9 +174,9 @@ test_verify_one_file_with_options! {
 }
 
 test_verify_one_file_with_options! {
-    #[test] basic_with_trait ["vstd"] => verus_code! {
-        trait Tr {
-            fn llama(&self, y: &Self, z: &Self) -> (b: bool)
+    #[test] with_trait ["vstd"] => verus_code! {
+        trait Tr : Sized {
+            fn llama(self, y: Self, z: Self) -> (b: bool)
                 requires self == y,
                 ensures b == (y == z);
         }
@@ -186,7 +186,7 @@ test_verify_one_file_with_options! {
         }
 
         impl Tr for X {
-            fn llama(&self, y: &Self, z: &Self) -> (b: bool)
+            fn llama(self, y: Self, z: Self) -> (b: bool)
             {
                 assume(false);
                 true
@@ -200,18 +200,18 @@ test_verify_one_file_with_options! {
             let y = X { t: 4 };
             let z = X { t: 6 };
 
-            let b = t(&x, &y, &z);
+            let b = t(x, y, z);
             assert(!b);
 
             let x = X { t: 4 };
             let y = X { t: 4 };
             let z = X { t: 4 };
 
-            let b = t(&x, &y, &z);
+            let b = t(x, y, z);
             assert(b);
 
-            assert(forall |x: X, y: X, z: X| (x == y) ==> (X::llama).requires((&x,&y,&z)));
-            assert(forall |x: X, y: X, z: X, b| (X::llama).ensures((&x,&y,&z),b) ==> b == (y == z));
+            assert(forall |x: X, y: X, z: X| (x == y) ==> (X::llama).requires((x,y,z)));
+            assert(forall |x: X, y: X, z: X, b| (X::llama).ensures((x,y,z),b) ==> b == (y == z));
         }
 
         fn test2() {
@@ -219,9 +219,9 @@ test_verify_one_file_with_options! {
 
             let x = X { t: 4 };
             let y = X { t: 4 };
-            let z = X { t: 6 };
+            let z = X { t: 4 };
 
-            let b = t(&x, &y, &z);
+            let b = t(x, y, z);
             assert(!b);     // FAILS
         }
 
@@ -232,22 +232,22 @@ test_verify_one_file_with_options! {
             let y = X { t: 13 };
             let z = X { t: 14 };
 
-            t(&x, &y, &z); // FAILS
+            t(x, y, z); // FAILS
         }
 
         fn test4() {
-            assert(forall |x: X, y: X, z: X| (y == z) ==> (X::llama).requires((&x,&y,&z))); // FAILS
+            assert(forall |x: X, y: X, z: X| (y == z) ==> (X::llama).requires((x,y,z))); // FAILS
         }
 
         fn test5() {
-            assert(forall |x: X, y: X, z: X, b| (X::llama).ensures((&x,&y,&z),b) ==> b == (y != z)); // FAILS
+            assert(forall |x: X, y: X, z: X, b| (X::llama).ensures((x,y,z),b) ==> b == (y != z)); // FAILS
         }
 
-        fn takes_fn1<F: Fn(&X, &X, &X) -> bool>(f: F)
+        fn takes_fn1<F: Fn(X, X, X) -> bool>(f: F)
             requires
-                f.requires((&X { t: 4 }, &X { t: 4 } , &X { t: 4 })),
-                f.requires((&X { t: 7 }, &X { t: 7 } , &X { t: 4 })),
-                forall |x: X, y: X, z: X, b| f.ensures((&x,&y,&z), b) ==> b == (y == z)
+                f.requires((X { t: 4 }, X { t: 4 } , X { t: 4 })),
+                f.requires((X { t: 7 }, X { t: 7 } , X { t: 4 })),
+                forall |x: X, y: X, z: X, b| f.ensures((x,y,z), b) ==> b == (y == z)
         {
         }
 
@@ -255,9 +255,9 @@ test_verify_one_file_with_options! {
             takes_fn1(X::llama);
         }
 
-        fn takes_fn2<F: Fn(&X, &X, &X) -> bool>(f: F)
+        fn takes_fn2<F: Fn(X, X, X) -> bool>(f: F)
             requires
-                f.requires((&X { t: 6 }, &X { t: 7 }, &X { t: 8 })),
+                f.requires((X { t: 6 }, X { t: 7 }, X { t: 8 })),
         {
         }
 
@@ -265,9 +265,9 @@ test_verify_one_file_with_options! {
             takes_fn2(X::llama); // FAILS
         }
 
-        fn takes_fn3<F: Fn(&X, &X, &X) -> bool>(f: F)
+        fn takes_fn3<F: Fn(X, X, X) -> bool>(f: F)
             requires
-                forall |x: X, y: X, z: X, b| f.ensures((&x,&y,&z), b) ==> b == (y != z)
+                forall |x: X, y: X, z: X, b| f.ensures((x,y,z), b) ==> b == (y != z)
         {
         }
 
@@ -275,9 +275,9 @@ test_verify_one_file_with_options! {
             takes_fn3(X::llama); // FAILS
         }
 
-        fn takes_fn4<T, F: Fn(&T, &T, &T) -> bool>(f: F)
+        fn takes_fn4<T, F: Fn(T, T, T) -> bool>(f: F)
             requires
-                forall |x: T, y: T, z: T, b| f.ensures((&x,&y,&z), b) ==> b == (y != z)
+                forall |x: T, y: T, z: T, b| f.ensures((x,y,z), b) ==> b == (y != z)
         {
         }