diff --git a/charon/src/driver.rs b/charon/src/driver.rs
index c41593ebd..64528fe6d 100644
--- a/charon/src/driver.rs
+++ b/charon/src/driver.rs
@@ -2,6 +2,7 @@ use crate::cli_options;
 use crate::export;
 use crate::get_mir::MirLevel;
 use crate::reorder_decls;
+use crate::transform::remove_arithmetic_overflow_checks;
 use crate::transform::{
     index_to_function_calls, insert_assign_return_unit, ops_to_function_calls, reconstruct_asserts,
     remove_drop_never, remove_dynamic_checks, remove_nops, remove_read_discriminant,
@@ -313,6 +314,12 @@ pub fn translate(
         // which ignores this first variable. This micro-pass updates this.
         update_closure_signatures::transform(&ctx, &mut llbc_funs);
 
+        // # Micro-pass: remove the dynamic checks we couldn't remove in [`remove_dynamic_checks`].
+        // **WARNING**: this pass uses the fact that the dynamic checks
+        // introduced by Rustc use a special "assert" construct. Because of
+        // this, it must happen *before* the [reconstruct_asserts] pass.
+        remove_arithmetic_overflow_checks::transform(&mut ctx, &mut llbc_funs, &mut llbc_globals);
+
         // # Micro-pass: reconstruct the asserts
         reconstruct_asserts::transform(&mut ctx, &mut llbc_funs, &mut llbc_globals);
 
diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs
index ae2e8f860..29e8727ad 100644
--- a/charon/src/transform/mod.rs
+++ b/charon/src/transform/mod.rs
@@ -2,6 +2,7 @@ pub mod index_to_function_calls;
 pub mod insert_assign_return_unit;
 pub mod ops_to_function_calls;
 pub mod reconstruct_asserts;
+pub mod remove_arithmetic_overflow_checks;
 pub mod remove_drop_never;
 pub mod remove_dynamic_checks;
 pub mod remove_nops;
diff --git a/charon/src/transform/remove_arithmetic_overflow_checks.rs b/charon/src/transform/remove_arithmetic_overflow_checks.rs
new file mode 100644
index 000000000..f42e481d0
--- /dev/null
+++ b/charon/src/transform/remove_arithmetic_overflow_checks.rs
@@ -0,0 +1,117 @@
+//! # Micro-pass: remove the overflow checks for arithmetic operations we couldn't remove in
+//! [`remove_dynamic_checks`]. See comments there for more details.
+use crate::formatter::{Formatter, IntoFormatter};
+use crate::llbc_ast::*;
+use crate::translate_ctx::TransCtx;
+use crate::types::*;
+use take_mut::take;
+
+struct RemoveDynChecks;
+
+impl RemoveDynChecks {
+    /// After `remove_dynamic_checks`, the only remaining dynamic checks are overflow checks. We
+    /// couldn't remove them in ullbc because the generated code spans two basic blocks. They are
+    /// inserted only in constants since we otherwise compile in release mode. These assertions
+    /// look like:
+    /// ```text
+    /// r := x checked.+ y;
+    /// assert(move r.1 == false);
+    /// z := move r.0;
+    /// ```
+    /// We replace that with:
+    /// ```text
+    /// z := x + y;
+    /// ```
+    fn simplify(&mut self, s: &mut Statement) {
+        if let RawStatement::Sequence(s0, s1) = &mut s.content {
+            if let RawStatement::Sequence(s1, s2) = &mut s1.content {
+                // TODO: the last statement is not necessarily a sequence
+                if let RawStatement::Sequence(s2, _) = &mut s2.content {
+                    if let (
+                        RawStatement::Assign(
+                            binop,
+                            Rvalue::BinaryOp(
+                                op @ (BinOp::CheckedAdd | BinOp::CheckedSub | BinOp::CheckedMul),
+                                _,
+                                _,
+                            ),
+                        ),
+                        RawStatement::Assert(Assert {
+                            cond: Operand::Move(assert_cond),
+                            expected: false,
+                        }),
+                        RawStatement::Assign(final_value, Rvalue::Use(Operand::Move(assigned))),
+                    ) = (&mut s0.content, &s1.content, &mut s2.content)
+                    {
+                        // assigned should be: binop.0
+                        // assert_cond should be: binop.1
+                        if let (
+                            [ProjectionElem::Field(FieldProjKind::Tuple(..), fid0)],
+                            [ProjectionElem::Field(FieldProjKind::Tuple(..), fid1)],
+                        ) = (
+                            assigned.projection.as_slice(),
+                            assert_cond.projection.as_slice(),
+                        ) {
+                            if assert_cond.var_id == binop.var_id
+                                && assigned.var_id == binop.var_id
+                                && binop.projection.len() == 0
+                                && fid0.index() == 0
+                                && fid1.index() == 1
+                            {
+                                // Switch to the unchecked operation.
+                                *op = match op {
+                                    BinOp::CheckedAdd => BinOp::Add,
+                                    BinOp::CheckedSub => BinOp::Sub,
+                                    BinOp::CheckedMul => BinOp::Mul,
+                                    _ => unreachable!(),
+                                };
+                                // Assign to the correct value in `s0`.
+                                std::mem::swap(binop, final_value);
+                                // Remove `s1` and `s2`.
+                                take(s, |s| {
+                                    let (s0, s1) = s.content.to_sequence();
+                                    let (_s1, s2) = s1.content.to_sequence();
+                                    let (_s2, s3) = s2.content.to_sequence();
+                                    Statement {
+                                        meta: s0.meta,
+                                        content: RawStatement::Sequence(s0, s3),
+                                    }
+                                });
+                            }
+                        }
+                    }
+                }
+            }
+        }
+    }
+}
+
+impl MutTypeVisitor for RemoveDynChecks {}
+impl MutExprVisitor for RemoveDynChecks {}
+
+impl MutAstVisitor for RemoveDynChecks {
+    fn spawn(&mut self, visitor: &mut dyn FnMut(&mut Self)) {
+        visitor(self)
+    }
+
+    fn merge(&mut self) {}
+
+    fn visit_statement(&mut self, s: &mut Statement) {
+        // Simplify this statement.
+        self.simplify(s);
+        // Recurse into subsequent statements.
+        self.default_visit_raw_statement(&mut s.content);
+    }
+}
+
+pub fn transform(ctx: &mut TransCtx, funs: &mut FunDecls, globals: &mut GlobalDecls) {
+    ctx.iter_bodies(funs, globals, |ctx, name, b| {
+        let fmt_ctx = ctx.into_fmt();
+        trace!(
+            "# About to remove the remaining overflow checks: {}:\n{}",
+            name.fmt_with_ctx(&fmt_ctx),
+            fmt_ctx.format_object(&*b)
+        );
+        RemoveDynChecks.visit_statement(&mut b.body);
+    })
+}
diff --git a/charon/src/transform/remove_dynamic_checks.rs b/charon/src/transform/remove_dynamic_checks.rs
index 79e1289b6..ee947bc7e 100644
--- a/charon/src/transform/remove_dynamic_checks.rs
+++ b/charon/src/transform/remove_dynamic_checks.rs
@@ -100,8 +100,8 @@ fn remove_dynamic_checks(ctx: &mut TransCtx, block: &mut BlockData) {
         // Overflow checks for addition/subtraction/multiplication. They look like:
         //   r := x checked.+ y;
         //   assert(move r.1 == false);
-        // They only happen in constants because we compile with `-C opt-level=3`. They're tricky
-        // to remove so we leave them for now.
+        // They only happen in constants because we compile with `-C opt-level=3`. They span two
+        // blocks so we remove them in a later pass.
         [.., Statement {
             content:
                 RawStatement::Assign(result, Rvalue::BinaryOp(BinOp::CheckedAdd | BinOp::CheckedSub | BinOp::CheckedMul, ..)),
@@ -112,7 +112,8 @@ fn remove_dynamic_checks(ctx: &mut TransCtx, block: &mut BlockData) {
             && p_id.index() == 1
             && *expected == false =>
         {
-            // We leave this assert intact.
+            // We leave this assert intact; it will be silplified in
+            // [`remove_arithmetic_overflow_checks`].
             return
         }
 
diff --git a/charon/tests/ui/remove-dynamic-checks.out b/charon/tests/ui/remove-dynamic-checks.out
index babd9b942..799887f19 100644
--- a/charon/tests/ui/remove-dynamic-checks.out
+++ b/charon/tests/ui/remove-dynamic-checks.out
@@ -373,21 +373,15 @@ fn test_crate::shr(@1: u32, @2: u32) -> u32
 
 global test_crate::_  {
     let @0: isize; // return
-    let @1: (isize, bool); // anonymous local
 
-    @1 := const (1 : isize) checked.+ const (1 : isize)
-    assert(move ((@1).1) == false)
-    @0 := move ((@1).0)
+    @0 := const (1 : isize) + const (1 : isize)
     return
 }
 
 global test_crate::_#1  {
     let @0: isize; // return
-    let @1: (isize, bool); // anonymous local
 
-    @1 := const (1 : isize) checked.- const (1 : isize)
-    assert(move ((@1).1) == false)
-    @0 := move ((@1).0)
+    @0 := const (1 : isize) - const (1 : isize)
     return
 }
 
@@ -400,11 +394,8 @@ global test_crate::_#2  {
 
 global test_crate::_#3  {
     let @0: isize; // return
-    let @1: (isize, bool); // anonymous local
 
-    @1 := const (2 : isize) checked.* const (2 : isize)
-    assert(move ((@1).1) == false)
-    @0 := move ((@1).0)
+    @0 := const (2 : isize) * const (2 : isize)
     return
 }
 
@@ -445,37 +436,28 @@ global test_crate::FOO  {
 
 global test_crate::_#8  {
     let @0: u32; // return
-    let @1: (u32, bool); // anonymous local
-    let @2: u32; // anonymous local
+    let @1: u32; // anonymous local
 
-    @2 := test_crate::FOO
-    @1 := const (1 : u32) checked.+ move (@2)
-    assert(move ((@1).1) == false)
-    @0 := move ((@1).0)
+    @1 := test_crate::FOO
+    @0 := const (1 : u32) + move (@1)
     return
 }
 
 global test_crate::_#9  {
     let @0: u32; // return
-    let @1: (u32, bool); // anonymous local
-    let @2: u32; // anonymous local
+    let @1: u32; // anonymous local
 
-    @2 := test_crate::FOO
-    @1 := const (1 : u32) checked.- move (@2)
-    assert(move ((@1).1) == false)
-    @0 := move ((@1).0)
+    @1 := test_crate::FOO
+    @0 := const (1 : u32) - move (@1)
     return
 }
 
 global test_crate::_#10  {
     let @0: u32; // return
-    let @1: (u32, bool); // anonymous local
-    let @2: u32; // anonymous local
+    let @1: u32; // anonymous local
 
-    @2 := test_crate::FOO
-    @1 := const (2 : u32) checked.* move (@2)
-    assert(move ((@1).1) == false)
-    @0 := move ((@1).0)
+    @1 := test_crate::FOO
+    @0 := const (2 : u32) * move (@1)
     return
 }