combine sign extend

cucapra · Nov 21, 2024 · cf9724e · cf9724e
1 parent 398caca
commit cf9724e
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/src/expr/simplify.rs b/src/expr/simplify.rs
@@ -135,7 +135,7 @@ fn simplify_bv_equal(ctx: &mut Context, a: ExprRef, b: ExprRef) -> Option<ExprRe
             debug_assert!(!va.get(ctx).is_equal(&vb.get(ctx)));
             Some(ctx.fals())
         }
-        Lits::One((lit, lit_expr), expr) => {
+        Lits::One((lit, _), expr) => {
             if lit.is_true() {
                 // a == true -> a
                 Some(expr)
@@ -281,6 +281,11 @@ fn simplify_bv_sign_ext(ctx: &mut Context, e: ExprRef, by: WidthInt) -> Option<E
     } else {
         match ctx.get(e) {
             Expr::BVLiteral(value) => Some(ctx.bv_lit(&value.get(ctx).sign_extend(by))),
+            Expr::BVSignExt {
+                e: inner_e,
+                by: inner_by,
+                ..
+            } => Some(ctx.sign_extend(*inner_e, by + inner_by)),
             _ => None,
         }
     }