diff --git a/kani-compiler/src/kani_middle/transform/check_aliasing/actions.rs b/kani-compiler/src/kani_middle/transform/check_aliasing/actions.rs
index f8514813e4f8..7b87259d7720 100644
--- a/kani-compiler/src/kani_middle/transform/check_aliasing/actions.rs
+++ b/kani-compiler/src/kani_middle/transform/check_aliasing/actions.rs
@@ -61,7 +61,7 @@ impl<'locals> CollectActions<'locals> {
                 // Direct reference to stack local
                 // x = &y;
                 let lvalue = to;
-                let rvalue = from.local.clone();
+                let rvalue = from.local;
                 self.actions.push(Action::NewStackReference { lvalue, rvalue });
             }
             [ProjectionElem::Deref] => {
diff --git a/kani-compiler/src/kani_middle/transform/check_aliasing/function_cache.rs b/kani-compiler/src/kani_middle/transform/check_aliasing/function_cache.rs
index 507dc0216e15..621572a1e28b 100644
--- a/kani-compiler/src/kani_middle/transform/check_aliasing/function_cache.rs
+++ b/kani-compiler/src/kani_middle/transform/check_aliasing/function_cache.rs
@@ -58,9 +58,9 @@ impl Cache {
     /// in the given compilation context, ctx
     pub fn register(&mut self, ctx: &TyCtxt, sig: Signature) -> Result<&MirInstance, MirError> {
         let Cache { cache } = self;
-        for i in 0..cache.len() {
-            if sig == cache[i].signature {
-                return Ok(&cache[i].instance);
+        for item in &cache {
+            if sig == item.signature {
+                return Ok(item.instance);
             }
         }
         let fndef = find_fn_def(*ctx, &sig.diagnostic)
diff --git a/kani-compiler/src/kani_middle/transform/check_aliasing/instrumentation.rs b/kani-compiler/src/kani_middle/transform/check_aliasing/instrumentation.rs
index 6cac39c43ae2..297412e985ec 100644
--- a/kani-compiler/src/kani_middle/transform/check_aliasing/instrumentation.rs
+++ b/kani-compiler/src/kani_middle/transform/check_aliasing/instrumentation.rs
@@ -119,7 +119,7 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> {
         let tcx = &self.tcx;
         let fn_pointers = &mut self.fn_pointers;
         let body = &mut self.body;
-        let span = self.span.clone();
+        let span = *self.span;
         let instance = cache.register(tcx, callee)?;
         let func_local = fn_pointers
             .entry(*instance)
@@ -210,13 +210,13 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> {
                 let kind = TerminatorKind::Goto { target: 0 };
                 let terminator = Terminator { kind, span };
                 let source = &mut self.min_processed.clone();
-                let enter_ghost_block = source.clone();
+                let enter_ghost_block = *source;
                 let body = &mut self.body;
                 body.replace_terminator(source, terminator.clone()); // replace terminator so you can instrument "after" it
                 body.insert_terminator(source, InsertPosition::After, terminator.clone());
-                let execute_terminator_block = source.clone();
+                let execute_terminator_block = *source;
                 body.insert_terminator(source, InsertPosition::After, terminator.clone());
-                let execute_ghost_block = source.clone();
+                let execute_ghost_block = *source;
 
                 // Instrument enter ghost:
                 let span = original_span;
@@ -398,7 +398,7 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> {
     pub fn instrument_instructions(&mut self) -> Result<()> {
         loop {
             let actions = self.instruction_actions();
-            if actions.len() > 0 {
+            if !actions.is_empty() {
                 eprintln!("Instrumenting actions:");
                 self.process_instruction();
             }
@@ -417,7 +417,7 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> {
                     SourceInstruction::Statement { idx: idx - 1, bb }
                 }
                 SourceInstruction::Terminator { bb }
-                    if self.body.blocks()[bb].statements.len() > 0 =>
+                    if !self.body.blocks()[bb].statements.is_empty() =>
                 {
                     SourceInstruction::Statement {
                         idx: self.body.blocks()[bb].statements.len() - 1,
diff --git a/kani-compiler/src/kani_middle/transform/check_aliasing/mod.rs b/kani-compiler/src/kani_middle/transform/check_aliasing/mod.rs
index d05f55dcc055..84fbba7740f1 100644
--- a/kani-compiler/src/kani_middle/transform/check_aliasing/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/check_aliasing/mod.rs
@@ -125,11 +125,10 @@ impl GlobalPass for GlobalAliasingPass {
                 .def
                 .all_attrs()
                 .into_iter()
-                .fold(false, |is_proof, attr| is_proof || attr.as_str().contains("kanitool::proof"))
+                .all(|attr| attr.as_str().contains("kanitool::proof")) &&
+                found.insert(instance)
             {
-                if found.insert(instance) {
-                    queue.push_back(instance)
-                }
+                queue.push_back(instance)
             }
         }
         while let Some(instance) = queue.pop_front() {