diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs
index 80347ea1c5..90cd0df8db 100644
--- a/source/rust_verify/src/rust_to_vir_expr.rs
+++ b/source/rust_verify/src/rust_to_vir_expr.rs
@@ -1846,6 +1846,43 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
         mk_expr(ExprX::Const(c))
     };
 
+    let cond_let_expr_to_vir_match = |cond: &Expr<'tcx>,
+                                      lhs_body,
+                                      lhs_span,
+                                      rhs_body,
+                                      rhs_span|
+     -> Result<ExprX, VirErr> {
+        let ExprKind::Let(LetExpr { pat, init: expr, .. }) = &cond.kind else {
+            panic!("Expected let expression");
+        };
+        // if let
+        let vir_place = expr_to_vir_place(bctx, expr)?;
+        let vir_place = simplify_place_by_cancelling(&vir_place);
+        let mut vir_arms: Vec<vir::ast::Arm> = Vec::new();
+        /* lhs */
+        {
+            let pattern = pattern_to_vir(bctx, pat)?;
+            let guard =
+                bctx.spanned_typed_new(expr.span, &bool_typ(), ExprX::Const(Constant::Bool(true)));
+            let vir_arm = ArmX { pattern, guard, body: lhs_body };
+            vir_arms.push(bctx.spanned_new(lhs_span, vir_arm));
+        }
+        /* rhs */
+        {
+            let pat_typ = vir_arms[0].x.pattern.typ.clone();
+            let pattern = bctx.spanned_typed_new(cond.span, &pat_typ, PatternX::Wildcard(false));
+            {
+                let mut erasure_info = bctx.ctxt.erasure_info.borrow_mut();
+                erasure_info.hir_vir_ids.push((cond.hir_id, pattern.span.id));
+            }
+            let guard =
+                bctx.spanned_typed_new(expr.span, &bool_typ(), ExprX::Const(Constant::Bool(true)));
+            let vir_arm = ArmX { pattern, guard, body: rhs_body };
+            vir_arms.push(bctx.spanned_new(rhs_span, vir_arm));
+        }
+        Ok(ExprX::Match(vir_place, Arc::new(vir_arms)))
+    };
+
     let expr_attrs = bctx.ctxt.tcx.hir_attrs(expr.hir_id);
     let expr_vattrs = bctx.ctxt.get_verifier_attrs(expr_attrs)?;
     if expr_vattrs.truncate {
@@ -2659,46 +2696,22 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
         ExprKind::If(cond, lhs, rhs) => {
             let cond = cond.peel_drop_temps();
             match cond.kind {
-                ExprKind::Let(LetExpr { pat, init: expr, ty: _, span: _, recovered: _ }) => {
-                    // if let
-                    let vir_place = expr_to_vir_place(bctx, expr)?;
-                    let vir_place = simplify_place_by_cancelling(&vir_place);
-                    let mut vir_arms: Vec<vir::ast::Arm> = Vec::new();
-                    /* lhs */
-                    {
-                        let pattern = pattern_to_vir(bctx, pat)?;
-                        let guard = bctx.spanned_typed_new(
-                            expr.span,
-                            &bool_typ(),
-                            ExprX::Const(Constant::Bool(true)),
-                        );
-                        let body = expr_to_vir_consume(bctx, &lhs)?;
-                        let vir_arm = ArmX { pattern, guard, body };
-                        vir_arms.push(bctx.spanned_new(lhs.span, vir_arm));
-                    }
-                    /* rhs */
-                    {
-                        let pat_typ = vir_arms[0].x.pattern.typ.clone();
-                        let pattern =
-                            bctx.spanned_typed_new(cond.span, &pat_typ, PatternX::Wildcard(false));
-                        {
-                            let mut erasure_info = bctx.ctxt.erasure_info.borrow_mut();
-                            erasure_info.hir_vir_ids.push((cond.hir_id, pattern.span.id));
-                        }
-                        let guard = bctx.spanned_typed_new(
-                            expr.span,
-                            &bool_typ(),
-                            ExprX::Const(Constant::Bool(true)),
-                        );
-                        let body = if let Some(rhs) = rhs {
-                            expr_to_vir_consume(bctx, &rhs)?
-                        } else {
-                            mk_expr(ExprX::Block(Arc::new(Vec::new()), None))?.expect_expr()
-                        };
-                        let vir_arm = ArmX { pattern, guard, body };
-                        vir_arms.push(bctx.spanned_new(lhs.span, vir_arm));
-                    }
-                    mk_expr(ExprX::Match(vir_place, Arc::new(vir_arms)))
+                ExprKind::Let(_) => {
+                    let (rhs_vir, rhs_span) = if let Some(rhs) = rhs {
+                        (expr_to_vir_consume(bctx, &rhs)?, rhs.span)
+                    } else {
+                        (
+                            mk_expr(ExprX::Block(Arc::new(Vec::new()), None))?.expect_expr(),
+                            cond.span,
+                        )
+                    };
+                    mk_expr(cond_let_expr_to_vir_match(
+                        cond,
+                        expr_to_vir_consume(bctx, &lhs)?,
+                        lhs.span,
+                        rhs_vir,
+                        rhs_span,
+                    )?)
                 }
                 _ => {
                     let vir_cond = expr_to_vir_consume(bctx, cond)?;
@@ -2828,9 +2841,34 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
             } else {
                 unsupported_err!(expr.span, "loop else");
             }
-            let cond = Some(expr_to_vir_consume(bctx, cond)?);
+            let body_span = body.span;
             let mut body = expr_to_vir_consume(bctx, body)?;
             let header = vir::headers::read_header(&mut body, &vir::headers::HeaderAllows::Loop)?;
+            let (cond, body) = match &cond.peel_drop_temps().kind {
+                ExprKind::Let(_) => {
+                    let body_ty = body.typ.clone();
+                    let wildcard_body = bctx.spanned_typed_new(
+                        cond.span,
+                        &body_ty,
+                        ExprX::BreakOrContinue { label: None, is_break: true },
+                    );
+                    (
+                        None,
+                        bctx.spanned_typed_new(
+                            cond.span,
+                            &body_ty,
+                            cond_let_expr_to_vir_match(
+                                cond,
+                                body,
+                                body_span,
+                                wildcard_body,
+                                cond.span,
+                            )?,
+                        ),
+                    )
+                }
+                _ => (Some(expr_to_vir_consume(bctx, cond)?), body),
+            };
             let label = label.map(|l| l.ident.to_string());
             Ok(ExprOrPlace::Expr(bctx.spanned_typed_new(
                 *header_span,
diff --git a/source/rust_verify_test/tests/loops.rs b/source/rust_verify_test/tests/loops.rs
index c368ad8fce..9b5c110a6d 100644
--- a/source/rust_verify_test/tests/loops.rs
+++ b/source/rust_verify_test/tests/loops.rs
@@ -18,6 +18,27 @@ test_verify_one_file! {
     } => Ok(())
 }
 
+test_verify_one_file! {
+    #[test] while_let_loop verus_code! {
+        enum MaybeU64 {
+            Some(u64),
+            None,
+        }
+
+        fn test1() {
+            let mut i: u64 = 0;
+            while let MaybeU64::Some(x) = if i < 1 { MaybeU64::Some(i) } else { MaybeU64::None }
+                invariant i <= 1
+                decreases 1 - i
+            {
+                assert(x == i);
+                i = i + 1;
+            }
+            assert(i <= 1);
+        }
+    } => Ok(())
+}
+
 test_verify_one_file! {
     #[test] basic_while_fail1 verus_code! {
         fn test1() {