From 39f7024243adc2f5d1568ac471af595b9b4c6bce Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Tue, 19 Dec 2023 09:40:40 -0800
Subject: [PATCH] Clippy fixes

---
 boogie_ast/src/boogie_program/mod.rs                |  3 ++-
 .../src/codegen_boogie/context/boogie_ctx.rs        | 13 ++++++-------
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/boogie_ast/src/boogie_program/mod.rs b/boogie_ast/src/boogie_program/mod.rs
index 93bfbeba9474..d62735eeefc4 100644
--- a/boogie_ast/src/boogie_program/mod.rs
+++ b/boogie_ast/src/boogie_program/mod.rs
@@ -188,7 +188,8 @@ impl Expr {
         Expr::FunctionCall { symbol, arguments }
     }
 
-    pub fn sign_extend(_e: Box<Expr>, _width: usize) -> Self {
+    pub fn sign_extend(e: Box<Expr>, _width: usize) -> Self {
+        let _e = e;
         todo!()
     }
 
diff --git a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
index 985816768938..bdd66f9b7ffe 100644
--- a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
+++ b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use itertools::Itertools;
+use std::cmp::Ordering;
 use std::io::Write;
 
 use crate::kani_queries::QueryDb;
@@ -329,16 +330,14 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
                     let to = self.codegen_type(*ty);
                     let Type::Bv(from_width) = from else { panic!("Expecting bv type in cast") };
                     let Type::Bv(to_width) = to else { panic!("Expecting bv type in cast") };
-                    let op = if from_width > to_width {
-                        Expr::extract(Box::new(o), to_width, 0)
-                    } else if from_width < to_width {
-                        match from_type.kind() {
+                    let op = match from_width.cmp(&to_width) {
+                        Ordering::Greater => Expr::extract(Box::new(o), to_width, 0),
+                        Ordering::Less => match from_type.kind() {
                             ty::Int(_) => Expr::sign_extend(Box::new(o), to_width - from_width),
                             ty::Uint(_) => Expr::zero_extend(Box::new(o), to_width - from_width),
                             _ => todo!(),
-                        }
-                    } else {
-                        o
+                        },
+                        Ordering::Equal => o,
                     };
                     (None, op)
                 } else {