diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs
index 0260ff116109..35e68ad9a6ca 100644
--- a/cprover_bindings/src/goto_program/builtin.rs
+++ b/cprover_bindings/src/goto_program/builtin.rs
@@ -312,6 +312,6 @@ impl BuiltinFn {
     }
 
     pub fn call(&self, arguments: Vec<Expr>, loc: Location) -> Expr {
-        self.as_expr().with_location(loc.clone()).call(arguments).with_location(loc)
+        self.as_expr().with_location(loc).call(arguments).with_location(loc)
     }
 }
diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
index 36c8a3244168..6b7891bd970e 100644
--- a/cprover_bindings/src/goto_program/expr.rs
+++ b/cprover_bindings/src/goto_program/expr.rs
@@ -1,5 +1,9 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This file has a lot of function with names like "div"
+#![allow(clippy::should_implement_trait)]
+
 use self::BinaryOperand::*;
 use self::ExprValue::*;
 use self::UnaryOperand::*;
@@ -488,7 +492,7 @@ impl Expr {
         let mut rval: Vec<_> = parameters
             .iter()
             .map(|parameter| {
-                arguments.remove(0).cast_to_machine_equivalent_type(&parameter.typ(), mm)
+                arguments.remove(0).cast_to_machine_equivalent_type(parameter.typ(), mm)
             })
             .collect();
 
@@ -510,7 +514,7 @@ impl Expr {
 
     /// `union {double d; uint64_t bp} u = {.bp = 0x1234}; >>> u.d <<<`
     pub fn double_constant_from_bitpattern(bp: u64) -> Self {
-        let c = unsafe { std::mem::transmute(bp) };
+        let c = f64::from_bits(bp);
         Self::double_constant(c)
     }
 
@@ -521,7 +525,7 @@ impl Expr {
 
     /// `union {float f; uint32_t bp} u = {.bp = 0x1234}; >>> u.f <<<`
     pub fn float_constant_from_bitpattern(bp: u32) -> Self {
-        let c = unsafe { std::mem::transmute(bp) };
+        let c = f32::from_bits(bp);
         Self::float_constant(c)
     }
 
@@ -622,7 +626,7 @@ impl Expr {
     /// e.g. `({ int y = foo (); int z; if (y > 0) z = y; else z = - y; z; })`
     /// `({ op1; op2; ...})`
     pub fn statement_expression(ops: Vec<Stmt>, typ: Type) -> Self {
-        assert!(ops.len() > 0);
+        assert!(!ops.is_empty());
         assert_eq!(ops.last().unwrap().get_expression().unwrap().typ, typ);
         expr!(StatementExpression { statements: ops }, typ)
     }
@@ -1350,7 +1354,7 @@ impl Expr {
         assert!(self.typ.is_integer());
         assert_eq!(self.typ, e.typ);
         let typ = self.typ.clone();
-        let res = self.clone().add_overflow(e.clone());
+        let res = self.clone().add_overflow(e);
         // If negative + something overflowed, the something must have been negative too, so we saturate to min.
         // (self < 0) ? min_int : max_int
         let saturating_val = self.is_negative().ternary(typ.min_int_expr(mm), typ.max_int_expr(mm));
@@ -1362,7 +1366,7 @@ impl Expr {
         assert!(self.typ.is_integer());
         assert_eq!(self.typ, e.typ);
         let typ = self.typ.clone();
-        let res = self.clone().sub_overflow(e.clone());
+        let res = self.sub_overflow(e.clone());
         // If something minus a negative overflowed, it must have overflowed past positive max. Saturate there.
         // Otherwise, if something minus a positive overflowed, it must have overflowed to past min. Saturate there.
         let saturating_val = e.is_negative().ternary(typ.max_int_expr(mm), typ.min_int_expr(mm));
@@ -1446,12 +1450,12 @@ impl Expr {
                 }
             }
             None => {
-                for i in 0..fields.len() {
-                    if fields[i].is_padding() {
+                for field in fields {
+                    if field.is_padding() {
                         continue;
                     }
-                    let name = fields[i].name();
-                    exprs.insert(name, self.clone().member(&name.to_string(), &symbol_table));
+                    let name = field.name();
+                    exprs.insert(name, self.clone().member(&name.to_string(), symbol_table));
                 }
             }
         }
diff --git a/cprover_bindings/src/goto_program/location.rs b/cprover_bindings/src/goto_program/location.rs
index 120832874968..e16120047213 100644
--- a/cprover_bindings/src/goto_program/location.rs
+++ b/cprover_bindings/src/goto_program/location.rs
@@ -138,7 +138,7 @@ impl Location {
                 file.into(),
                 function.intern(),
                 line,
-                col.map(|x| x.try_into().unwrap()),
+                col,
                 comment.into(),
                 property_name.into(),
             ),
diff --git a/cprover_bindings/src/goto_program/mod.rs b/cprover_bindings/src/goto_program/mod.rs
index a66aca693f37..0b0049459b57 100644
--- a/cprover_bindings/src/goto_program/mod.rs
+++ b/cprover_bindings/src/goto_program/mod.rs
@@ -1,7 +1,12 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
 //! This module contains typesafe representations of CBMC's data structures
 
+// There are a fair number of constructs in this module that are better maintained as
+// explicit pattern matching versus using the `matches!` macro.
+#![allow(clippy::match_like_matches_macro)]
+
 mod builtin;
 mod expr;
 mod location;
diff --git a/cprover_bindings/src/goto_program/stmt.rs b/cprover_bindings/src/goto_program/stmt.rs
index 9108dbd57fbf..e079e531434f 100644
--- a/cprover_bindings/src/goto_program/stmt.rs
+++ b/cprover_bindings/src/goto_program/stmt.rs
@@ -205,10 +205,10 @@ impl Stmt {
         Stmt::block(
             vec![
                 // Assert our expected true expression.
-                Stmt::assert(expect_true.clone(), "sanity_check", &assert_msg, loc.clone()),
+                Stmt::assert(expect_true.clone(), "sanity_check", &assert_msg, loc),
                 // If expect_true is false, assume false to block any further
                 // exploration of this path.
-                Stmt::assume(expect_true, loc.clone()),
+                Stmt::assume(expect_true, loc),
             ],
             loc,
         )
@@ -246,7 +246,7 @@ impl Stmt {
     /// SUCCESS/FAILURE, it uses SATISFIED/FAILED
     pub fn cover(cond: Expr, loc: Location) -> Self {
         assert!(cond.typ().is_bool());
-        BuiltinFn::CProverCover.call(vec![cond], loc.clone()).as_stmt(loc)
+        BuiltinFn::CProverCover.call(vec![cond], loc).as_stmt(loc)
     }
 
     /// `lhs.typ lhs = value;` or `lhs.typ lhs;`
@@ -330,7 +330,7 @@ impl Stmt {
     pub fn with_label<T: Into<InternedString>>(self, label: T) -> Self {
         let label = label.into();
         assert!(!label.is_empty());
-        stmt!(Label { label, body: self }, self.location().clone())
+        stmt!(Label { label, body: self }, *self.location())
     }
 }
 
diff --git a/cprover_bindings/src/goto_program/symbol.rs b/cprover_bindings/src/goto_program/symbol.rs
index 38fc9b8a8ae2..13c6e9f369f7 100644
--- a/cprover_bindings/src/goto_program/symbol.rs
+++ b/cprover_bindings/src/goto_program/symbol.rs
@@ -159,7 +159,7 @@ impl Symbol {
             name.to_string(),
             loc,
             typ,
-            body.map_or(SymbolValues::None, |x| SymbolValues::Stmt(x)),
+            body.map_or(SymbolValues::None, SymbolValues::Stmt),
             Some(name),
             pretty_name,
         )
diff --git a/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs b/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs
index dd3f08f97d78..4bf9ed007d9d 100644
--- a/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs
+++ b/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs
@@ -81,7 +81,7 @@ impl ExprTransformer {
 
     /// Extract `empty_statics` map for final processing.
     fn empty_statics_owned(&mut self) -> HashMap<InternedString, Expr> {
-        std::mem::replace(&mut self.empty_statics, HashMap::default())
+        std::mem::take(&mut self.empty_statics)
     }
 
     /// Add identifier to a transformed parameter if it's missing;
diff --git a/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/name_transformer.rs b/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/name_transformer.rs
index f021b7ea9f93..10d0a792367c 100644
--- a/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/name_transformer.rs
+++ b/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/name_transformer.rs
@@ -48,8 +48,8 @@ impl NameTransformer {
         }
 
         // Don't tranform the `tag-` prefix of identifiers
-        let (prefix, name) = if orig_name.starts_with("tag-") {
-            (&orig_name[..4], &orig_name[4..])
+        let (prefix, name) = if let Some(tag) = orig_name.strip_prefix("tag-") {
+            ("tag-", tag)
         } else {
             ("", orig_name)
         };
@@ -95,7 +95,8 @@ impl NameTransformer {
                     return new_name.replace(illegal, replacement);
                 }
             }
-            return new_name;
+
+            new_name
         }
 
         let name = fix_name(name);
diff --git a/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs b/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs
index f09259781f01..b69771153080 100644
--- a/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs
+++ b/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs
@@ -22,7 +22,7 @@ impl NondetTransformer {
 
     /// Extract `nondet_types` map for final processing.
     pub fn nondet_types_owned(&mut self) -> HashMap<String, Type> {
-        std::mem::replace(&mut self.nondet_types, HashMap::default())
+        std::mem::take(&mut self.nondet_types)
     }
 }
 
@@ -87,7 +87,7 @@ impl Transformer for NondetTransformer {
         let fields = transformed_typ.lookup_components(self.symbol_table()).unwrap().clone();
         let transformed_values: Vec<_> = fields
             .into_iter()
-            .zip(values.into_iter())
+            .zip(values.iter())
             .map(
                 |(field, value)| {
                     if field.is_padding() { value.clone() } else { self.transform_expr(value) }
diff --git a/cprover_bindings/src/goto_program/symtab_transformer/transformer.rs b/cprover_bindings/src/goto_program/symtab_transformer/transformer.rs
index 8b7df396c93a..262ca4c702af 100644
--- a/cprover_bindings/src/goto_program/symtab_transformer/transformer.rs
+++ b/cprover_bindings/src/goto_program/symtab_transformer/transformer.rs
@@ -70,8 +70,8 @@ pub trait Transformer: Sized {
     }
 
     /// Transforms an array type (`typ x[size]`)
-    fn transform_type_array(&mut self, typ: &Box<Type>, size: &u64) -> Type {
-        let transformed_typ = self.transform_type(typ.as_ref());
+    fn transform_type_array(&mut self, typ: &Type, size: &u64) -> Type {
+        let transformed_typ = self.transform_type(typ);
         transformed_typ.array_of(*size)
     }
 
@@ -81,8 +81,8 @@ pub trait Transformer: Sized {
     }
 
     /// Transforms a c bit field type (`typ x : width`)
-    fn transform_type_c_bit_field(&mut self, typ: &Box<Type>, width: &u64) -> Type {
-        let transformed_typ = self.transform_type(typ.as_ref());
+    fn transform_type_c_bit_field(&mut self, typ: &Type, width: &u64) -> Type {
+        let transformed_typ = self.transform_type(typ);
         transformed_typ.as_bitfield(*width)
     }
 
@@ -104,7 +104,7 @@ pub trait Transformer: Sized {
     }
 
     /// Transforms a function type (`return_type x(parameters)`)
-    fn transform_type_code(&mut self, parameters: &[Parameter], return_type: &Box<Type>) -> Type {
+    fn transform_type_code(&mut self, parameters: &[Parameter], return_type: &Type) -> Type {
         let transformed_parameters =
             parameters.iter().map(|parameter| self.transform_type_parameter(parameter)).collect();
         let transformed_return_type = self.transform_type(return_type);
@@ -127,7 +127,7 @@ pub trait Transformer: Sized {
     }
 
     /// Transforms a flexible array type (`typ x[]`)
-    fn transform_type_flexible_array(&mut self, typ: &Box<Type>) -> Type {
+    fn transform_type_flexible_array(&mut self, typ: &Type) -> Type {
         let transformed_typ = self.transform_type(typ);
         Type::flexible_array_of(transformed_typ)
     }
@@ -148,14 +148,14 @@ pub trait Transformer: Sized {
     }
 
     /// Transforms an infinite array type (`typ x[__CPROVER_infinity()]`)
-    fn transform_type_infinite_array(&mut self, typ: &Box<Type>) -> Type {
-        let transformed_typ = self.transform_type(typ.as_ref());
+    fn transform_type_infinite_array(&mut self, typ: &Type) -> Type {
+        let transformed_typ = self.transform_type(typ);
         transformed_typ.infinite_array_of()
     }
 
     /// Transforms a pointer type (`typ*`)
-    fn transform_type_pointer(&mut self, typ: &Box<Type>) -> Type {
-        let transformed_typ = self.transform_type(typ.as_ref());
+    fn transform_type_pointer(&mut self, typ: &Type) -> Type {
+        let transformed_typ = self.transform_type(typ);
         transformed_typ.to_pointer()
     }
 
@@ -219,23 +219,23 @@ pub trait Transformer: Sized {
     fn transform_type_variadic_code(
         &mut self,
         parameters: &[Parameter],
-        return_type: &Box<Type>,
+        return_type: &Type,
     ) -> Type {
         let transformed_parameters =
             parameters.iter().map(|parameter| self.transform_type_parameter(parameter)).collect();
-        let transformed_return_type = self.transform_type(return_type.as_ref());
+        let transformed_return_type = self.transform_type(return_type);
         Type::variadic_code(transformed_parameters, transformed_return_type)
     }
 
     /// Transforms a vector type (`typ __attribute__((vector_size (size * sizeof(typ)))) var;`)
-    fn transform_type_vector(&mut self, typ: &Box<Type>, size: &u64) -> Type {
-        let transformed_typ = self.transform_type(typ.as_ref());
+    fn transform_type_vector(&mut self, typ: &Type, size: &u64) -> Type {
+        let transformed_typ = self.transform_type(typ);
         Type::vector(transformed_typ, *size)
     }
 
     /// Transforms a type def (`typedef typ tag`)
-    fn transform_type_def(&mut self, tag: InternedString, typ: &Box<Type>) -> Type {
-        let transformed_typ = self.transform_type(typ.as_ref());
+    fn transform_type_def(&mut self, tag: InternedString, typ: &Type) -> Type {
+        let transformed_typ = self.transform_type(typ);
         transformed_typ.to_typedef(tag)
     }
 
@@ -279,7 +279,7 @@ pub trait Transformer: Sized {
             ExprValue::UnOp { op, e } => self.transform_expr_un_op(typ, op, e),
             ExprValue::Vector { elems } => self.transform_expr_vector(typ, elems),
         }
-        .with_location(e.location().clone())
+        .with_location(*e.location())
     }
 
     /// Transforms a reference expr (`&self`)
@@ -450,7 +450,7 @@ pub trait Transformer: Sized {
             transformed_typ
         );
         let transformed_values: Vec<_> =
-            values.into_iter().map(|value| self.transform_expr(value)).collect();
+            values.iter().map(|value| self.transform_expr(value)).collect();
         Expr::struct_expr_from_padded_values(
             transformed_typ,
             transformed_values,
@@ -530,7 +530,7 @@ pub trait Transformer: Sized {
             }
             StmtBody::While { cond, body } => self.transform_stmt_while(cond, body),
         }
-        .with_location(stmt.location().clone())
+        .with_location(*stmt.location())
     }
 
     /// Transforms an assign stmt (`lhs = rhs;`)
diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs
index 6937ca8e6a12..dde052638e20 100644
--- a/cprover_bindings/src/goto_program/typ.rs
+++ b/cprover_bindings/src/goto_program/typ.rs
@@ -73,7 +73,7 @@ pub enum Type {
 }
 
 /// Machine dependent integers: `bool`, `char`, `int`, `size_t`, etc.
-#[derive(PartialEq, Debug, Clone, Copy)]
+#[derive(PartialEq, Eq, Debug, Clone, Copy)]
 pub enum CIntType {
     /// `bool`
     Bool,
@@ -769,10 +769,10 @@ impl Type {
 
     /// If typ.field_name exists in the symbol table, return Some(field.typ),
     /// otherwise, return none.
-    pub fn lookup_field_type<'a, T: Into<InternedString>>(
+    pub fn lookup_field_type<T: Into<InternedString>>(
         &self,
         field_name: T,
-        st: &'a SymbolTable,
+        st: &SymbolTable,
     ) -> Option<Type> {
         self.lookup_field(field_name, st).map(|f| f.typ())
     }
@@ -1279,7 +1279,7 @@ impl Type {
             Type::Array { typ, size } => {
                 format!("array_of_{}_{}", size, typ.to_identifier())
             }
-            Type::Bool => format!("bool"),
+            Type::Bool => "bool".to_string(),
             Type::CBitField { width, typ } => {
                 format!("cbitfield_of_{}_{}", width, typ.to_identifier())
             }
@@ -1295,11 +1295,11 @@ impl Type {
                 let return_string = return_type.to_identifier();
                 format!("code_from_{}_to_{}", parameter_string, return_string)
             }
-            Type::Constructor => format!("constructor"),
-            Type::Double => format!("double"),
-            Type::Empty => format!("empty"),
+            Type::Constructor => "constructor".to_string(),
+            Type::Double => "double".to_string(),
+            Type::Empty => "empty".to_string(),
             Type::FlexibleArray { typ } => format!("flexarray_of_{}", typ.to_identifier()),
-            Type::Float => format!("float"),
+            Type::Float => "float".to_string(),
             Type::IncompleteStruct { tag } => tag.to_string(),
             Type::IncompleteUnion { tag } => tag.to_string(),
             Type::InfiniteArray { typ } => {
diff --git a/cprover_bindings/src/irep/irep.rs b/cprover_bindings/src/irep/irep.rs
index 29be8e4bf4c2..d9b9c80afb59 100644
--- a/cprover_bindings/src/irep/irep.rs
+++ b/cprover_bindings/src/irep/irep.rs
@@ -38,7 +38,7 @@ impl Irep {
 impl Irep {
     pub fn with_location(self, l: &Location, mm: &MachineModel) -> Self {
         if !l.is_none() {
-            self.with_named_sub(IrepId::CSourceLocation, l.to_irep(&mm))
+            self.with_named_sub(IrepId::CSourceLocation, l.to_irep(mm))
         } else {
             self
         }
@@ -102,7 +102,7 @@ impl Irep {
     }
 
     pub fn just_id(id: IrepId) -> Irep {
-        Irep { id: id, sub: Vec::new(), named_sub: LinearMap::new() }
+        Irep { id, sub: Vec::new(), named_sub: LinearMap::new() }
     }
 
     pub fn just_int_id<T>(i: T) -> Irep
@@ -112,7 +112,7 @@ impl Irep {
         Irep::just_id(IrepId::from_int(i))
     }
     pub fn just_named_sub(named_sub: LinearMap<IrepId, Irep>) -> Irep {
-        Irep { id: IrepId::EmptyString, sub: vec![], named_sub: named_sub }
+        Irep { id: IrepId::EmptyString, sub: vec![], named_sub }
     }
 
     pub fn just_string_id<T: Into<InternedString>>(s: T) -> Irep {
@@ -120,7 +120,7 @@ impl Irep {
     }
 
     pub fn just_sub(sub: Vec<Irep>) -> Irep {
-        Irep { id: IrepId::EmptyString, sub: sub, named_sub: LinearMap::new() }
+        Irep { id: IrepId::EmptyString, sub, named_sub: LinearMap::new() }
     }
 
     pub fn nil() -> Irep {
diff --git a/cprover_bindings/src/irep/serialize.rs b/cprover_bindings/src/irep/serialize.rs
index 0ca9ff417efe..a76ae584cf29 100644
--- a/cprover_bindings/src/irep/serialize.rs
+++ b/cprover_bindings/src/irep/serialize.rs
@@ -52,7 +52,7 @@ impl Serialize for crate::goto_program::SymbolTable {
         S: Serializer,
     {
         let mut obj = serializer.serialize_map(None)?;
-        obj.serialize_entry("symbolTable", &StreamingSymbols(&self))?;
+        obj.serialize_entry("symbolTable", &StreamingSymbols(self))?;
         obj.end()
     }
 }
diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs
index 92c7d54d4293..62515f6eca0d 100644
--- a/cprover_bindings/src/irep/to_irep.rs
+++ b/cprover_bindings/src/irep/to_irep.rs
@@ -206,7 +206,7 @@ impl ToIrep for ExprValue {
             }
             //TODO, determine if there is an endineness problem here
             ExprValue::DoubleConstant(i) => {
-                let c: u64 = unsafe { std::mem::transmute(*i) };
+                let c: u64 = i.to_bits();
                 Irep {
                     id: IrepId::Constant,
                     sub: vec![],
@@ -217,7 +217,7 @@ impl ToIrep for ExprValue {
                 }
             }
             ExprValue::FloatConstant(i) => {
-                let c: u32 = unsafe { std::mem::transmute(*i) };
+                let c: u32 = i.to_bits();
                 Irep {
                     id: IrepId::Constant,
                     sub: vec![],
@@ -405,8 +405,7 @@ impl ToIrep for StmtBody {
             StmtBody::Assume { cond } => code_irep(IrepId::Assume, vec![cond.to_irep(mm)]),
             StmtBody::AtomicBlock(stmts) => {
                 let mut irep_stmts = vec![code_irep(IrepId::AtomicBegin, vec![])];
-                irep_stmts
-                    .append(&mut stmts.into_iter().map(|x| x.to_irep(mm)).collect::<Vec<Irep>>());
+                irep_stmts.append(&mut stmts.iter().map(|x| x.to_irep(mm)).collect());
                 irep_stmts.push(code_irep(IrepId::AtomicEnd, vec![]));
                 code_irep(IrepId::Block, irep_stmts)
             }
diff --git a/cprover_bindings/src/machine_model.rs b/cprover_bindings/src/machine_model.rs
index 87963d1c8c20..d48d5c05dc81 100644
--- a/cprover_bindings/src/machine_model.rs
+++ b/cprover_bindings/src/machine_model.rs
@@ -46,7 +46,8 @@ impl From<RoundingMode> for BigInt {
     }
 }
 
-/// Constructor
+// TODO: This file should be refactored. This is a bit "OO" style when it doesn't have to be.
+// Delete this "constructor" and all the accessors below, just make all the fields pub!
 impl MachineModel {
     pub fn new(
         alignment: u64,
diff --git a/cprover_bindings/src/utils.rs b/cprover_bindings/src/utils.rs
index 52738f96ac45..86f64065574b 100644
--- a/cprover_bindings/src/utils.rs
+++ b/cprover_bindings/src/utils.rs
@@ -14,7 +14,7 @@ pub const BUG_REPORT_URL: &str =
 /// The aggregate name used in CBMC for aggregates of type `n`.
 pub fn aggr_tag<T: Into<InternedString>>(n: T) -> InternedString {
     let n = n.into();
-    format!("tag-{}", n.to_string()).into()
+    format!("tag-{}", n).into()
 }
 
 pub trait NumUtils {
@@ -96,8 +96,7 @@ pub fn max_int(width: u64, signed: bool) -> BigInt {
 pub fn min_int(width: u64, signed: bool) -> BigInt {
     if signed {
         let max = max_int(width, true);
-        let min = -max - 1;
-        min
+        -max - 1
     } else {
         BigInt::zero()
     }
diff --git a/kani-compiler/build.rs b/kani-compiler/build.rs
index 672866b8f9a7..c42fc62a55b8 100644
--- a/kani-compiler/build.rs
+++ b/kani-compiler/build.rs
@@ -33,7 +33,7 @@ fn setup_lib(out_dir: &str, lib_out: &str, lib: &str) {
         "--out-dir",
         lib_out,
         "--target-dir",
-        &out_dir,
+        out_dir,
     ];
     let result = Command::new("cargo")
         .env("CARGO_ENCODED_RUSTFLAGS", "--cfg=kani")
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
index 653fa5b77515..9ab4d1412941 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -198,7 +198,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 // This follows the naming convention defined in `typ.rs`.
                 let lc = Local::from_usize(arg_i + starting_idx);
                 let (name, base_name) = self.codegen_spread_arg_name(&lc);
-                let sym = Symbol::variable(name, base_name, self.codegen_ty(arg_t), loc.clone())
+                let sym = Symbol::variable(name, base_name, self.codegen_ty(arg_t), loc)
                     .with_is_hidden(false);
                 // The spread arguments are additional function paramaters that are patched in
                 // They are to the function signature added in the `fn_typ` function.
@@ -212,7 +212,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }));
         let marshalled_tuple_value =
             Expr::struct_expr(tup_typ.clone(), marshalled_tuple_fields, &self.symbol_table)
-                .with_location(loc.clone());
+                .with_location(loc);
         self.declare_variable(
             self.codegen_var_name(&spread_arg),
             self.codegen_var_base_name(&spread_arg),
@@ -291,21 +291,19 @@ impl<'tcx> GotocCtx<'tcx> {
         let mangled_name = current_fn.name();
         let loc = self.codegen_span(&current_fn.mir().span);
 
-        let harness = HarnessMetadata {
+        HarnessMetadata {
             pretty_name,
             mangled_name,
             original_file: loc.filename().unwrap(),
             original_line: loc.line().unwrap().to_string(),
             unwind_value: None,
-        };
-
-        harness
+        }
     }
 
     /// Updates the proof harness with new unwind value
     fn handle_kanitool_unwind(&mut self, attr: &Attribute, harness: &mut HarnessMetadata) {
         // If some unwind value already exists, then the current unwind being handled is a duplicate
-        if !harness.unwind_value.is_none() {
+        if harness.unwind_value.is_some() {
             self.tcx.sess.span_err(attr.span, "Only one '#[kani::unwind]' allowed");
             return;
         }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 29c64f519152..97e394d7d83c 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -59,8 +59,8 @@ impl<'tcx> GotocCtx<'tcx> {
             let fargs = self.codegen_funcall_args(args);
             Stmt::block(
                 vec![
-                    self.codegen_intrinsic(instance, fargs, &destination, Some(span)),
-                    Stmt::goto(self.current_fn().find_label(&target), loc),
+                    self.codegen_intrinsic(instance, fargs, destination, Some(span)),
+                    Stmt::goto(self.current_fn().find_label(target), loc),
                 ],
                 loc,
             )
@@ -351,11 +351,11 @@ impl<'tcx> GotocCtx<'tcx> {
                 emit_concurrency_warning!(intrinsic, loc);
                 let var1_ref = fargs.remove(0);
                 let var1 = var1_ref.dereference();
-                let tmp = self.gen_temp_variable(var1.typ().clone(), loc.clone()).to_expr();
-                let decl_stmt = Stmt::decl(tmp.clone(), Some(var1.to_owned()), loc.clone());
+                let tmp = self.gen_temp_variable(var1.typ().clone(), loc).to_expr();
+                let decl_stmt = Stmt::decl(tmp.clone(), Some(var1.to_owned()), loc);
                 let var2 = fargs.remove(0);
-                let op_expr = (var1.clone()).$op(var2).with_location(loc.clone());
-                let assign_stmt = (var1.clone()).assign(op_expr, loc.clone());
+                let op_expr = (var1.clone()).$op(var2).with_location(loc);
+                let assign_stmt = (var1.clone()).assign(op_expr, loc);
                 let res_stmt = self.codegen_expr_to_place(p, tmp.clone());
                 Stmt::atomic_block(vec![decl_stmt, assign_stmt, res_stmt], loc)
             }};
@@ -684,18 +684,10 @@ impl<'tcx> GotocCtx<'tcx> {
         let msg1 = format!("first argument for {} is finite", intrinsic);
         let msg2 = format!("second argument for {} is finite", intrinsic);
         let loc = self.codegen_span_option(span);
-        let finite_check1 = self.codegen_assert(
-            arg1.is_finite(),
-            PropertyClass::FiniteCheck,
-            msg1.as_str(),
-            loc.clone(),
-        );
-        let finite_check2 = self.codegen_assert(
-            arg2.is_finite(),
-            PropertyClass::FiniteCheck,
-            msg2.as_str(),
-            loc.clone(),
-        );
+        let finite_check1 =
+            self.codegen_assert(arg1.is_finite(), PropertyClass::FiniteCheck, msg1.as_str(), loc);
+        let finite_check2 =
+            self.codegen_assert(arg2.is_finite(), PropertyClass::FiniteCheck, msg2.as_str(), loc);
         Stmt::block(vec![finite_check1, finite_check2, stmt], loc)
     }
 
@@ -703,7 +695,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let mm = self.symbol_table.machine_model();
         let atyp = a.typ();
         let btyp = b.typ();
-        let dividend_is_int_min = if atyp.is_signed(&mm) {
+        let dividend_is_int_min = if atyp.is_signed(mm) {
             a.clone().eq(atyp.min_int_expr(mm))
         } else {
             Expr::bool_false()
@@ -801,7 +793,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         // Otherwise we generate a no-op statement
         let loc = self.codegen_span_option(span);
-        return Stmt::skip(loc);
+        Stmt::skip(loc)
     }
 
     /// An atomic load simply returns the value referenced
@@ -820,7 +812,7 @@ impl<'tcx> GotocCtx<'tcx> {
     ) -> Stmt {
         emit_concurrency_warning!(intrinsic, loc);
         let var1_ref = fargs.remove(0);
-        let var1 = var1_ref.dereference().with_location(loc.clone());
+        let var1 = var1_ref.dereference().with_location(loc);
         let res_stmt = self.codegen_expr_to_place(p, var1);
         Stmt::atomic_block(vec![res_stmt], loc)
     }
@@ -848,19 +840,19 @@ impl<'tcx> GotocCtx<'tcx> {
     ) -> Stmt {
         emit_concurrency_warning!(intrinsic, loc);
         let var1_ref = fargs.remove(0);
-        let var1 = var1_ref.dereference().with_location(loc.clone());
-        let tmp = self.gen_temp_variable(var1.typ().clone(), loc.clone()).to_expr();
-        let decl_stmt = Stmt::decl(tmp.clone(), Some(var1.to_owned()), loc.clone());
-        let var2 = fargs.remove(0).with_location(loc.clone());
-        let var3 = fargs.remove(0).with_location(loc.clone());
-        let eq_expr = (var1.clone()).eq(var2.clone());
-        let assign_stmt = (var1.clone()).assign(var3, loc.clone());
-        let cond_update_stmt = Stmt::if_then_else(eq_expr, assign_stmt, None, loc.clone());
+        let var1 = var1_ref.dereference().with_location(loc);
+        let tmp = self.gen_temp_variable(var1.typ().clone(), loc).to_expr();
+        let decl_stmt = Stmt::decl(tmp.clone(), Some(var1.to_owned()), loc);
+        let var2 = fargs.remove(0).with_location(loc);
+        let var3 = fargs.remove(0).with_location(loc);
+        let eq_expr = (var1.clone()).eq(var2);
+        let assign_stmt = var1.assign(var3, loc);
+        let cond_update_stmt = Stmt::if_then_else(eq_expr, assign_stmt, None, loc);
         let place_type = self.place_ty(p);
         let res_type = self.codegen_ty(place_type);
         let tuple_expr =
             Expr::struct_expr_from_values(res_type, vec![tmp, Expr::c_true()], &self.symbol_table)
-                .with_location(loc.clone());
+                .with_location(loc);
         let res_stmt = self.codegen_expr_to_place(p, tuple_expr);
         Stmt::atomic_block(vec![decl_stmt, cond_update_stmt, res_stmt], loc)
     }
@@ -884,19 +876,19 @@ impl<'tcx> GotocCtx<'tcx> {
     ) -> Stmt {
         emit_concurrency_warning!(intrinsic, loc);
         let var1_ref = fargs.remove(0);
-        let var1 = var1_ref.dereference().with_location(loc.clone());
-        let tmp = self.gen_temp_variable(var1.typ().clone(), loc.clone()).to_expr();
-        let decl_stmt = Stmt::decl(tmp.clone(), Some(var1.to_owned()), loc.clone());
-        let var2 = fargs.remove(0).with_location(loc.clone());
-        let assign_stmt = (var1.clone()).assign(var2, loc.clone());
-        let res_stmt = self.codegen_expr_to_place(p, tmp.clone());
+        let var1 = var1_ref.dereference().with_location(loc);
+        let tmp = self.gen_temp_variable(var1.typ().clone(), loc).to_expr();
+        let decl_stmt = Stmt::decl(tmp.clone(), Some(var1.to_owned()), loc);
+        let var2 = fargs.remove(0).with_location(loc);
+        let assign_stmt = var1.assign(var2, loc);
+        let res_stmt = self.codegen_expr_to_place(p, tmp);
         Stmt::atomic_block(vec![decl_stmt, assign_stmt, res_stmt], loc)
     }
 
     /// Atomic no-ops (e.g., atomic_fence) are transformed into SKIP statements
     fn codegen_atomic_noop(&mut self, intrinsic: &str, loc: Location) -> Stmt {
         emit_concurrency_warning!(intrinsic, loc);
-        let skip_stmt = Stmt::skip(loc.clone());
+        let skip_stmt = Stmt::skip(loc);
         Stmt::atomic_block(vec![skip_stmt], loc)
     }
 
@@ -966,8 +958,8 @@ impl<'tcx> GotocCtx<'tcx> {
         // This comes up specifically when handling the empty string; CBMC will
         // fail on passing a reference to it unless we codegen this zero check.
         let copy_if_nontrivial = count_bytes.is_zero().ternary(dst, copy_call);
-        let copy_expr = if p.is_some() {
-            self.codegen_expr_to_place(p.unwrap(), copy_if_nontrivial)
+        let copy_expr = if let Some(p) = p {
+            self.codegen_expr_to_place(p, copy_if_nontrivial)
         } else {
             copy_if_nontrivial.as_stmt(loc)
         };
@@ -1277,11 +1269,11 @@ impl<'tcx> GotocCtx<'tcx> {
         let newval = fargs.remove(0);
         // Type checker should have ensured it's a vector type
         let elem_ty = cbmc_ret_ty.base_type().unwrap().clone();
-        let tmp = self.gen_temp_variable(cbmc_ret_ty, loc.clone()).to_expr();
+        let tmp = self.gen_temp_variable(cbmc_ret_ty, loc).to_expr();
         Stmt::block(
             vec![
-                Stmt::decl(tmp.clone(), Some(vec), loc.clone()),
-                tmp.clone().index_array(index).assign(newval.cast_to(elem_ty), loc.clone()),
+                Stmt::decl(tmp.clone(), Some(vec), loc),
+                tmp.clone().index_array(index).assign(newval.cast_to(elem_ty), loc),
                 self.codegen_expr_to_place(p, tmp),
             ],
             loc,
@@ -1415,10 +1407,8 @@ impl<'tcx> GotocCtx<'tcx> {
         let layout = self.layout_of(ty);
         let size_of_elem = Expr::int_constant(layout.size.bytes(), res_ty);
         let size_of_count_elems = count.mul_overflow(size_of_elem);
-        let message = format!(
-            "{}: attempt to compute number in bytes which would overflow",
-            intrinsic.to_string()
-        );
+        let message =
+            format!("{}: attempt to compute number in bytes which would overflow", intrinsic);
         let assert_stmt = self.codegen_assert(
             size_of_count_elems.overflowed.not(),
             PropertyClass::ArithmeticOverflow,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index 213271a40ac2..2d1a3312d715 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -40,7 +40,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     _ => projection.goto_expr,
                 }
             }
-            Operand::Constant(c) => self.codegen_constant(&c),
+            Operand::Constant(c) => self.codegen_constant(c),
         }
     }
 
@@ -140,7 +140,7 @@ impl<'tcx> GotocCtx<'tcx> {
         match v {
             ConstValue::Scalar(s) => self.codegen_scalar(s, lit_ty, span),
             ConstValue::Slice { data, start, end } => {
-                self.codegen_slice_value(v, lit_ty, span, &data.inner(), start, end)
+                self.codegen_slice_value(v, lit_ty, span, data.inner(), start, end)
             }
             ConstValue::ByRef { alloc, offset } => {
                 debug!("ConstValue by ref {:?} {:?}", alloc, offset);
@@ -318,7 +318,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 var.clone()
                     .member("case", &tcx.symbol_table)
                     .assign(param.to_expr(), Location::none()),
-                var.clone().ret(Location::none()),
+                var.ret(Location::none()),
             ];
             Symbol::function(
                 &func_name,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 84a90e39f114..5d137ac5cc5d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -482,7 +482,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_get_discriminant(place, pt, res_ty)
             }
             Rvalue::Aggregate(ref k, operands) => {
-                self.codegen_rvalue_aggregate(&*k, operands, res_ty)
+                self.codegen_rvalue_aggregate(k, operands, res_ty)
             }
             Rvalue::ThreadLocalRef(_) => {
                 let typ = self.codegen_ty(res_ty);
@@ -581,10 +581,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let dst_metadata_field = if let Some(vtable_typ) =
             dst_goto_typ.lookup_field_type("vtable", &self.symbol_table)
         {
-            (
-                "vtable",
-                src_goto_expr.member("vtable", &self.symbol_table).cast_to(vtable_typ.clone()),
-            )
+            ("vtable", src_goto_expr.member("vtable", &self.symbol_table).cast_to(vtable_typ))
         } else if let Some(len_typ) = dst_goto_typ.lookup_field_type("len", &self.symbol_table) {
             ("len", src_goto_expr.member("len", &self.symbol_table).cast_to(len_typ))
         } else {
@@ -754,7 +751,7 @@ impl<'tcx> GotocCtx<'tcx> {
         // vtable fat pointer (which can happen with auto trait fat pointers)
         if self.is_vtable_fat_pointer(src_mir_type) {
             self.cast_unsized_dyn_trait_to_unsized_dyn_trait(
-                src_goto_expr.clone(),
+                src_goto_expr,
                 src_mir_type,
                 dst_mir_type,
             )
@@ -766,7 +763,7 @@ impl<'tcx> GotocCtx<'tcx> {
             );
 
             // Sized to unsized cast
-            self.cast_sized_expr_to_unsized_expr(src_goto_expr.clone(), src_mir_type, dst_mir_type)
+            self.cast_sized_expr_to_unsized_expr(src_goto_expr, src_mir_type, dst_mir_type)
         }
     }
 
@@ -920,7 +917,7 @@ impl<'tcx> GotocCtx<'tcx> {
         } else {
             Expr::object_size(temp_var.address_of())
         };
-        let check = Expr::eq(cbmc_size, vt_size.clone());
+        let check = Expr::eq(cbmc_size, vt_size);
         let assert_msg =
             format!("Correct CBMC vtable size for {:?} (MIR type {:?})", ty, operand_type.kind());
         let size_assert =
@@ -1239,7 +1236,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         for (field, expr) in cast_required {
             // Replace the field expression with the cast expression
-            src_goto_field_values.insert(field.clone(), expr.clone());
+            src_goto_field_values.insert(field, expr.clone());
         }
         let dst_goto_expr = Expr::struct_expr(
             self.codegen_ty(dst_mir_type),
@@ -1270,7 +1267,7 @@ impl<'tcx> GotocCtx<'tcx> {
         }
 
         match (src_mir_type.kind(), dst_mir_type.kind()) {
-            (_, ty::Dynamic(..)) => Some((src_mir_type.clone(), dst_mir_type.clone())),
+            (_, ty::Dynamic(..)) => Some((src_mir_type, dst_mir_type)),
             (ty::Adt(..), ty::Adt(..)) => {
                 let src_fields = self.mir_struct_field_types(src_mir_type);
                 let dst_fields = self.mir_struct_field_types(dst_mir_type);
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 612b2093fafc..f424b55befed 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -77,12 +77,8 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             TerminatorKind::Unreachable => Stmt::block(
                 vec![
-                    self.codegen_assert_false(
-                        PropertyClass::Unreachable,
-                        "unreachable code",
-                        loc.clone(),
-                    ),
-                    Stmt::assume(Expr::bool_false(), loc.clone()),
+                    self.codegen_assert_false(PropertyClass::Unreachable, "unreachable code", loc),
+                    Stmt::assume(Expr::bool_false(), loc),
                 ],
                 loc,
             ),
@@ -142,7 +138,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 .codegen_unimplemented(
                     "InlineAsm",
                     Type::empty(),
-                    loc.clone(),
+                    loc,
                     "https://github.com/model-checking/kani/issues/2",
                 )
                 .as_stmt(loc),
@@ -196,8 +192,7 @@ impl<'tcx> GotocCtx<'tcx> {
                             }
                         }
                         let self_data = trait_fat_ptr.to_owned().member("data", &self.symbol_table);
-                        let self_ref =
-                            self_data.clone().cast_to(trait_fat_ptr.typ().clone().to_pointer());
+                        let self_ref = self_data.cast_to(trait_fat_ptr.typ().clone().to_pointer());
 
                         let call =
                             fn_ptr.dereference().call(vec![self_ref]).as_stmt(Location::none());
@@ -332,7 +327,7 @@ impl<'tcx> GotocCtx<'tcx> {
         // ignore_var_ty. So the tuple is always the last arg, but it might be in the
         // first or the second position.
         // Note 2: For empty closures, the only argument needed is the environment struct.
-        if fargs.len() > 0 {
+        if !fargs.is_empty() {
             let tupe = fargs.remove(fargs.len() - 1);
             let tupled_args: Vec<Type> = match self.operand_ty(last_mir_arg.unwrap()).kind() {
                 ty::Tuple(tupled_args) => tupled_args.iter().map(|s| self.codegen_ty(s)).collect(),
@@ -350,7 +345,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     fn codegen_end_call(&self, target: Option<&BasicBlock>, loc: Location) -> Stmt {
         if let Some(next_bb) = target {
-            Stmt::goto(self.current_fn().find_label(&next_bb), loc)
+            Stmt::goto(self.current_fn().find_label(next_bb), loc)
         } else {
             Stmt::assert_sanity_check(
                 Expr::bool_false(),
@@ -433,26 +428,26 @@ impl<'tcx> GotocCtx<'tcx> {
                             idx,
                             destination,
                             &mut fargs,
-                            loc.clone(),
+                            loc,
                         )
                     }
                     // Normal, non-virtual function calls
                     InstanceDef::Item(..)
                     | InstanceDef::DropGlue(_, Some(_))
                     | InstanceDef::Intrinsic(..)
-                    | InstanceDef::FnPtrShim(.., _)
+                    | InstanceDef::FnPtrShim(..)
                     | InstanceDef::VtableShim(..)
                     | InstanceDef::ReifyShim(..)
                     | InstanceDef::ClosureOnceShim { .. }
                     | InstanceDef::CloneShim(..) => {
                         let func_exp = self.codegen_operand(func);
                         vec![
-                            self.codegen_expr_to_place(&destination, func_exp.call(fargs))
-                                .with_location(loc.clone()),
+                            self.codegen_expr_to_place(destination, func_exp.call(fargs))
+                                .with_location(loc),
                         ]
                     }
                 };
-                stmts.push(self.codegen_end_call(target.as_ref(), loc.clone()));
+                stmts.push(self.codegen_end_call(target.as_ref(), loc));
                 return Stmt::block(stmts, loc);
             }
             // Function call through a pointer
@@ -461,9 +456,9 @@ impl<'tcx> GotocCtx<'tcx> {
                 // Actually generate the function call and return.
                 return Stmt::block(
                     vec![
-                        self.codegen_expr_to_place(&destination, func_expr.call(fargs))
-                            .with_location(loc.clone()),
-                        Stmt::goto(self.current_fn().find_label(&target.unwrap()), loc.clone()),
+                        self.codegen_expr_to_place(destination, func_expr.call(fargs))
+                            .with_location(loc),
+                        Stmt::goto(self.current_fn().find_label(&target.unwrap()), loc),
                     ],
                     loc,
                 );
@@ -478,7 +473,7 @@ impl<'tcx> GotocCtx<'tcx> {
         def_id: DefId,
         idx: usize,
         place: &Place<'tcx>,
-        fargs: &mut Vec<Expr>,
+        fargs: &mut [Expr],
         loc: Location,
     ) -> Vec<Stmt> {
         let vtable_field_name = self.vtable_field_name(def_id, idx);
@@ -500,16 +495,12 @@ impl<'tcx> GotocCtx<'tcx> {
         // could be vacuously true.
         let call_is_nonnull = fn_ptr.clone().is_nonnull();
         let assert_msg = format!("Non-null virtual function call for {:?}", vtable_field_name);
-        let assert_nonnull = self.codegen_assert(
-            call_is_nonnull,
-            PropertyClass::DefaultAssertion,
-            &assert_msg,
-            loc.clone(),
-        );
+        let assert_nonnull =
+            self.codegen_assert(call_is_nonnull, PropertyClass::DefaultAssertion, &assert_msg, loc);
 
         // Virtual function call and corresponding nonnull assertion.
         let call = fn_ptr.dereference().call(fargs.to_vec());
-        let call_stmt = self.codegen_expr_to_place(place, call).with_location(loc.clone());
+        let call_stmt = self.codegen_expr_to_place(place, call).with_location(loc);
         let call_stmt = if self.vtable_ctx.emit_vtable_restrictions {
             self.virtual_call_with_restricted_fn_ptr(trait_fat_ptr.typ().clone(), idx, call_stmt)
         } else {
@@ -525,7 +516,7 @@ impl<'tcx> GotocCtx<'tcx> {
         if self.place_ty(p).is_unit() {
             e.as_stmt(Location::none())
         } else {
-            unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(&p))
+            unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(p))
                 .goto_expr
                 .assign(e, Location::none())
         }
@@ -554,7 +545,7 @@ impl<'tcx> GotocCtx<'tcx> {
         Stmt::block(
             vec![
                 self.codegen_assert_false(property_class, msg, loc),
-                BuiltinFn::Abort.call(vec![], loc.clone()).as_stmt(loc.clone()),
+                BuiltinFn::Abort.call(vec![], loc).as_stmt(loc),
             ],
             loc,
         )
@@ -631,7 +622,7 @@ impl<'tcx> GotocCtx<'tcx> {
                             .codegen_unimplemented(
                                 "ty::Generator",
                                 Type::code(vec![], Type::empty()),
-                                location.clone(),
+                                location,
                                 "https://github.com/model-checking/kani/issues/416",
                             )
                             .as_stmt(location);
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs
index 822dfc2fc412..6bd76916fcb6 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs
@@ -34,7 +34,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let typ = self.codegen_ty(self.tcx.type_of(def_id));
         let span = self.tcx.def_span(def_id);
         let location = self.codegen_span(&span);
-        let symbol = Symbol::static_variable(symbol_name.to_string(), base_name, typ, location)
+        let symbol = Symbol::static_variable(symbol_name, base_name, typ, location)
             .with_is_hidden(false) // Static items are always user defined.
             .with_pretty_name(pretty_name);
         self.symbol_table.insert(symbol);
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 1f4e09bdaff3..ad518b73329c 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -16,7 +16,6 @@ use rustc_middle::ty::{
     self, AdtDef, FloatTy, Instance, IntTy, PolyFnSig, Ty, UintTy, VariantDef, VtblEntry,
 };
 use rustc_middle::ty::{List, TypeFoldable};
-use rustc_span;
 use rustc_span::def_id::DefId;
 use rustc_target::abi::{
     Abi::Vector, FieldsShape, Integer, Layout, Primitive, TagEncoding, VariantIdx, Variants,
@@ -139,7 +138,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
             // The leading argument should be exactly the environment
             assert!(prev_args.len() == 1);
-            let env = prev_args[0].clone();
+            let env = prev_args[0];
 
             // Recombine arguments: environment first, then the flattened tuple elements
             let recombined_args = iter::once(env).chain(args);
@@ -1109,7 +1108,7 @@ impl<'tcx> GotocCtx<'tcx> {
                             fields.push(DatatypeComponent::field(
                                 "cases",
                                 ctx.ensure_union(
-                                    &format!("{}-union", name.to_string()),
+                                    &format!("{}-union", name),
                                     NO_PRETTY_NAME,
                                     |ctx, name| {
                                         ctx.codegen_enum_cases(
@@ -1279,7 +1278,7 @@ impl<'tcx> GotocCtx<'tcx> {
         variant: &Layout,
         initial_offset: usize,
     ) -> Type {
-        let case_name = format!("{}::{}", name.to_string(), case.name);
+        let case_name = format!("{}::{}", name, case.name);
         debug!("handling variant {}: {:?}", case_name, case);
         self.ensure_struct(&case_name, NO_PRETTY_NAME, |tcx, _| {
             tcx.codegen_variant_struct_fields(case, subst, variant, initial_offset)
@@ -1291,7 +1290,7 @@ impl<'tcx> GotocCtx<'tcx> {
         debug! {"handling simd with layout {:?}", layout};
 
         let (element, size) = match layout {
-            Vector { element, count } => (element.clone(), count),
+            Vector { element, count } => (element, count),
             _ => unreachable!(),
         };
 
@@ -1345,7 +1344,7 @@ impl<'tcx> GotocCtx<'tcx> {
             if let Some(self_param) = params.first() {
                 let ident = self_param.identifier();
                 let ty = self_param.typ().clone();
-                params[0] = ty.clone().to_pointer().as_parameter(ident, ident);
+                params[0] = ty.to_pointer().as_parameter(ident, ident);
             }
         }
 
@@ -1452,20 +1451,20 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn use_thin_pointer(&self, mir_type: Ty<'tcx>) -> bool {
         // ptr_metadata_ty is not defined on all types, the projection of an associated type
         let (metadata, _check_is_sized) = mir_type.ptr_metadata_ty(self.tcx, normalize_type);
-        return !self.is_unsized(mir_type) || metadata == self.tcx.types.unit;
+        !self.is_unsized(mir_type) || metadata == self.tcx.types.unit
     }
     /// A pointer to the mir type should be a slice fat pointer.
     /// We use a slice fat pointer if the metadata is the slice length (type usize).
     pub fn use_slice_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool {
         let (metadata, _check_is_sized) = mir_type.ptr_metadata_ty(self.tcx, normalize_type);
-        return metadata == self.tcx.types.usize;
+        metadata == self.tcx.types.usize
     }
     /// A pointer to the mir type should be a vtable fat pointer.
     /// We use a vtable fat pointer if this is a fat pointer to anything that is not a slice ptr.
     /// I.e.: The metadata is not length (type usize).
     pub fn use_vtable_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool {
         let (metadata, _check_is_sized) = mir_type.ptr_metadata_ty(self.tcx, normalize_type);
-        return metadata != self.tcx.types.unit && metadata != self.tcx.types.usize;
+        metadata != self.tcx.types.unit && metadata != self.tcx.types.usize
     }
 
     /// Check if the mir type already is a vtable fat pointer.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index 6a39fcd9129b..ef59ea1fc7d7 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -24,9 +24,10 @@ use rustc_session::Session;
 use rustc_target::abi::Endian;
 use rustc_target::spec::PanicStrategy;
 use std::collections::BTreeMap;
+use std::fmt::Write;
 use std::io::BufWriter;
 use std::iter::FromIterator;
-use std::path::PathBuf;
+use std::path::Path;
 use std::rc::Rc;
 use tracing::{debug, warn};
 
@@ -37,7 +38,7 @@ pub struct GotocCodegenBackend {
 
 impl GotocCodegenBackend {
     pub fn new(queries: &Rc<QueryDb>) -> Box<dyn CodegenBackend> {
-        Box::new(GotocCodegenBackend { queries: Rc::clone(&queries) })
+        Box::new(GotocCodegenBackend { queries: Rc::clone(queries) })
     }
 }
 
@@ -58,8 +59,8 @@ impl CodegenBackend for GotocCodegenBackend {
     ) -> Box<dyn Any> {
         super::utils::init();
 
-        check_target(&tcx.sess);
-        check_options(&tcx.sess, need_metadata_module);
+        check_target(tcx.sess);
+        check_options(tcx.sess, need_metadata_module);
 
         let codegen_units: &'tcx [CodegenUnit<'_>] = tcx.collect_and_partition_mono_items(()).1;
         let mut c = GotocCtx::new(tcx, self.queries.clone());
@@ -279,7 +280,7 @@ fn check_options(session: &Session, need_metadata_module: bool) {
     session.abort_if_errors();
 }
 
-fn write_file<T>(base_filename: &PathBuf, extension: &str, source: &T, pretty: bool)
+fn write_file<T>(base_filename: &Path, extension: &str, source: &T, pretty: bool)
 where
     T: serde::Serialize,
 {
@@ -306,7 +307,7 @@ fn print_report<'tcx>(ctx: &GotocCtx, tcx: TyCtxt<'tcx>) {
             .collect();
         let mut msg = String::from("Found the following unsupported constructs:\n");
         unsupported.iter().for_each(|(construct, locations)| {
-            msg += &format!("    - {} ({})\n", construct, locations.len())
+            writeln!(&mut msg, "    - {} ({})", construct, locations.len()).unwrap();
         });
         msg += "\nVerification will fail if one or more of these constructs is reachable.";
         msg += "\nSee https://model-checking.github.io/kani/rust-feature-support.html for more \
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
index 8a0281b1cbf8..09e04df2bedf 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
@@ -55,7 +55,7 @@ impl<'tcx> CurrentFnCtx<'tcx> {
 impl<'tcx> CurrentFnCtx<'tcx> {
     /// Returns the current block, replacing it with an empty vector.
     pub fn extract_block(&mut self) -> Vec<Stmt> {
-        std::mem::replace(&mut self.block, vec![])
+        std::mem::take(&mut self.block)
     }
 
     pub fn get_and_incr_counter(&mut self) -> u64 {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index 862fcf92c21d..2e87c9ce1093 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -189,7 +189,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let name = name.into();
         if !self.symbol_table.contains(name) {
             tracing::debug!(?name, "Ensure global variable");
-            let sym = Symbol::static_variable(name, name, t.clone(), loc)
+            let sym = Symbol::static_variable(name, name, t, loc)
                 .with_is_file_local(is_file_local)
                 .with_is_hidden(false);
             let var = sym.to_expr();
@@ -221,7 +221,7 @@ impl<'tcx> GotocCtx<'tcx> {
         if !self.symbol_table.contains(aggr_tag(struct_name)) {
             let pretty_name = pretty_name.intern();
             // Prevent recursion by inserting an incomplete value.
-            self.symbol_table.insert(Symbol::incomplete_struct(struct_name, pretty_name.clone()));
+            self.symbol_table.insert(Symbol::incomplete_struct(struct_name, pretty_name));
             let components = f(self, struct_name);
             let struct_name: InternedString = struct_name;
             let sym = Symbol::struct_type(struct_name, pretty_name, components);
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs
index 7c9bf2c3de90..a1e829b9b398 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs
@@ -97,8 +97,8 @@ impl VtableCtx {
         assert!(self.emit_vtable_restrictions);
         let site = CallSite {
             trait_method: TraitDefinedMethod { trait_name, vtable_idx: method },
-            function_name: function_name,
-            label: label,
+            function_name,
+            label,
         };
         self.call_sites.push(site);
     }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
index e5dd9c55b64e..7340ba96e602 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -83,8 +83,8 @@ impl<'tcx> GotocHook<'tcx> for ExpectFail {
         let loc = tcx.codegen_span_option(span);
         Stmt::block(
             vec![
-                tcx.codegen_assert(cond, property_class, &msg, loc.clone()),
-                Stmt::goto(tcx.current_fn().find_label(&target), loc.clone()),
+                tcx.codegen_assert(cond, property_class, &msg, loc),
+                Stmt::goto(tcx.current_fn().find_label(&target), loc),
             ],
             loc,
         )
@@ -118,10 +118,7 @@ impl<'tcx> GotocHook<'tcx> for Assume {
         let loc = tcx.codegen_span_option(span);
 
         Stmt::block(
-            vec![
-                Stmt::assume(cond, loc.clone()),
-                Stmt::goto(tcx.current_fn().find_label(&target), loc.clone()),
-            ],
+            vec![Stmt::assume(cond, loc), Stmt::goto(tcx.current_fn().find_label(&target), loc)],
             loc,
         )
     }
@@ -166,19 +163,14 @@ impl<'tcx> GotocHook<'tcx> for Assert {
 
         // Since `cond` might have side effects, assign it to a temporary
         // variable so that it's evaluated once, then assert and assume it
-        let tmp = tcx.gen_temp_variable(cond.typ().clone(), caller_loc.clone()).to_expr();
+        let tmp = tcx.gen_temp_variable(cond.typ().clone(), caller_loc).to_expr();
         Stmt::block(
             vec![
                 reach_stmt,
-                Stmt::decl(tmp.clone(), Some(cond), caller_loc.clone()),
-                tcx.codegen_assert(
-                    tmp.clone(),
-                    PropertyClass::DefaultAssertion,
-                    &msg,
-                    caller_loc.clone(),
-                ),
-                Stmt::assume(tmp, caller_loc.clone()),
-                Stmt::goto(tcx.current_fn().find_label(&target), caller_loc.clone()),
+                Stmt::decl(tmp.clone(), Some(cond), caller_loc),
+                tcx.codegen_assert(tmp.clone(), PropertyClass::DefaultAssertion, &msg, caller_loc),
+                Stmt::assume(tmp, caller_loc),
+                Stmt::goto(tcx.current_fn().find_label(&target), caller_loc),
             ],
             caller_loc,
         )
@@ -219,8 +211,8 @@ impl<'tcx> GotocHook<'tcx> for Nondet {
                     .goto_expr;
             Stmt::block(
                 vec![
-                    pe.clone().assign(tcx.codegen_ty(pt).nondet(), loc.clone()),
-                    Stmt::goto(tcx.current_fn().find_label(&target), loc.clone()),
+                    pe.assign(tcx.codegen_ty(pt).nondet(), loc),
+                    Stmt::goto(tcx.current_fn().find_label(&target), loc),
                 ],
                 loc,
             )
@@ -281,8 +273,8 @@ impl<'tcx> GotocHook<'tcx> for PtrRead {
             vec![
                 unwrap_or_return_codegen_unimplemented_stmt!(tcx, tcx.codegen_place(&assign_to))
                     .goto_expr
-                    .assign(src.dereference().with_location(loc.clone()), loc.clone()),
-                Stmt::goto(tcx.current_fn().find_label(&target), loc.clone()),
+                    .assign(src.dereference().with_location(loc), loc),
+                Stmt::goto(tcx.current_fn().find_label(&target), loc),
             ],
             loc,
         )
@@ -315,8 +307,8 @@ impl<'tcx> GotocHook<'tcx> for PtrWrite {
         let src = fargs.remove(0);
         Stmt::block(
             vec![
-                dst.dereference().assign(src, loc.clone()).with_location(loc.clone()),
-                Stmt::goto(tcx.current_fn().find_label(&target), loc.clone()),
+                dst.dereference().assign(src, loc).with_location(loc),
+                Stmt::goto(tcx.current_fn().find_label(&target), loc),
             ],
             loc,
         )
@@ -351,7 +343,7 @@ impl<'tcx> GotocHook<'tcx> for RustAlloc {
                     .goto_expr
                     .assign(
                         BuiltinFn::Malloc
-                            .call(vec![size], loc.clone())
+                            .call(vec![size], loc)
                             .cast_to(Type::unsigned_int(8).to_pointer()),
                         loc,
                     ),
@@ -389,12 +381,9 @@ impl<'tcx> GotocHook<'tcx> for SliceFromRawPart {
         let len = fargs.remove(0);
         let code = unwrap_or_return_codegen_unimplemented_stmt!(tcx, tcx.codegen_place(&assign_to))
             .goto_expr
-            .assign(
-                Expr::struct_expr_from_values(pt, vec![data, len], &tcx.symbol_table),
-                loc.clone(),
-            )
-            .with_location(loc.clone());
-        Stmt::block(vec![code, Stmt::goto(tcx.current_fn().find_label(&target), loc.clone())], loc)
+            .assign(Expr::struct_expr_from_values(pt, vec![data, len], &tcx.symbol_table), loc)
+            .with_location(loc);
+        Stmt::block(vec![code, Stmt::goto(tcx.current_fn().find_label(&target), loc)], loc)
     }
 }
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
index c1a6af2ee143..590e6b078523 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
@@ -55,7 +55,7 @@ static DEFAULT_HOOK: SyncLazy<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send +
 impl<'tcx> GotocCtx<'tcx> {
     // Calls the closure while updating the tracked global variable marking the
     // codegen item for panic debugging.
-    pub fn call_with_panic_debug_info<F: FnOnce(&mut GotocCtx<'tcx>) -> ()>(
+    pub fn call_with_panic_debug_info<F: FnOnce(&mut GotocCtx<'tcx>)>(
         &mut self,
         call: F,
         panic_debug: String,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
index ee28f916f794..b0f342d8f697 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
@@ -61,18 +61,18 @@ impl<'tcx> GotocCtx<'tcx> {
         if !self.unsupported_constructs.contains_key(&key) {
             self.unsupported_constructs.insert(key, Vec::new());
         }
-        self.unsupported_constructs.get_mut(&key).unwrap().push(loc.clone());
+        self.unsupported_constructs.get_mut(&key).unwrap().push(loc);
 
         let body = vec![
             // Assert false to alert the user that there is a path that uses an unimplemented feature.
             self.codegen_assert_false(
                 PropertyClass::UnsupportedConstruct,
                 &GotocCtx::unsupported_msg(operation_name, Some(url)),
-                loc.clone(),
+                loc,
             ),
             // Assume false to block any further exploration of this path.
-            Stmt::assume(Expr::bool_false(), loc.clone()),
-            t.nondet().as_stmt(loc.clone()).with_location(loc.clone()), //TODO assume rust validity contraints
+            Stmt::assume(Expr::bool_false(), loc),
+            t.nondet().as_stmt(loc).with_location(loc), //TODO assume rust validity contraints
         ];
 
         Expr::statement_expression(body, t).with_location(loc)
@@ -95,9 +95,9 @@ impl<'tcx> GotocCtx<'tcx> {
 
     pub fn unsupported_msg(item: &str, url: Option<&str>) -> String {
         let mut s = format!("{} is not currently supported by Kani", item);
-        if url.is_some() {
+        if let Some(url) = url {
             s.push_str(". Please post your example at ");
-            s.push_str(url.unwrap());
+            s.push_str(url);
         }
         s
     }
diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index 2e8edb1673d8..6755d4473dcf 100644
--- a/kani-compiler/src/main.rs
+++ b/kani-compiler/src/main.rs
@@ -119,7 +119,7 @@ impl Callbacks for KaniCallbacks {}
 /// Generate the arguments to pass to rustc_driver.
 fn generate_rustc_args(args: &ArgMatches) -> Vec<String> {
     let mut gotoc_args =
-        rustc_gotoc_flags(&args.value_of(parser::KANI_LIB).unwrap_or(std::env!("KANI_LIB_PATH")));
+        rustc_gotoc_flags(args.value_of(parser::KANI_LIB).unwrap_or(std::env!("KANI_LIB_PATH")));
     let mut rustc_args = vec![String::from("rustc")];
     if args.is_present(parser::GOTO_C) {
         rustc_args.append(&mut gotoc_args);
diff --git a/kani-compiler/src/parser.rs b/kani-compiler/src/parser.rs
index baf293cc1688..ae48a8e8ead6 100644
--- a/kani-compiler/src/parser.rs
+++ b/kani-compiler/src/parser.rs
@@ -8,48 +8,48 @@ use clap::{
 use std::env;
 
 /// Option name used to set log level.
-pub const LOG_LEVEL: &'static str = "log-level";
+pub const LOG_LEVEL: &str = "log-level";
 
 /// Option name used to enable goto-c compilation.
-pub const GOTO_C: &'static str = "goto-c";
+pub const GOTO_C: &str = "goto-c";
 
 /// Option name used to override Kani library path.
-pub const KANI_LIB: &'static str = "kani-lib";
+pub const KANI_LIB: &str = "kani-lib";
 
 /// Option name used to select symbol table passes.
-pub const SYM_TABLE_PASSES: &'static str = "symbol-table-passes";
+pub const SYM_TABLE_PASSES: &str = "symbol-table-passes";
 
 /// Option name used to set the log output to a json file.
-pub const JSON_OUTPUT: &'static str = "json-output";
+pub const JSON_OUTPUT: &str = "json-output";
 
 /// Option name used to force logger to use color output. This doesn't work with --json-output.
-pub const COLOR_OUTPUT: &'static str = "color-output";
+pub const COLOR_OUTPUT: &str = "color-output";
 
 /// Option name used to dump function pointer restrictions.
-pub const RESTRICT_FN_PTRS: &'static str = "restrict-vtable-fn-ptrs";
+pub const RESTRICT_FN_PTRS: &str = "restrict-vtable-fn-ptrs";
 
 /// Option name used to enable assertion reachability checks.
-pub const ASSERTION_REACH_CHECKS: &'static str = "assertion-reach-checks";
+pub const ASSERTION_REACH_CHECKS: &str = "assertion-reach-checks";
 
 /// Option name used to use json pretty-print for output files.
-pub const PRETTY_OUTPUT_FILES: &'static str = "pretty-json-files";
+pub const PRETTY_OUTPUT_FILES: &str = "pretty-json-files";
 
 /// Option used for suppressing global ASM error.
-pub const IGNORE_GLOBAL_ASM: &'static str = "ignore-global-asm";
+pub const IGNORE_GLOBAL_ASM: &str = "ignore-global-asm";
 
 /// Option name used to override the sysroot.
-pub const SYSROOT: &'static str = "sysroot";
+pub const SYSROOT: &str = "sysroot";
 
 /// Option name used to pass extra rustc-options.
-pub const RUSTC_OPTIONS: &'static str = "rustc-options";
+pub const RUSTC_OPTIONS: &str = "rustc-options";
 
-pub const RUSTC_VERSION: &'static str = "rustc-version";
+pub const RUSTC_VERSION: &str = "rustc-version";
 
 /// Environmental variable used to retrieve extra Kani command arguments.
-const KANIFLAGS_ENV_VAR: &'static str = "KANIFLAGS";
+const KANIFLAGS_ENV_VAR: &str = "KANIFLAGS";
 
 /// Flag used to indicated that we should retrieve more arguments from `KANIFLAGS' env variable.
-const KANI_ARGS_FLAG: &'static str = "--kani-flags";
+const KANI_ARGS_FLAG: &str = "--kani-flags";
 
 /// Configure command options for the Kani compiler.
 pub fn parser<'a, 'b>() -> App<'a, 'b> {
@@ -160,7 +160,7 @@ pub fn command_arguments(args: &Vec<String>) -> Vec<String> {
     if has_kani_flags {
         let mut new_args: Vec<String> = Vec::new();
         new_args.push(args[0].clone());
-        let env_flags = env::var(KANIFLAGS_ENV_VAR).unwrap_or(String::new());
+        let env_flags = env::var(KANIFLAGS_ENV_VAR).unwrap_or_default();
         new_args.extend(
             shell_words::split(&env_flags)
                 .expect(&format!("Cannot parse {} value '{}'", KANIFLAGS_ENV_VAR, env_flags)),
diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs
index 3b46c4e2a88e..37d3f87343f3 100644
--- a/kani-compiler/src/session.rs
+++ b/kani-compiler/src/session.rs
@@ -5,7 +5,6 @@
 
 use crate::parser;
 use clap::ArgMatches;
-use rustc_driver;
 use std::lazy::SyncLazy;
 use std::panic;
 use std::str::FromStr;
@@ -13,7 +12,7 @@ use tracing_subscriber::{filter::Directive, layer::SubscriberExt, EnvFilter, Reg
 use tracing_tree::HierarchicalLayer;
 
 /// Environment variable used to control this session log tracing.
-const LOG_ENV_VAR: &'static str = "KANI_LOG";
+const LOG_ENV_VAR: &str = "KANI_LOG";
 
 // Include Kani's bug reporting URL in our panics.
 const BUG_REPORT_URL: &str =
diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs
index f82ca7426e5e..32a27319daae 100644
--- a/kani-driver/src/args.rs
+++ b/kani-driver/src/args.rs
@@ -179,7 +179,7 @@ impl KaniArgs {
 }
 
 arg_enum! {
-    #[derive(Debug, PartialEq)]
+    #[derive(Debug, PartialEq, Eq)]
     pub enum OutputFormat {
         Regular,
         Terse,
@@ -187,7 +187,7 @@ arg_enum! {
     }
 }
 
-#[derive(Debug, PartialEq)]
+#[derive(Debug, PartialEq, Eq)]
 pub enum AbstractionType {
     Std,
     Kani,
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 636a0df574dc..90c447269053 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -11,7 +11,7 @@ use std::time::Instant;
 use crate::args::KaniArgs;
 use crate::session::KaniSession;
 
-#[derive(PartialEq)]
+#[derive(PartialEq, Eq)]
 pub enum VerificationStatus {
     Success,
     Failure,
@@ -150,15 +150,7 @@ impl KaniSession {
 pub fn resolve_unwind_value(args: &KaniArgs, harness_metadata: &HarnessMetadata) -> Option<u32> {
     // Check for which flag is being passed and prioritize extracting unwind from the
     // respective flag/annotation.
-    if let Some(harness_unwind) = args.unwind {
-        Some(harness_unwind)
-    } else if let Some(annotation_unwind) = harness_metadata.unwind_value {
-        Some(annotation_unwind)
-    } else if let Some(default_unwind) = args.default_unwind {
-        Some(default_unwind)
-    } else {
-        None
-    }
+    args.unwind.or(harness_metadata.unwind_value).or(args.default_unwind)
 }
 
 #[cfg(test)]
diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs
index 0097ac2bbdaa..00d5256cf291 100644
--- a/kani-driver/src/main.rs
+++ b/kani-driver/src/main.rs
@@ -171,7 +171,7 @@ impl KaniSession {
     }
 }
 
-#[derive(Debug, PartialEq)]
+#[derive(Debug, PartialEq, Eq)]
 enum InvocationType {
     CargoKani(Vec<OsString>),
     Standalone,
diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs
index 4d1b37fd6526..1ec5d8c92435 100644
--- a/kani-driver/src/metadata.rs
+++ b/kani-driver/src/metadata.rs
@@ -146,7 +146,7 @@ pub fn mock_proof_harness(name: &str, unwind_value: Option<u32>) -> HarnessMetad
         mangled_name: name.into(),
         original_file: "<unknown>".into(),
         original_line: "<unknown>".into(),
-        unwind_value: unwind_value,
+        unwind_value,
     }
 }
 
diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs
index 83514a64aed4..0cb83279a71d 100644
--- a/kani-driver/src/session.rs
+++ b/kani-driver/src/session.rs
@@ -138,9 +138,7 @@ impl KaniSession {
         let output_file = std::fs::File::create(&stdout)?;
         cmd.stdout(output_file);
 
-        return cmd
-            .status()
-            .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy()));
+        cmd.status().context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy()))
     }
 }
 
diff --git a/kani_metadata/src/vtable.rs b/kani_metadata/src/vtable.rs
index 25cff442c650..ba29b6203ee6 100644
--- a/kani_metadata/src/vtable.rs
+++ b/kani_metadata/src/vtable.rs
@@ -22,7 +22,7 @@ pub struct TraitDefinedMethod {
 /// This is identified by:
 ///   1. The (mangled) name of the function this code is a part of
 ///   2. The (unique) label we applied
-#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
 pub struct CallSite {
     /// The "Trait::method" being invoked at this location
     pub trait_method: TraitDefinedMethod,
@@ -37,7 +37,7 @@ pub struct CallSite {
 }
 
 /// A set of possible targets for a vtable entry's function pointer.
-#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
 pub struct PossibleMethodEntry {
     /// The `Trait::method` entry we have new possibilities for.
     pub trait_method: TraitDefinedMethod,
diff --git a/tools/bookrunner/librustdoc/clean/mod.rs b/tools/bookrunner/librustdoc/clean/mod.rs
index 2459e6504298..9e8a794a7832 100644
--- a/tools/bookrunner/librustdoc/clean/mod.rs
+++ b/tools/bookrunner/librustdoc/clean/mod.rs
@@ -18,8 +18,7 @@ use rustc_hir as hir;
 use rustc_hir::def::{CtorKind, DefKind, Res};
 use rustc_hir::def_id::{DefId, CRATE_DEF_INDEX, LOCAL_CRATE};
 use rustc_middle::middle::resolve_lifetime as rl;
-use rustc_middle::ty::subst::{InternalSubsts, Subst};
-use rustc_middle::ty::{self, AdtKind, DefIdTree, EarlyBinder, Lift, Ty, TyCtxt};
+use rustc_middle::ty::{self, DefIdTree, Lift, Ty, TyCtxt};
 use rustc_middle::{bug, span_bug};
 use rustc_span::hygiene::{AstPass, MacroKind};
 use rustc_span::symbol::{kw, sym, Ident, Symbol};
@@ -1432,7 +1431,7 @@ fn normalize<'tcx>(cx: &mut DocContext<'tcx>, ty: Ty<'_>) -> Option<Ty<'tcx>> {
 }
 
 impl<'tcx> Clean<Type> for Ty<'tcx> {
-    fn clean(&self, cx: &mut DocContext<'_>) -> Type {
+    fn clean(&self, _cx: &mut DocContext<'_>) -> Type {
         trace!("cleaning type: {:?}", self);
         unreachable!();
     }
diff --git a/tools/bookrunner/src/bookrunner.rs b/tools/bookrunner/src/bookrunner.rs
index dddf4f4e4c8a..225c60055dfd 100644
--- a/tools/bookrunner/src/bookrunner.rs
+++ b/tools/bookrunner/src/bookrunner.rs
@@ -68,7 +68,7 @@ impl Tree {
     /// A helper format function that indents each level of the tree.
     fn fmt_aux(&self, p: usize, f: &mut Formatter<'_>) -> Result {
         // Do not print line numbers.
-        if self.children.len() == 0 {
+        if self.children.is_empty() {
             return Ok(());
         }
         // Write `p` spaces into the formatter.
diff --git a/tools/bookrunner/src/books.rs b/tools/bookrunner/src/books.rs
index 70e28998982a..c5b375e9ce81 100644
--- a/tools/bookrunner/src/books.rs
+++ b/tools/bookrunner/src/books.rs
@@ -17,7 +17,6 @@ use rustdoc::{
     doctest::Tester,
     html::markdown::{ErrorCodes, Ignore, LangString},
 };
-use serde_json;
 use std::{
     collections::{HashMap, HashSet},
     ffi::OsStr,
@@ -132,7 +131,7 @@ impl Book {
                         hierarchy_path.push(format!("{}{}", prev_text, text));
                     } else {
                         // If not, add the current title to the hierarchy.
-                        hierarchy_path.push(text.to_string());
+                        hierarchy_path.push(&text);
                     }
                     prev_event_is_text_or_code = true;
                 }
@@ -201,7 +200,7 @@ impl Book {
     fn extract_examples(&self) {
         let mut config_paths = get_config_paths(self.name.as_str());
         for (par_from, par_to) in &self.hierarchy {
-            extract(&par_from, &par_to, &mut config_paths, self.default_edition);
+            extract(par_from, par_to, &mut config_paths, self.default_edition);
         }
         if !config_paths.is_empty() {
             panic!(
@@ -459,7 +458,7 @@ fn paths_to_string(paths: HashSet<PathBuf>) -> String {
 
 /// Creates a new [`Tree`] from `path`, and a test `result`.
 fn tree_from_path(mut path: Vec<String>, result: bool) -> bookrunner::Tree {
-    assert!(path.len() > 0, "Error: `path` must contain at least 1 element.");
+    assert!(!path.is_empty(), "Error: `path` must contain at least 1 element.");
     let mut tree = bookrunner::Tree::new(
         bookrunner::Node::new(
             path.pop().unwrap(),
diff --git a/tools/bookrunner/src/util.rs b/tools/bookrunner/src/util.rs
index 8529afd33b4d..03d286309303 100644
--- a/tools/bookrunner/src/util.rs
+++ b/tools/bookrunner/src/util.rs
@@ -17,7 +17,7 @@ use std::{
 };
 
 /// Step at which Kani should panic.
-#[derive(PartialEq)]
+#[derive(PartialEq, Eq)]
 pub enum FailStep {
     /// Kani panics before the codegen step (up to MIR generation). This step
     /// runs the same checks on the test code as `cargo check` including syntax,
@@ -113,7 +113,7 @@ fn try_parse_args(cur_args: Vec<String>, name: &str, line: &str) -> Vec<String>
     let name = format!("{}-flags:", name);
     let mut split = line.split(&name).skip(1);
     let args: Vec<String> = if let Some(rest) = split.next() {
-        rest.trim().split_whitespace().map(String::from).collect()
+        rest.split_whitespace().map(String::from).collect()
     } else {
         Vec::new()
     };
diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs
index 29f47a11bb51..f186f5251933 100644
--- a/tools/compiletest/src/main.rs
+++ b/tools/compiletest/src/main.rs
@@ -349,7 +349,7 @@ fn common_inputs_stamp() -> Stamp {
     let kani_bin_path = &rust_src_dir.join("target/debug/kani-compiler");
 
     // Create stamp based on the `kani-compiler` binary
-    let mut stamp = Stamp::from_path(&kani_bin_path);
+    let mut stamp = Stamp::from_path(kani_bin_path);
 
     // Add source, library and script directories
     stamp.add_dir(&rust_src_dir.join("src/"));
diff --git a/tools/make-kani-release/src/main.rs b/tools/make-kani-release/src/main.rs
index ecb9044210fc..aa5da20d1637 100644
--- a/tools/make-kani-release/src/main.rs
+++ b/tools/make-kani-release/src/main.rs
@@ -57,7 +57,7 @@ fn prebundle(dir: &Path) -> Result<()> {
         );
     }
 
-    if !which::which("cbmc").is_ok() {
+    if which::which("cbmc").is_err() {
         bail!("Couldn't find the 'cbmc' binary to include in the release bundle.");
     }