diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index 0f78b416cf4..204910b8d65 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -1618,8 +1618,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             mir::Rvalue::BinaryOp(op, box (ref left, ref right)) => {
                 self.encode_assign_binary_op(op, left, right, encoded_lhs, ty, location)?
             }
-            mir::Rvalue::CheckedBinaryOp(_, _) => {
-                todo!()
+            mir::Rvalue::CheckedBinaryOp(op, box (ref left, ref right)) => {
+                self.encode_assign_checked_binary_op(op, left, right, encoded_lhs, ty, location)?
             }
             mir::Rvalue::UnaryOp(op, ref operand) => {
                 self.encode_assign_unary_op(op, operand, encoded_lhs, ty, location)?