From acb67a91543274e2b400f3953361d7bf7b0c46b9 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Fri, 1 Mar 2024 16:01:21 +0100 Subject: [PATCH] Optimize encoding of mir::BinOp::Rem for unsigned integers --- prusti-viper/src/encoder/mir_encoder/mod.rs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/prusti-viper/src/encoder/mir_encoder/mod.rs b/prusti-viper/src/encoder/mir_encoder/mod.rs index 8712faff6e1..700807d8833 100644 --- a/prusti-viper/src/encoder/mir_encoder/mod.rs +++ b/prusti-viper/src/encoder/mir_encoder/mod.rs @@ -487,7 +487,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> MirEncoder<'p, 'v, 'tcx> { mir::BinOp::Le => vir::Expr::le_cmp(left, right), mir::BinOp::AddUnchecked | mir::BinOp::Add => vir::Expr::add(left, right), mir::BinOp::SubUnchecked | mir::BinOp::Sub => vir::Expr::sub(left, right), - mir::BinOp::Rem => vir::Expr::rem(left, right), + mir::BinOp::Rem => { + if matches!(ty.kind(), ty::TyKind::Uint(_)) { + vir::Expr::modulo(left, right) + } else { + vir::Expr::rem(left, right) + } + } mir::BinOp::Div => vir::Expr::div(left, right), mir::BinOp::MulUnchecked | mir::BinOp::Mul => vir::Expr::mul(left, right), mir::BinOp::BitAnd if is_bool => vir::Expr::and(left, right),