From 50b973ba3031cb89985e08296ff06dade3e83798 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Wed, 19 Feb 2025 18:14:29 +0100
Subject: [PATCH] Remove useless unit locals

---
 charon/src/ast/expressions_utils.rs           |  14 +
 charon/src/ast/gast_utils.rs                  |   5 +
 .../transform/insert_assign_return_unit.rs    |  11 +-
 charon/src/transform/mod.rs                   |   5 +-
 charon/src/transform/remove_unit_locals.rs    |  75 ++
 charon/tests/cargo/build-script.out           |   4 +-
 charon/tests/cargo/dependencies.out           |  11 +-
 charon/tests/cargo/toml.out                   |   4 +-
 charon/tests/ui/arrays.out                    | 534 +++++-----
 charon/tests/ui/associated-types.out          |   4 +-
 .../tests/ui/call-to-known-trait-method.out   |   8 +-
 charon/tests/ui/comments.out                  | 128 +--
 charon/tests/ui/demo.out                      |  64 +-
 charon/tests/ui/disambiguator.out             |   8 +-
 charon/tests/ui/diverging.out                 |   4 +-
 charon/tests/ui/dyn-trait.out                 |   8 +-
 charon/tests/ui/external.out                  |   8 +-
 charon/tests/ui/impl-trait.out                |  16 +-
 charon/tests/ui/issue-114-opaque-bodies.out   |   8 +-
 charon/tests/ui/issue-118-generic-copy.out    |  12 +-
 charon/tests/ui/issue-165-vec-macro.out       |   8 +-
 charon/tests/ui/issue-297-cfg.out             | 311 +++---
 charon/tests/ui/issue-320-slice-pattern.out   | 112 +--
 .../ui/issue-322-macro-disambiguator.out      |  10 +-
 charon/tests/ui/issue-323-closure-borrow.out  |  12 +-
 .../ui/issue-372-type-param-out-of-range.out  |  12 +-
 charon/tests/ui/issue-378-ctor-as-fn.out      |   4 +-
 .../tests/ui/issue-4-slice-try-into-array.out |   4 +-
 charon/tests/ui/issue-4-traits.out            |   4 +-
 charon/tests/ui/issue-45-misc.out             |  74 +-
 charon/tests/ui/issue-507-cfg.out             | 109 +-
 .../issue-70-override-provided-method.2.out   |  32 +-
 .../issue-70-override-provided-method.3.out   |  20 +-
 .../ui/issue-70-override-provided-method.out  |   4 +-
 .../tests/ui/issue-72-hash-missing-impl.out   |   8 +-
 charon/tests/ui/issue-73-extern.out           |   4 +-
 .../ui/issue-91-enum-to-discriminant-cast.out |   4 +-
 .../issue-92-nonpositive-variant-indices.out  |  12 +-
 .../issue-97-missing-parent-item-clause.out   |   4 +-
 charon/tests/ui/iterator.out                  | 342 +++----
 charon/tests/ui/loops.out                     | 933 +++++++-----------
 .../tests/ui/method-impl-generalization.out   |   8 +-
 charon/tests/ui/ml-name-matcher-tests.out     |  16 +-
 charon/tests/ui/no_nested_borrows.out         |  43 +-
 charon/tests/ui/opacity.out                   |   4 +-
 charon/tests/ui/opaque-trait.out              |  28 +-
 charon/tests/ui/opaque_attribute.out          |   4 +-
 charon/tests/ui/panics.out                    |  14 +-
 .../ui/predicates-on-late-bound-vars.out      |   4 +-
 charon/tests/ui/ptr_to_promoted.out           |   4 +-
 charon/tests/ui/quantified-clause.out         |   8 +-
 charon/tests/ui/reconstruct_early_return.out  |  71 +-
 charon/tests/ui/remove-dynamic-checks.out     |  32 +-
 charon/tests/ui/rust-name-matcher-tests.out   |  16 +-
 charon/tests/ui/rvalues.out                   |  32 +-
 charon/tests/ui/send_bound.out                |   8 +-
 .../assoc-ty-via-supertrait-and-bounds.out    |   4 +-
 .../call-inherent-method-with-trait-bound.out |  16 +-
 .../call-method-via-supertrait-bound.out      |   8 +-
 ...lt-method-with-clause-and-marker-trait.out |   4 +-
 .../simple/fewer-clauses-in-method-impl.out   |   4 +-
 ...ulted-method-with-clause-with-assoc-ty.out |   8 +-
 .../generic-impl-with-defaulted-method.out    |   8 +-
 .../ui/simple/generic-impl-with-method.out    |   4 +-
 .../opaque-trait-with-clause-in-method.out    |   4 +-
 .../pass-higher-kinded-fn-item-as-closure.out |   8 +-
 .../quantified-trait-type-constraint.out      |   4 +-
 ...rtrait-impl-with-assoc-type-constraint.out |   4 +-
 charon/tests/ui/skip-borrowck.out             |  16 +-
 charon/tests/ui/statics.out                   |  16 +-
 charon/tests/ui/string-literal.out            |   4 +-
 charon/tests/ui/traits.out                    |  28 +-
 .../ui/type_inference_is_order_dependent.out  |   4 +-
 charon/tests/ui/typenum.out                   |   8 +-
 charon/tests/ui/ullbc-control-flow.out        | 180 ++--
 charon/tests/ui/unions.out                    |   7 +-
 charon/tests/ui/unsafe.out                    |  16 +-
 charon/tests/ui/unsize.out                    |   4 +-
 .../ui/unsupported/issue-79-bound-regions.out |   4 +-
 79 files changed, 1445 insertions(+), 2164 deletions(-)
 create mode 100644 charon/src/transform/remove_unit_locals.rs

diff --git a/charon/src/ast/expressions_utils.rs b/charon/src/ast/expressions_utils.rs
index 394d6a8ba..9ec3f86de 100644
--- a/charon/src/ast/expressions_utils.rs
+++ b/charon/src/ast/expressions_utils.rs
@@ -43,6 +43,20 @@ impl Place {
     }
 }
 
+impl Rvalue {
+    pub fn unit_value() -> Self {
+        Rvalue::Aggregate(
+            AggregateKind::Adt(
+                TypeId::Tuple,
+                None,
+                None,
+                GenericArgs::empty(GenericsSource::Builtin),
+            ),
+            Vec::new(),
+        )
+    }
+}
+
 impl BorrowKind {
     pub fn mutable(x: bool) -> Self {
         if x {
diff --git a/charon/src/ast/gast_utils.rs b/charon/src/ast/gast_utils.rs
index ae7507e0f..ec828543b 100644
--- a/charon/src/ast/gast_utils.rs
+++ b/charon/src/ast/gast_utils.rs
@@ -63,6 +63,11 @@ impl Locals {
     pub fn return_place(&self) -> Place {
         self.place_for_var(VarId::new(0))
     }
+
+    /// Locals that aren't arguments or return values.
+    pub fn non_argument_locals(&self) -> impl Iterator<Item = (VarId, &Var)> {
+        self.vars.iter_indexed().skip(1 + self.arg_count)
+    }
 }
 
 impl std::ops::Index<VarId> for Locals {
diff --git a/charon/src/transform/insert_assign_return_unit.rs b/charon/src/transform/insert_assign_return_unit.rs
index feaa66383..efda4673c 100644
--- a/charon/src/transform/insert_assign_return_unit.rs
+++ b/charon/src/transform/insert_assign_return_unit.rs
@@ -17,18 +17,9 @@ impl UllbcPass for Transform {
                 for block in &mut body.body {
                     if let RawTerminator::Return = block.terminator.content {
                         let return_place = body.locals.return_place();
-                        let unit_value = Rvalue::Aggregate(
-                            AggregateKind::Adt(
-                                TypeId::Tuple,
-                                None,
-                                None,
-                                GenericArgs::empty(GenericsSource::Builtin),
-                            ),
-                            Vec::new(),
-                        );
                         let assign_st = Statement::new(
                             block.terminator.span,
-                            RawStatement::Assign(return_place, unit_value),
+                            RawStatement::Assign(return_place, Rvalue::unit_value()),
                         );
                         block.statements.push(assign_st)
                     }
diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs
index 17e941f57..e5271c4d3 100644
--- a/charon/src/transform/mod.rs
+++ b/charon/src/transform/mod.rs
@@ -23,6 +23,7 @@ pub mod remove_drop_never;
 pub mod remove_dynamic_checks;
 pub mod remove_nops;
 pub mod remove_read_discriminant;
+pub mod remove_unit_locals;
 pub mod remove_unused_locals;
 pub mod remove_unused_methods;
 pub mod reorder_decls;
@@ -120,9 +121,9 @@ pub static ULLBC_PASSES: &[Pass] = &[
     // of Aeneas, it means the return variable contains ⊥ upon returning.
     // For this reason, when the function has return type unit, we insert
     // an extra assignment just before returning.
-    // This also applies to globals (for checking or executing code before
-    // the main or at compile-time).
     UnstructuredBody(&insert_assign_return_unit::Transform),
+    // # Micro-pass: remove locals of type `()` which show up a lot.
+    UnstructuredBody(&remove_unit_locals::Transform),
     // # Micro-pass: remove the drops of locals whose type is `Never` (`!`). This
     // is in preparation of the next transformation.
     UnstructuredBody(&remove_drop_never::Transform),
diff --git a/charon/src/transform/remove_unit_locals.rs b/charon/src/transform/remove_unit_locals.rs
new file mode 100644
index 000000000..7b6783d79
--- /dev/null
+++ b/charon/src/transform/remove_unit_locals.rs
@@ -0,0 +1,75 @@
+use derive_generic_visitor::*;
+use std::collections::HashSet;
+
+use crate::transform::TransformCtx;
+use crate::ullbc_ast::*;
+
+use super::ctx::UllbcPass;
+
+pub struct Transform;
+impl UllbcPass for Transform {
+    fn transform_body(&self, _ctx: &mut TransformCtx, body: &mut ExprBody) {
+        // Replace any copy/move of a unit local to a plain const assignment. Note: we don't touch
+        // other `Rvalue`s as they might have side-effects (e.g. reading through a pointer).
+        body.visit_statements(|st| {
+            if let RawStatement::Assign(_, rvalue) = &mut st.content
+                && let Rvalue::Use(Operand::Move(from) | Operand::Copy(from)) = rvalue
+                && from.is_local()
+                && from.ty().is_unit()
+            {
+                *rvalue = Rvalue::unit_value()
+            }
+        });
+
+        // Find the unused locals of unit type.
+        #[derive(Visitor)]
+        struct UnitLocalsVisitor {
+            unused_unit_locals: HashSet<VarId>,
+        }
+        impl VisitBody for UnitLocalsVisitor {
+            fn enter_place(&mut self, x: &Place) {
+                if let Some(var_id) = x.as_local() {
+                    self.unused_unit_locals.remove(&var_id);
+                }
+            }
+            fn visit_ullbc_statement(
+                &mut self,
+                x: &ullbc_ast::Statement,
+            ) -> ControlFlow<Self::Break> {
+                match &x.content {
+                    RawStatement::Assign(place, rvalue) => {
+                        if place.is_local() && place.ty().is_unit() {
+                            // Don't count the assignment as a use.
+                        } else {
+                            self.visit(place)?;
+                        }
+                        self.visit(rvalue)?;
+                    }
+                    _ => self.visit_inner(x)?,
+                }
+                Continue(())
+            }
+        }
+        let unused_unit_locals = (UnitLocalsVisitor {
+            unused_unit_locals: body
+                .locals
+                .non_argument_locals()
+                .filter(|(_, var)| var.ty.is_unit())
+                .map(|(id, _)| id)
+                .collect(),
+        })
+        .visit_by_val_infallible(&*body)
+        .unused_unit_locals;
+
+        // Remove side-effect-free assignments into unused places.
+        body.visit_statements(|st| {
+            if let RawStatement::Assign(place, rvalue) = &st.content
+                && let Some(var_id) = place.as_local()
+                && unused_unit_locals.contains(&var_id)
+                && rvalue.is_aggregate()
+            {
+                st.content = RawStatement::Nop;
+            }
+        });
+    }
+}
diff --git a/charon/tests/cargo/build-script.out b/charon/tests/cargo/build-script.out
index a5c1bcad8..265ad21b1 100644
--- a/charon/tests/cargo/build-script.out
+++ b/charon/tests/cargo/build-script.out
@@ -13,10 +13,8 @@ global test_cargo_build_script::FOO: u8 = test_cargo_build_script::FOO()
 fn test_cargo_build_script::main()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/cargo/dependencies.out b/charon/tests/cargo/dependencies.out
index 06123c686..c627e551e 100644
--- a/charon/tests/cargo/dependencies.out
+++ b/charon/tests/cargo/dependencies.out
@@ -40,7 +40,6 @@ fn test_cargo_dependencies::silly_incr<'_0>(@1: &'_0 mut (u32))
     let @2: (); // anonymous local
     let @3: &'_ mut (u32); // anonymous local
     let @4: fn(u32) -> u32; // anonymous local
-    let @5: (); // anonymous local
 
     @3 := &two-phase-mut *(x@1)
     @4 := {test_cargo_dependencies::silly_incr::closure} {}
@@ -48,8 +47,7 @@ fn test_cargo_dependencies::silly_incr<'_0>(@1: &'_0 mut (u32))
     drop @4
     drop @3
     drop @2
-    @5 := ()
-    @0 := move (@5)
+    @0 := ()
     @0 := ()
     return
 }
@@ -96,8 +94,6 @@ fn test_cargo_dependencies::main()
     let @19: &'_ (u32); // anonymous local
     let @20: &'_ (u32); // anonymous local
     let @21: core::option::Option<core::fmt::Arguments<'_>>[core::marker::Sized<core::fmt::Arguments<'_>>]; // anonymous local
-    let @22: (); // anonymous local
-    let @23: (); // anonymous local
 
     x@1 := const (0 : u32)
     @fake_read(x@1)
@@ -136,16 +132,13 @@ fn test_cargo_dependencies::main()
     }
     drop @14
     drop @13
-    @22 := ()
-    @5 := move (@22)
     drop @12
     drop right_val@11
     drop left_val@10
     drop @9
     drop @6
     drop @5
-    @23 := ()
-    @0 := move (@23)
+    @0 := ()
     drop x@1
     @0 := ()
     return
diff --git a/charon/tests/cargo/toml.out b/charon/tests/cargo/toml.out
index 4714956f7..7bce209a1 100644
--- a/charon/tests/cargo/toml.out
+++ b/charon/tests/cargo/toml.out
@@ -35,7 +35,6 @@ fn test_cargo_toml::main()
     let @1: bool; // anonymous local
     let @2: &'_ (core::option::Option<bool>[core::marker::Sized<bool>]); // anonymous local
     let @3: core::option::Option<bool>[core::marker::Sized<bool>]; // anonymous local
-    let @4: (); // anonymous local
 
     @3 := core::option::Option::Some { 0: const (false) }
     @2 := &@3
@@ -44,8 +43,7 @@ fn test_cargo_toml::main()
     @fake_read(@1)
     drop @3
     drop @1
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/arrays.out b/charon/tests/ui/arrays.out
index 0c543a3d6..eee94daa9 100644
--- a/charon/tests/ui/arrays.out
+++ b/charon/tests/ui/arrays.out
@@ -9,11 +9,9 @@ fn test_crate::incr<'_0>(@1: &'_0 mut (u32))
 {
     let @0: (); // return
     let x@1: &'_ mut (u32); // arg #1
-    let @2: (); // anonymous local
 
     *(x@1) := copy (*(x@1)) + const (1 : u32)
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -578,23 +576,21 @@ fn test_crate::update_update_array(@1: Array<Array<u32, 32 : usize>, 32 : usize>
     let j@3: usize; // arg #3
     let @4: usize; // anonymous local
     let @5: usize; // anonymous local
-    let @6: (); // anonymous local
-    let @7: &'_ mut (Array<Array<u32, 32 : usize>, 32 : usize>); // anonymous local
+    let @6: &'_ mut (Array<Array<u32, 32 : usize>, 32 : usize>); // anonymous local
+    let @7: &'_ mut (Array<u32, 32 : usize>); // anonymous local
     let @8: &'_ mut (Array<u32, 32 : usize>); // anonymous local
-    let @9: &'_ mut (Array<u32, 32 : usize>); // anonymous local
-    let @10: &'_ mut (u32); // anonymous local
+    let @9: &'_ mut (u32); // anonymous local
 
     @4 := copy (i@2)
     @5 := copy (j@3)
-    @7 := &mut s@1
-    @8 := @ArrayIndexMut<'_, Array<u32, 32 : usize>, 32 : usize>(move (@7), copy (@4))
-    @9 := &mut *(@8)
-    @10 := @ArrayIndexMut<'_, u32, 32 : usize>(move (@9), copy (@5))
-    *(@10) := const (0 : u32)
+    @6 := &mut s@1
+    @7 := @ArrayIndexMut<'_, Array<u32, 32 : usize>, 32 : usize>(move (@6), copy (@4))
+    @8 := &mut *(@7)
+    @9 := @ArrayIndexMut<'_, u32, 32 : usize>(move (@8), copy (@5))
+    *(@9) := const (0 : u32)
     drop @5
     drop @4
-    @6 := ()
-    @0 := move (@6)
+    @0 := ()
     @0 := ()
     return
 }
@@ -604,23 +600,21 @@ fn test_crate::incr_array_self<'_0>(@1: &'_0 mut (Array<u32, 2 : usize>))
     let @0: (); // return
     let s@1: &'_ mut (Array<u32, 2 : usize>); // arg #1
     let @2: usize; // anonymous local
-    let @3: (); // anonymous local
-    let @4: u32; // anonymous local
-    let @5: &'_ mut (Array<u32, 2 : usize>); // anonymous local
-    let @6: &'_ mut (u32); // anonymous local
-    let @7: &'_ (Array<u32, 2 : usize>); // anonymous local
-    let @8: &'_ (u32); // anonymous local
+    let @3: u32; // anonymous local
+    let @4: &'_ mut (Array<u32, 2 : usize>); // anonymous local
+    let @5: &'_ mut (u32); // anonymous local
+    let @6: &'_ (Array<u32, 2 : usize>); // anonymous local
+    let @7: &'_ (u32); // anonymous local
 
     @2 := const (0 : usize)
-    @7 := &*(s@1)
-    @8 := @ArrayIndexShared<'_, u32, 2 : usize>(move (@7), copy (@2))
-    @4 := copy (*(@8)) + const (1 : u32)
-    @5 := &mut *(s@1)
-    @6 := @ArrayIndexMut<'_, u32, 2 : usize>(move (@5), copy (@2))
-    *(@6) := move (@4)
+    @6 := &*(s@1)
+    @7 := @ArrayIndexShared<'_, u32, 2 : usize>(move (@6), copy (@2))
+    @3 := copy (*(@7)) + const (1 : u32)
+    @4 := &mut *(s@1)
+    @5 := @ArrayIndexMut<'_, u32, 2 : usize>(move (@4), copy (@2))
+    *(@5) := move (@3)
     drop @2
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     @0 := ()
     return
 }
@@ -630,23 +624,21 @@ fn test_crate::incr_slice_self<'_0>(@1: &'_0 mut (Slice<u32>))
     let @0: (); // return
     let s@1: &'_ mut (Slice<u32>); // arg #1
     let @2: usize; // anonymous local
-    let @3: (); // anonymous local
-    let @4: u32; // anonymous local
-    let @5: &'_ mut (Slice<u32>); // anonymous local
-    let @6: &'_ mut (u32); // anonymous local
-    let @7: &'_ (Slice<u32>); // anonymous local
-    let @8: &'_ (u32); // anonymous local
+    let @3: u32; // anonymous local
+    let @4: &'_ mut (Slice<u32>); // anonymous local
+    let @5: &'_ mut (u32); // anonymous local
+    let @6: &'_ (Slice<u32>); // anonymous local
+    let @7: &'_ (u32); // anonymous local
 
     @2 := const (0 : usize)
-    @7 := &*(s@1)
-    @8 := @SliceIndexShared<'_, u32>(move (@7), copy (@2))
-    @4 := copy (*(@8)) + const (1 : u32)
-    @5 := &mut *(s@1)
-    @6 := @SliceIndexMut<'_, u32>(move (@5), copy (@2))
-    *(@6) := move (@4)
+    @6 := &*(s@1)
+    @7 := @SliceIndexShared<'_, u32>(move (@6), copy (@2))
+    @3 := copy (*(@7)) + const (1 : u32)
+    @4 := &mut *(s@1)
+    @5 := @SliceIndexMut<'_, u32>(move (@4), copy (@2))
+    *(@5) := move (@3)
     drop @2
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     @0 := ()
     return
 }
@@ -656,12 +648,10 @@ fn test_crate::array_local_deep_copy<'_0>(@1: &'_0 (Array<u32, 32 : usize>))
     let @0: (); // return
     let x@1: &'_ (Array<u32, 32 : usize>); // arg #1
     let _y@2: Array<u32, 32 : usize>; // local
-    let @3: (); // anonymous local
 
     _y@2 := copy (*(x@1))
     @fake_read(_y@2)
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     drop _y@2
     @0 := ()
     return
@@ -671,10 +661,8 @@ fn test_crate::take_array(@1: Array<u32, 2 : usize>)
 {
     let @0: (); // return
     let @1: Array<u32, 2 : usize>; // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -683,10 +671,8 @@ fn test_crate::take_array_borrow<'_0>(@1: &'_0 (Array<u32, 2 : usize>))
 {
     let @0: (); // return
     let @1: &'_ (Array<u32, 2 : usize>); // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -695,10 +681,8 @@ fn test_crate::take_slice<'_0>(@1: &'_0 (Slice<u32>))
 {
     let @0: (); // return
     let @1: &'_ (Slice<u32>); // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -707,10 +691,8 @@ fn test_crate::take_mut_slice<'_0>(@1: &'_0 mut (Slice<u32>))
 {
     let @0: (); // return
     let @1: &'_ mut (Slice<u32>); // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -730,7 +712,6 @@ fn test_crate::const_slice()
     let @2: &'_ (Array<u32, 2 : usize>); // anonymous local
     let @3: &'_ (Array<u32, 2 : usize>); // anonymous local
     let @4: Array<u32, 2 : usize>; // anonymous local
-    let @5: (); // anonymous local
 
     @4 := [const (0 : u32), const (0 : u32); 2 : usize]
     @3 := &@4
@@ -740,8 +721,7 @@ fn test_crate::const_slice()
     @fake_read(@1)
     drop @3
     drop @1
-    @5 := ()
-    @0 := move (@5)
+    @0 := ()
     drop @4
     @0 := ()
     return
@@ -766,7 +746,6 @@ fn test_crate::take_all()
     let @14: &'_ mut (Slice<u32>); // anonymous local
     let @15: &'_ mut (Array<u32, 2 : usize>); // anonymous local
     let @16: &'_ mut (Array<u32, 2 : usize>); // anonymous local
-    let @17: (); // anonymous local
 
     x@1 := [const (0 : u32), const (0 : u32); 2 : usize]
     @fake_read(x@1)
@@ -805,8 +784,7 @@ fn test_crate::take_all()
     drop @14
     drop @16
     drop @13
-    @17 := ()
-    @0 := move (@17)
+    @0 := ()
     drop x@1
     @0 := ()
     return
@@ -902,8 +880,6 @@ fn test_crate::index_all() -> u32
     let @21: &'_ mut (Slice<u32>); // anonymous local
     let @22: &'_ mut (Array<u32, 2 : usize>); // anonymous local
     let @23: &'_ mut (Array<u32, 2 : usize>); // anonymous local
-    let @24: (); // anonymous local
-    let @25: (); // anonymous local
 
     x@1 := [const (0 : u32), const (0 : u32); 2 : usize]
     @fake_read(x@1)
@@ -911,15 +887,11 @@ fn test_crate::index_all() -> u32
     if move (@3) {
         _y@4 := [const (0 : u32), const (0 : u32); 2 : usize]
         @fake_read(_y@4)
-        @24 := ()
-        @2 := move (@24)
         drop _y@4
     }
     else {
         _z@5 := [const (0 : u32); 1 : usize]
         @fake_read(_z@5)
-        @25 := ()
-        @2 := move (@25)
         drop _z@5
     }
     drop @3
@@ -970,16 +942,14 @@ fn test_crate::update_array(@1: Array<u32, 2 : usize>)
     let @0: (); // return
     let x@1: Array<u32, 2 : usize>; // arg #1
     let @2: usize; // anonymous local
-    let @3: (); // anonymous local
-    let @4: &'_ mut (Array<u32, 2 : usize>); // anonymous local
-    let @5: &'_ mut (u32); // anonymous local
+    let @3: &'_ mut (Array<u32, 2 : usize>); // anonymous local
+    let @4: &'_ mut (u32); // anonymous local
 
     @2 := const (0 : usize)
-    @4 := &mut x@1
-    @5 := @ArrayIndexMut<'_, u32, 2 : usize>(move (@4), copy (@2))
-    *(@5) := const (1 : u32)
-    @3 := ()
-    @0 := move (@3)
+    @3 := &mut x@1
+    @4 := @ArrayIndexMut<'_, u32, 2 : usize>(move (@3), copy (@2))
+    *(@4) := const (1 : u32)
+    @0 := ()
     drop @2
     @0 := ()
     return
@@ -990,16 +960,14 @@ fn test_crate::update_array_mut_borrow<'_0>(@1: &'_0 mut (Array<u32, 2 : usize>)
     let @0: (); // return
     let x@1: &'_ mut (Array<u32, 2 : usize>); // arg #1
     let @2: usize; // anonymous local
-    let @3: (); // anonymous local
-    let @4: &'_ mut (Array<u32, 2 : usize>); // anonymous local
-    let @5: &'_ mut (u32); // anonymous local
+    let @3: &'_ mut (Array<u32, 2 : usize>); // anonymous local
+    let @4: &'_ mut (u32); // anonymous local
 
     @2 := const (0 : usize)
-    @4 := &mut *(x@1)
-    @5 := @ArrayIndexMut<'_, u32, 2 : usize>(move (@4), copy (@2))
-    *(@5) := const (1 : u32)
-    @3 := ()
-    @0 := move (@3)
+    @3 := &mut *(x@1)
+    @4 := @ArrayIndexMut<'_, u32, 2 : usize>(move (@3), copy (@2))
+    *(@4) := const (1 : u32)
+    @0 := ()
     drop @2
     @0 := ()
     return
@@ -1010,16 +978,14 @@ fn test_crate::update_mut_slice<'_0>(@1: &'_0 mut (Slice<u32>))
     let @0: (); // return
     let x@1: &'_ mut (Slice<u32>); // arg #1
     let @2: usize; // anonymous local
-    let @3: (); // anonymous local
-    let @4: &'_ mut (Slice<u32>); // anonymous local
-    let @5: &'_ mut (u32); // anonymous local
+    let @3: &'_ mut (Slice<u32>); // anonymous local
+    let @4: &'_ mut (u32); // anonymous local
 
     @2 := const (0 : usize)
-    @4 := &mut *(x@1)
-    @5 := @SliceIndexMut<'_, u32>(move (@4), copy (@2))
-    *(@5) := const (1 : u32)
-    @3 := ()
-    @0 := move (@3)
+    @3 := &mut *(x@1)
+    @4 := @SliceIndexMut<'_, u32>(move (@3), copy (@2))
+    *(@4) := const (1 : u32)
+    @0 := ()
     drop @2
     @0 := ()
     return
@@ -1040,7 +1006,6 @@ fn test_crate::update_all()
     let @10: &'_ mut (Slice<u32>); // anonymous local
     let @11: &'_ mut (Array<u32, 2 : usize>); // anonymous local
     let @12: &'_ mut (Array<u32, 2 : usize>); // anonymous local
-    let @13: (); // anonymous local
 
     x@1 := [const (0 : u32), const (0 : u32); 2 : usize]
     @fake_read(x@1)
@@ -1066,8 +1031,7 @@ fn test_crate::update_all()
     drop @10
     drop @12
     drop @9
-    @13 := ()
-    @0 := move (@13)
+    @0 := ()
     drop x@1
     @0 := ()
     return
@@ -1083,7 +1047,6 @@ fn test_crate::range_all()
     let @5: &'_ mut (Slice<u32>); // anonymous local
     let @6: &'_ mut (Array<u32, 4 : usize>); // anonymous local
     let @7: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // anonymous local
-    let @8: (); // anonymous local
 
     x@1 := [const (0 : u32), const (0 : u32), const (0 : u32), const (0 : u32); 4 : usize]
     @fake_read(x@1)
@@ -1100,8 +1063,7 @@ fn test_crate::range_all()
     drop @5
     drop @4
     drop @2
-    @8 := ()
-    @0 := move (@8)
+    @0 := ()
     drop x@1
     @0 := ()
     return
@@ -1151,10 +1113,8 @@ fn test_crate::take_array_t(@1: Array<test_crate::AB, 2 : usize>)
 {
     let @0: (); // return
     let @1: Array<test_crate::AB, 2 : usize>; // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -1167,7 +1127,6 @@ fn test_crate::non_copyable_array()
     let @3: test_crate::AB; // anonymous local
     let @4: (); // anonymous local
     let @5: Array<test_crate::AB, 2 : usize>; // anonymous local
-    let @6: (); // anonymous local
 
     @2 := test_crate::AB::A {  }
     @3 := test_crate::AB::B {  }
@@ -1181,8 +1140,7 @@ fn test_crate::non_copyable_array()
     @4 := test_crate::take_array_t(move (@5))
     drop @5
     drop @4
-    @6 := ()
-    @0 := move (@6)
+    @0 := ()
     // this fails, naturally:
     // take_array_t(x);
     drop x@1
@@ -1197,55 +1155,48 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
     let sum@2: u32; // local
     let i@3: usize; // local
     let @4: (); // anonymous local
-    let @5: (); // anonymous local
-    let @6: bool; // anonymous local
+    let @5: bool; // anonymous local
+    let @6: usize; // anonymous local
     let @7: usize; // anonymous local
-    let @8: usize; // anonymous local
-    let @9: &'_ (Slice<u32>); // anonymous local
-    let @10: u32; // anonymous local
-    let @11: usize; // anonymous local
-    let @12: (); // anonymous local
-    let @13: (); // anonymous local
-    let @14: (); // anonymous local
-    let @15: &'_ (Slice<u32>); // anonymous local
-    let @16: &'_ (u32); // anonymous local
+    let @8: &'_ (Slice<u32>); // anonymous local
+    let @9: u32; // anonymous local
+    let @10: usize; // anonymous local
+    let @11: (); // anonymous local
+    let @12: &'_ (Slice<u32>); // anonymous local
+    let @13: &'_ (u32); // anonymous local
 
     sum@2 := const (0 : u32)
     @fake_read(sum@2)
     i@3 := const (0 : usize)
     @fake_read(i@3)
     loop {
-        @7 := copy (i@3)
-        @9 := &*(s@1)
-        @8 := core::slice::{Slice<T>}::len<'_, u32>[core::marker::Sized<u32>](move (@9))
-        drop @9
-        @6 := move (@7) < move (@8)
-        if move (@6) {
-            drop @8
+        @6 := copy (i@3)
+        @8 := &*(s@1)
+        @7 := core::slice::{Slice<T>}::len<'_, u32>[core::marker::Sized<u32>](move (@8))
+        drop @8
+        @5 := move (@6) < move (@7)
+        if move (@5) {
             drop @7
-            @11 := copy (i@3)
-            @15 := &*(s@1)
-            @16 := @SliceIndexShared<'_, u32>(move (@15), copy (@11))
-            @10 := copy (*(@16))
-            sum@2 := copy (sum@2) + move (@10)
+            drop @6
+            @10 := copy (i@3)
+            @12 := &*(s@1)
+            @13 := @SliceIndexShared<'_, u32>(move (@12), copy (@10))
+            @9 := copy (*(@13))
+            sum@2 := copy (sum@2) + move (@9)
+            drop @9
             drop @10
-            drop @11
             i@3 := copy (i@3) + const (1 : usize)
-            @13 := ()
-            @5 := move (@13)
-            drop @6
+            drop @5
             continue 0
         }
         else {
             break 0
         }
     }
-    drop @8
     drop @7
-    @14 := ()
-    @4 := move (@14)
-    drop @12
     drop @6
+    drop @11
+    drop @5
     drop @4
     @0 := copy (sum@2)
     drop i@3
@@ -1267,24 +1218,20 @@ fn test_crate::sum2<'_0, '_1>(@1: &'_0 (Slice<u32>), @2: &'_1 (Slice<u32>)) -> u
     let @9: &'_ (Slice<u32>); // anonymous local
     let i@10: usize; // local
     let @11: (); // anonymous local
-    let @12: (); // anonymous local
-    let @13: bool; // anonymous local
+    let @12: bool; // anonymous local
+    let @13: usize; // anonymous local
     let @14: usize; // anonymous local
-    let @15: usize; // anonymous local
-    let @16: &'_ (Slice<u32>); // anonymous local
+    let @15: &'_ (Slice<u32>); // anonymous local
+    let @16: u32; // anonymous local
     let @17: u32; // anonymous local
-    let @18: u32; // anonymous local
-    let @19: usize; // anonymous local
-    let @20: u32; // anonymous local
-    let @21: usize; // anonymous local
-    let @22: (); // anonymous local
-    let @23: (); // anonymous local
-    let @24: (); // anonymous local
-    let @25: (); // anonymous local
-    let @26: &'_ (Slice<u32>); // anonymous local
-    let @27: &'_ (u32); // anonymous local
-    let @28: &'_ (Slice<u32>); // anonymous local
-    let @29: &'_ (u32); // anonymous local
+    let @18: usize; // anonymous local
+    let @19: u32; // anonymous local
+    let @20: usize; // anonymous local
+    let @21: (); // anonymous local
+    let @22: &'_ (Slice<u32>); // anonymous local
+    let @23: &'_ (u32); // anonymous local
+    let @24: &'_ (Slice<u32>); // anonymous local
+    let @25: &'_ (u32); // anonymous local
 
     sum@3 := const (0 : u32)
     @fake_read(sum@3)
@@ -1304,52 +1251,46 @@ fn test_crate::sum2<'_0, '_1>(@1: &'_0 (Slice<u32>), @2: &'_1 (Slice<u32>)) -> u
     }
     drop @8
     drop @6
-    @23 := ()
-    @4 := move (@23)
     drop @5
     drop @4
     i@10 := const (0 : usize)
     @fake_read(i@10)
     loop {
-        @14 := copy (i@10)
-        @16 := &*(s@1)
-        @15 := core::slice::{Slice<T>}::len<'_, u32>[core::marker::Sized<u32>](move (@16))
-        drop @16
-        @13 := move (@14) < move (@15)
-        if move (@13) {
-            drop @15
+        @13 := copy (i@10)
+        @15 := &*(s@1)
+        @14 := core::slice::{Slice<T>}::len<'_, u32>[core::marker::Sized<u32>](move (@15))
+        drop @15
+        @12 := move (@13) < move (@14)
+        if move (@12) {
             drop @14
-            @19 := copy (i@10)
-            @28 := &*(s@1)
-            @29 := @SliceIndexShared<'_, u32>(move (@28), copy (@19))
-            @18 := copy (*(@29))
-            @21 := copy (i@10)
-            @26 := &*(s2@2)
-            @27 := @SliceIndexShared<'_, u32>(move (@26), copy (@21))
-            @20 := copy (*(@27))
-            @17 := move (@18) + move (@20)
+            drop @13
+            @18 := copy (i@10)
+            @24 := &*(s@1)
+            @25 := @SliceIndexShared<'_, u32>(move (@24), copy (@18))
+            @17 := copy (*(@25))
+            @20 := copy (i@10)
+            @22 := &*(s2@2)
+            @23 := @SliceIndexShared<'_, u32>(move (@22), copy (@20))
+            @19 := copy (*(@23))
+            @16 := move (@17) + move (@19)
+            drop @19
+            drop @17
+            sum@3 := copy (sum@3) + move (@16)
+            drop @16
             drop @20
             drop @18
-            sum@3 := copy (sum@3) + move (@17)
-            drop @17
-            drop @21
-            drop @19
             i@10 := copy (i@10) + const (1 : usize)
-            @24 := ()
-            @12 := move (@24)
-            drop @13
+            drop @12
             continue 0
         }
         else {
             break 0
         }
     }
-    drop @15
     drop @14
-    @25 := ()
-    @11 := move (@25)
-    drop @22
     drop @13
+    drop @21
+    drop @12
     drop @11
     @0 := copy (sum@3)
     drop i@10
@@ -1365,9 +1306,8 @@ fn test_crate::f0()
     let @3: &'_ mut (Array<u32, 2 : usize>); // anonymous local
     let @4: Array<u32, 2 : usize>; // anonymous local
     let @5: usize; // anonymous local
-    let @6: (); // anonymous local
-    let @7: &'_ mut (Slice<u32>); // anonymous local
-    let @8: &'_ mut (u32); // anonymous local
+    let @6: &'_ mut (Slice<u32>); // anonymous local
+    let @7: &'_ mut (u32); // anonymous local
 
     @4 := [const (1 : u32), const (2 : u32); 2 : usize]
     @3 := &mut @4
@@ -1377,12 +1317,11 @@ fn test_crate::f0()
     @fake_read(s@1)
     drop @3
     @5 := const (0 : usize)
-    @7 := &mut *(s@1)
-    @8 := @SliceIndexMut<'_, u32>(move (@7), copy (@5))
-    *(@8) := const (1 : u32)
+    @6 := &mut *(s@1)
+    @7 := @SliceIndexMut<'_, u32>(move (@6), copy (@5))
+    *(@7) := const (1 : u32)
     drop @5
-    @6 := ()
-    @0 := move (@6)
+    @0 := ()
     drop @4
     drop s@1
     @0 := ()
@@ -1394,19 +1333,17 @@ fn test_crate::f1()
     let @0: (); // return
     let s@1: Array<u32, 2 : usize>; // local
     let @2: usize; // anonymous local
-    let @3: (); // anonymous local
-    let @4: &'_ mut (Array<u32, 2 : usize>); // anonymous local
-    let @5: &'_ mut (u32); // anonymous local
+    let @3: &'_ mut (Array<u32, 2 : usize>); // anonymous local
+    let @4: &'_ mut (u32); // anonymous local
 
     s@1 := [const (1 : u32), const (2 : u32); 2 : usize]
     @fake_read(s@1)
     @2 := const (0 : usize)
-    @4 := &mut s@1
-    @5 := @ArrayIndexMut<'_, u32, 2 : usize>(move (@4), copy (@2))
-    *(@5) := const (1 : u32)
+    @3 := &mut s@1
+    @4 := @ArrayIndexMut<'_, u32, 2 : usize>(move (@3), copy (@2))
+    *(@4) := const (1 : u32)
     drop @2
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     drop s@1
     @0 := ()
     return
@@ -1416,10 +1353,8 @@ fn test_crate::f2(@1: u32)
 {
     let @0: (); // return
     let @1: u32; // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -1543,8 +1478,6 @@ fn test_crate::ite()
     let @9: &'_ mut (Slice<u32>); // anonymous local
     let @10: &'_ mut (Array<u32, 2 : usize>); // anonymous local
     let @11: &'_ mut (Array<u32, 2 : usize>); // anonymous local
-    let @12: (); // anonymous local
-    let @13: (); // anonymous local
 
     x@1 := [const (0 : u32), const (0 : u32); 2 : usize]
     @fake_read(x@1)
@@ -1568,13 +1501,11 @@ fn test_crate::ite()
         drop @9
         drop @11
         drop @8
-        @12 := ()
-        @0 := move (@12)
+        @0 := ()
         drop y@3
     }
     else {
-        @13 := ()
-        @0 := move (@13)
+        @0 := ()
     }
     drop @2
     drop x@1
@@ -1589,16 +1520,13 @@ fn test_crate::zero_slice<'_0>(@1: &'_0 mut (Slice<u8>))
     let i@2: usize; // local
     let len@3: usize; // local
     let @4: &'_ (Slice<u8>); // anonymous local
-    let @5: (); // anonymous local
-    let @6: bool; // anonymous local
+    let @5: bool; // anonymous local
+    let @6: usize; // anonymous local
     let @7: usize; // anonymous local
     let @8: usize; // anonymous local
-    let @9: usize; // anonymous local
-    let @10: (); // anonymous local
-    let @11: (); // anonymous local
-    let @12: (); // anonymous local
-    let @13: &'_ mut (Slice<u8>); // anonymous local
-    let @14: &'_ mut (u8); // anonymous local
+    let @9: (); // anonymous local
+    let @10: &'_ mut (Slice<u8>); // anonymous local
+    let @11: &'_ mut (u8); // anonymous local
 
     i@2 := const (0 : usize)
     @fake_read(i@2)
@@ -1607,33 +1535,30 @@ fn test_crate::zero_slice<'_0>(@1: &'_0 mut (Slice<u8>))
     drop @4
     @fake_read(len@3)
     loop {
-        @7 := copy (i@2)
-        @8 := copy (len@3)
-        @6 := move (@7) < move (@8)
-        if move (@6) {
-            drop @8
+        @6 := copy (i@2)
+        @7 := copy (len@3)
+        @5 := move (@6) < move (@7)
+        if move (@5) {
             drop @7
-            @9 := copy (i@2)
-            @13 := &mut *(a@1)
-            @14 := @SliceIndexMut<'_, u8>(move (@13), copy (@9))
-            *(@14) := const (0 : u8)
-            drop @9
-            i@2 := copy (i@2) + const (1 : usize)
-            @11 := ()
-            @5 := move (@11)
             drop @6
+            @8 := copy (i@2)
+            @10 := &mut *(a@1)
+            @11 := @SliceIndexMut<'_, u8>(move (@10), copy (@8))
+            *(@11) := const (0 : u8)
+            drop @8
+            i@2 := copy (i@2) + const (1 : usize)
+            drop @5
             continue 0
         }
         else {
             break 0
         }
     }
-    drop @8
     drop @7
-    @12 := ()
-    @0 := move (@12)
-    drop @10
     drop @6
+    @0 := ()
+    drop @9
+    drop @5
     drop len@3
     drop i@2
     @0 := ()
@@ -1647,13 +1572,10 @@ fn test_crate::iter_mut_slice<'_0>(@1: &'_0 mut (Slice<u8>))
     let len@2: usize; // local
     let @3: &'_ (Slice<u8>); // anonymous local
     let i@4: usize; // local
-    let @5: (); // anonymous local
-    let @6: bool; // anonymous local
+    let @5: bool; // anonymous local
+    let @6: usize; // anonymous local
     let @7: usize; // anonymous local
-    let @8: usize; // anonymous local
-    let @9: (); // anonymous local
-    let @10: (); // anonymous local
-    let @11: (); // anonymous local
+    let @8: (); // anonymous local
 
     @3 := &*(a@1)
     len@2 := core::slice::{Slice<T>}::len<'_, u8>[core::marker::Sized<u8>](move (@3))
@@ -1662,28 +1584,25 @@ fn test_crate::iter_mut_slice<'_0>(@1: &'_0 mut (Slice<u8>))
     i@4 := const (0 : usize)
     @fake_read(i@4)
     loop {
-        @7 := copy (i@4)
-        @8 := copy (len@2)
-        @6 := move (@7) < move (@8)
-        if move (@6) {
-            drop @8
+        @6 := copy (i@4)
+        @7 := copy (len@2)
+        @5 := move (@6) < move (@7)
+        if move (@5) {
             drop @7
-            i@4 := copy (i@4) + const (1 : usize)
-            @10 := ()
-            @5 := move (@10)
             drop @6
+            i@4 := copy (i@4) + const (1 : usize)
+            drop @5
             continue 0
         }
         else {
             break 0
         }
     }
-    drop @8
     drop @7
-    @11 := ()
-    @0 := move (@11)
-    drop @9
     drop @6
+    @0 := ()
+    drop @8
+    drop @5
     drop i@4
     drop len@2
     @0 := ()
@@ -1697,55 +1616,48 @@ fn test_crate::sum_mut_slice<'_0>(@1: &'_0 mut (Slice<u32>)) -> u32
     let i@2: usize; // local
     let s@3: u32; // local
     let @4: (); // anonymous local
-    let @5: (); // anonymous local
-    let @6: bool; // anonymous local
+    let @5: bool; // anonymous local
+    let @6: usize; // anonymous local
     let @7: usize; // anonymous local
-    let @8: usize; // anonymous local
-    let @9: &'_ (Slice<u32>); // anonymous local
-    let @10: u32; // anonymous local
-    let @11: usize; // anonymous local
-    let @12: (); // anonymous local
-    let @13: (); // anonymous local
-    let @14: (); // anonymous local
-    let @15: &'_ (Slice<u32>); // anonymous local
-    let @16: &'_ (u32); // anonymous local
+    let @8: &'_ (Slice<u32>); // anonymous local
+    let @9: u32; // anonymous local
+    let @10: usize; // anonymous local
+    let @11: (); // anonymous local
+    let @12: &'_ (Slice<u32>); // anonymous local
+    let @13: &'_ (u32); // anonymous local
 
     i@2 := const (0 : usize)
     @fake_read(i@2)
     s@3 := const (0 : u32)
     @fake_read(s@3)
     loop {
-        @7 := copy (i@2)
-        @9 := &*(a@1)
-        @8 := core::slice::{Slice<T>}::len<'_, u32>[core::marker::Sized<u32>](move (@9))
-        drop @9
-        @6 := move (@7) < move (@8)
-        if move (@6) {
-            drop @8
+        @6 := copy (i@2)
+        @8 := &*(a@1)
+        @7 := core::slice::{Slice<T>}::len<'_, u32>[core::marker::Sized<u32>](move (@8))
+        drop @8
+        @5 := move (@6) < move (@7)
+        if move (@5) {
             drop @7
-            @11 := copy (i@2)
-            @15 := &*(a@1)
-            @16 := @SliceIndexShared<'_, u32>(move (@15), copy (@11))
-            @10 := copy (*(@16))
-            s@3 := copy (s@3) + move (@10)
+            drop @6
+            @10 := copy (i@2)
+            @12 := &*(a@1)
+            @13 := @SliceIndexShared<'_, u32>(move (@12), copy (@10))
+            @9 := copy (*(@13))
+            s@3 := copy (s@3) + move (@9)
+            drop @9
             drop @10
-            drop @11
             i@2 := copy (i@2) + const (1 : usize)
-            @13 := ()
-            @5 := move (@13)
-            drop @6
+            drop @5
             continue 0
         }
         else {
             break 0
         }
     }
-    drop @8
     drop @7
-    @14 := ()
-    @4 := move (@14)
-    drop @12
     drop @6
+    drop @11
+    drop @5
     drop @4
     @0 := copy (s@3)
     drop s@3
@@ -1758,16 +1670,14 @@ fn test_crate::slice_pattern_1(@1: Array<(), 1 : usize>)
     let @0: (); // return
     let x@1: Array<(), 1 : usize>; // arg #1
     let _named@2: (); // local
-    let @3: (); // anonymous local
-    let @4: &'_ (Array<(), 1 : usize>); // anonymous local
-    let @5: &'_ (()); // anonymous local
+    let @3: &'_ (Array<(), 1 : usize>); // anonymous local
+    let @4: &'_ (()); // anonymous local
 
     @fake_read(x@1)
-    @4 := &x@1
-    @5 := @ArrayIndexShared<'_, (), 1 : usize>(move (@4), const (0 : usize))
-    _named@2 := copy (*(@5))
-    @3 := ()
-    @0 := move (@3)
+    @3 := &x@1
+    @4 := @ArrayIndexShared<'_, (), 1 : usize>(move (@3), const (0 : usize))
+    _named@2 := copy (*(@4))
+    @0 := ()
     drop _named@2
     @0 := ()
     return
@@ -1782,26 +1692,24 @@ where
     let _a@2: &'_ mut (T); // local
     let _b@3: &'_ mut (T); // local
     let _c@4: &'_ mut (T); // local
-    let @5: (); // anonymous local
-    let @6: &'_ mut (Array<&'_ mut (T), 3 : usize>); // anonymous local
-    let @7: &'_ mut (&'_ mut (T)); // anonymous local
-    let @8: &'_ mut (Array<&'_ mut (T), 3 : usize>); // anonymous local
-    let @9: &'_ mut (&'_ mut (T)); // anonymous local
-    let @10: &'_ mut (Array<&'_ mut (T), 3 : usize>); // anonymous local
-    let @11: &'_ mut (&'_ mut (T)); // anonymous local
+    let @5: &'_ mut (Array<&'_ mut (T), 3 : usize>); // anonymous local
+    let @6: &'_ mut (&'_ mut (T)); // anonymous local
+    let @7: &'_ mut (Array<&'_ mut (T), 3 : usize>); // anonymous local
+    let @8: &'_ mut (&'_ mut (T)); // anonymous local
+    let @9: &'_ mut (Array<&'_ mut (T), 3 : usize>); // anonymous local
+    let @10: &'_ mut (&'_ mut (T)); // anonymous local
 
     @fake_read(x@1)
-    @10 := &mut x@1
-    @11 := @ArrayIndexMut<'_, &'_ mut (T), 3 : usize>(move (@10), const (0 : usize))
-    _a@2 := move (*(@11))
-    @8 := &mut x@1
-    @9 := @ArrayIndexMut<'_, &'_ mut (T), 3 : usize>(move (@8), const (1 : usize))
-    _b@3 := move (*(@9))
-    @6 := &mut x@1
-    @7 := @ArrayIndexMut<'_, &'_ mut (T), 3 : usize>(move (@6), const (2 : usize))
-    _c@4 := move (*(@7))
-    @5 := ()
-    @0 := move (@5)
+    @9 := &mut x@1
+    @10 := @ArrayIndexMut<'_, &'_ mut (T), 3 : usize>(move (@9), const (0 : usize))
+    _a@2 := move (*(@10))
+    @7 := &mut x@1
+    @8 := @ArrayIndexMut<'_, &'_ mut (T), 3 : usize>(move (@7), const (1 : usize))
+    _b@3 := move (*(@8))
+    @5 := &mut x@1
+    @6 := @ArrayIndexMut<'_, &'_ mut (T), 3 : usize>(move (@5), const (2 : usize))
+    _c@4 := move (*(@6))
+    @0 := ()
     drop _c@4
     drop _b@3
     drop _a@2
@@ -1814,16 +1722,14 @@ fn test_crate::slice_pattern_3<'_0>(@1: &'_0 (Array<(), 1 : usize>))
     let @0: (); // return
     let x@1: &'_ (Array<(), 1 : usize>); // arg #1
     let _named@2: &'_ (()); // local
-    let @3: (); // anonymous local
-    let @4: &'_ (Array<(), 1 : usize>); // anonymous local
-    let @5: &'_ (()); // anonymous local
+    let @3: &'_ (Array<(), 1 : usize>); // anonymous local
+    let @4: &'_ (()); // anonymous local
 
     @fake_read(x@1)
-    @4 := &*(x@1)
-    @5 := @ArrayIndexShared<'_, (), 1 : usize>(move (@4), const (0 : usize))
-    _named@2 := &*(@5)
-    @3 := ()
-    @0 := move (@3)
+    @3 := &*(x@1)
+    @4 := @ArrayIndexShared<'_, (), 1 : usize>(move (@3), const (0 : usize))
+    _named@2 := &*(@4)
+    @0 := ()
     drop _named@2
     @0 := ()
     return
diff --git a/charon/tests/ui/associated-types.out b/charon/tests/ui/associated-types.out
index 8359ac27f..9999ecb51 100644
--- a/charon/tests/ui/associated-types.out
+++ b/charon/tests/ui/associated-types.out
@@ -181,15 +181,13 @@ fn test_crate::call_fn()
     let @0: (); // return
     let @1: core::option::Option<&'_ (bool)>[core::marker::Sized<&'_ (bool)>]; // anonymous local
     let @2: core::option::Option<&'_ (bool)>[core::marker::Sized<&'_ (bool)>]; // anonymous local
-    let @3: (); // anonymous local
 
     @2 := core::option::Option::None {  }
     @1 := test_crate::external_use_item<'_, &'_ (bool), core::option::Option<&'_ (bool)>[core::marker::Sized<&'_ (bool)>], &'_ (bool)>[core::marker::Sized<&'_ (bool)>, test_crate::{impl test_crate::Foo<'a, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]> for &'a (T)}<'_, bool>[core::marker::Sized<bool>], test_crate::{impl test_crate::Foo<'a, T> for core::option::Option<T>[@TraitClause0]}#1<'_, &'_ (bool)>[core::marker::Sized<&'_ (bool)>, core::marker::{impl core::marker::Copy for &'_0 (T)}#4<'_, bool>]](move (@2))
     drop @2
     @fake_read(@1)
     drop @1
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/call-to-known-trait-method.out b/charon/tests/ui/call-to-known-trait-method.out
index 4c8dc0828..d2d1cbe80 100644
--- a/charon/tests/ui/call-to-known-trait-method.out
+++ b/charon/tests/ui/call-to-known-trait-method.out
@@ -69,10 +69,8 @@ where
     [@TraitClause4]: core::marker::Sized<C>,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -120,7 +118,6 @@ fn test_crate::main()
     let _x@1: (u8, bool); // local
     let _y@2: test_crate::Struct<bool>[core::marker::Sized<bool>]; // local
     let @3: (); // anonymous local
-    let @4: (); // anonymous local
 
     _x@1 := (const (0 : u8), const (false))
     @fake_read(_x@1)
@@ -128,8 +125,7 @@ fn test_crate::main()
     @fake_read(_y@2)
     @3 := test_crate::{impl test_crate::Trait<B, (A, B)> for test_crate::Struct<A>[@TraitClause0]}::method<u8, bool, alloc::string::String>[core::marker::Sized<u8>, core::marker::Sized<bool>, core::clone::impls::{impl core::clone::Clone for u8}#6, core::cmp::impls::{impl core::cmp::PartialEq<bool> for bool}#19, core::marker::Sized<alloc::string::String>]()
     drop @3
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     drop _y@2
     drop _x@1
     @0 := ()
diff --git a/charon/tests/ui/comments.out b/charon/tests/ui/comments.out
index 3800e05df..46bfafdd6 100644
--- a/charon/tests/ui/comments.out
+++ b/charon/tests/ui/comments.out
@@ -4,10 +4,8 @@ fn test_crate::function_call(@1: u32)
 {
     let @0: (); // return
     let @1: u32; // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -28,25 +26,22 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
     let @5: u32; // anonymous local
     let @6: u32; // anonymous local
     let @7: (); // anonymous local
-    let @8: (); // anonymous local
-    let @9: bool; // anonymous local
+    let @8: bool; // anonymous local
+    let @9: usize; // anonymous local
     let @10: usize; // anonymous local
-    let @11: usize; // anonymous local
-    let @12: &'_ (Slice<u32>); // anonymous local
-    let @13: u32; // anonymous local
-    let @14: usize; // anonymous local
-    let @15: (); // anonymous local
-    let @16: u32; // anonymous local
-    let @17: bool; // anonymous local
+    let @11: &'_ (Slice<u32>); // anonymous local
+    let @12: u32; // anonymous local
+    let @13: usize; // anonymous local
+    let @14: (); // anonymous local
+    let @15: u32; // anonymous local
+    let @16: bool; // anonymous local
+    let @17: u32; // anonymous local
     let @18: u32; // anonymous local
-    let @19: u32; // anonymous local
-    let @20: (); // anonymous local
+    let @19: (); // anonymous local
+    let @20: u32; // anonymous local
     let @21: u32; // anonymous local
-    let @22: u32; // anonymous local
-    let @23: (); // anonymous local
-    let @24: (); // anonymous local
-    let @25: &'_ (Slice<u32>); // anonymous local
-    let @26: &'_ (u32); // anonymous local
+    let @22: &'_ (Slice<u32>); // anonymous local
+    let @23: &'_ (u32); // anonymous local
 
     // `let sum`
     sum@2 := const (0 : u32)
@@ -65,66 +60,62 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
     drop @4
     // Start of loop
     loop {
-        @10 := copy (i@3)
-        @12 := &*(s@1)
-        @11 := core::slice::{Slice<T>}::len<'_, u32>[core::marker::Sized<u32>](move (@12))
-        drop @12
-        @9 := move (@10) < move (@11)
-        if move (@9) {
-            drop @11
+        @9 := copy (i@3)
+        @11 := &*(s@1)
+        @10 := core::slice::{Slice<T>}::len<'_, u32>[core::marker::Sized<u32>](move (@11))
+        drop @11
+        @8 := move (@9) < move (@10)
+        if move (@8) {
             drop @10
+            drop @9
             // Add to running sum
-            @14 := copy (i@3)
-            @25 := &*(s@1)
-            @26 := @SliceIndexShared<'_, u32>(move (@25), copy (@14))
-            @13 := copy (*(@26))
-            sum@2 := copy (sum@2) + move (@13)
+            @13 := copy (i@3)
+            @22 := &*(s@1)
+            @23 := @SliceIndexShared<'_, u32>(move (@22), copy (@13))
+            @12 := copy (*(@23))
+            sum@2 := copy (sum@2) + move (@12)
+            drop @12
             drop @13
-            drop @14
             // Increment `i`
             i@3 := copy (i@3) + const (1 : usize)
-            @23 := ()
-            @8 := move (@23)
             // Before end of loop
-            drop @9
+            drop @8
             continue 0
         }
         else {
             break 0
         }
     }
-    drop @11
     drop @10
-    @24 := ()
-    @7 := move (@24)
-    drop @15
     drop @9
+    drop @14
+    drop @8
     drop @7
     // Assign the result of an `if`.
-    @18 := copy (sum@2)
-    @17 := move (@18) > const (10 : u32)
-    if move (@17) {
-        drop @18
+    @17 := copy (sum@2)
+    @16 := move (@17) > const (10 : u32)
+    if move (@16) {
+        drop @17
         // sum + 100
-        @19 := copy (sum@2)
-        @16 := move (@19) + const (100 : u32)
-        drop @19
+        @18 := copy (sum@2)
+        @15 := move (@18) + const (100 : u32)
+        drop @18
     }
     else {
-        drop @18
+        drop @17
         // let sum untouched
-        @16 := copy (sum@2)
+        @15 := copy (sum@2)
     }
-    drop @17
-    sum@2 := move (@16)
     drop @16
+    sum@2 := move (@15)
+    drop @15
     // Function call
-    @22 := copy (sum@2)
-    @21 := move (@22) + const (2 : u32)
-    drop @22
-    @20 := test_crate::function_call(move (@21))
+    @21 := copy (sum@2)
+    @20 := move (@21) + const (2 : u32)
     drop @21
+    @19 := test_crate::function_call(move (@20))
     drop @20
+    drop @19
     // Return final value
     @0 := copy (sum@2)
     drop i@3
@@ -198,10 +189,8 @@ where
 {
     let @0: (); // return
     let @1: T; // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     drop @1
     @0 := ()
     return
@@ -261,10 +250,8 @@ fn test_crate::foo()
     let @31: &'_ (u32); // anonymous local
     let @32: &'_ (u32); // anonymous local
     let @33: core::option::Option<core::fmt::Arguments<'_>>[core::marker::Sized<core::fmt::Arguments<'_>>]; // anonymous local
-    let @34: (); // anonymous local
-    let @35: (); // anonymous local
-    let @36: &'_ (Array<u32, 10 : usize>); // anonymous local
-    let @37: &'_ (u32); // anonymous local
+    let @34: &'_ (Array<u32, 10 : usize>); // anonymous local
+    let @35: &'_ (u32); // anonymous local
 
     // Call `default` and destructure the result
     @3 := test_crate::{impl core::default::Default for test_crate::Foo}::default()
@@ -303,9 +290,9 @@ fn test_crate::foo()
     @fake_read(a@15)
     // `assert_eq`
     @19 := const (9 : usize)
-    @36 := &a@15
-    @37 := @ArrayIndexShared<'_, u32, 10 : usize>(move (@36), copy (@19))
-    @18 := &*(@37)
+    @34 := &a@15
+    @35 := @ArrayIndexShared<'_, u32, 10 : usize>(move (@34), copy (@19))
+    @18 := &*(@35)
     @21 := const (9 : u32)
     @20 := &@21
     @17 := (move (@18), move (@20))
@@ -334,8 +321,6 @@ fn test_crate::foo()
     }
     drop @26
     drop @25
-    @34 := ()
-    @16 := move (@34)
     drop @24
     drop right_val@23
     drop left_val@22
@@ -343,8 +328,7 @@ fn test_crate::foo()
     drop @19
     drop @17
     drop @16
-    @35 := ()
-    @0 := move (@35)
+    @0 := ()
     drop a@15
     drop super_long_field_name@9
     drop x@8
@@ -372,7 +356,6 @@ fn test_crate::thing()
     let @3: (); // anonymous local
     let @4: u32; // anonymous local
     let @5: u32; // anonymous local
-    let @6: (); // anonymous local
 
     // This comment belongs above the assignment to `x` and not above intermediate computations.
     @5 := test_crate::CONSTANT
@@ -384,8 +367,7 @@ fn test_crate::thing()
     @3 := test_crate::function_call(move (@4))
     drop @4
     drop @3
-    @6 := ()
-    @0 := move (@6)
+    @0 := ()
     drop x@1
     @0 := ()
     return
@@ -395,12 +377,10 @@ fn test_crate::fake_read(@1: u32)
 {
     let @0: (); // return
     let x@1: u32; // arg #1
-    let @2: (); // anonymous local
 
     // This statement is translated to a `fake_read`.
     @fake_read(x@1)
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/demo.out b/charon/tests/ui/demo.out
index 009d56940..9f2aba594 100644
--- a/charon/tests/ui/demo.out
+++ b/charon/tests/ui/demo.out
@@ -73,11 +73,9 @@ fn test_crate::incr<'a>(@1: &'a mut (u32))
 {
     let @0: (); // return
     let x@1: &'_ mut (u32); // arg #1
-    let @2: (); // anonymous local
 
     *(x@1) := copy (*(x@1)) + const (1 : u32)
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -95,7 +93,6 @@ fn test_crate::use_incr()
     let @8: (); // anonymous local
     let @9: &'_ mut (u32); // anonymous local
     let @10: &'_ mut (u32); // anonymous local
-    let @11: (); // anonymous local
 
     x@1 := const (0 : u32)
     @fake_read(x@1)
@@ -117,8 +114,7 @@ fn test_crate::use_incr()
     drop @9
     drop @10
     drop @8
-    @11 := ()
-    @0 := move (@11)
+    @0 := ()
     drop x@1
     @0 := ()
     return
@@ -257,57 +253,47 @@ where
     let l@1: &'_ mut (test_crate::CList<T>[@TraitClause0]); // arg #1
     let i@2: u32; // arg #2
     let @3: (); // anonymous local
-    let @4: (); // anonymous local
-    let x@5: &'_ mut (T); // local
-    let tl@6: &'_ mut (alloc::boxed::Box<test_crate::CList<T>[@TraitClause0]>[core::marker::Sized<alloc::alloc::Global>]); // local
-    let @7: (); // anonymous local
-    let @8: bool; // anonymous local
-    let @9: u32; // anonymous local
-    let @10: &'_ mut (test_crate::CList<T>[@TraitClause0]); // anonymous local
-    let @11: (); // anonymous local
-    let @12: (); // anonymous local
-    let @13: (); // anonymous local
-    let @14: (); // anonymous local
+    let x@4: &'_ mut (T); // local
+    let tl@5: &'_ mut (alloc::boxed::Box<test_crate::CList<T>[@TraitClause0]>[core::marker::Sized<alloc::alloc::Global>]); // local
+    let @6: (); // anonymous local
+    let @7: bool; // anonymous local
+    let @8: u32; // anonymous local
+    let @9: &'_ mut (test_crate::CList<T>[@TraitClause0]); // anonymous local
+    let @10: (); // anonymous local
 
     loop {
         @fake_read(l@1)
         match *(l@1) {
             0 => {
-                x@5 := &mut (*(l@1) as variant @0).0
-                tl@6 := &mut (*(l@1) as variant @0).1
-                @9 := copy (i@2)
-                @8 := move (@9) == const (0 : u32)
-                if move (@8) {
+                x@4 := &mut (*(l@1) as variant @0).0
+                tl@5 := &mut (*(l@1) as variant @0).1
+                @8 := copy (i@2)
+                @7 := move (@8) == const (0 : u32)
+                if move (@7) {
                 }
                 else {
-                    drop @9
-                    @13 := ()
-                    @7 := move (@13)
                     drop @8
                     drop @7
+                    drop @6
                     i@2 := copy (i@2) - const (1 : u32)
-                    @10 := &mut *(*(tl@6))
-                    l@1 := move (@10)
-                    drop @10
-                    @14 := ()
-                    @4 := move (@14)
-                    drop tl@6
-                    drop x@5
+                    @9 := &mut *(*(tl@5))
+                    l@1 := move (@9)
+                    drop @9
+                    drop tl@5
+                    drop x@4
                     continue 0
                 }
-                drop @9
-                @0 := &mut *(x@5)
                 drop @8
+                @0 := &mut *(x@4)
                 drop @7
-                drop tl@6
-                drop x@5
+                drop @6
+                drop tl@5
+                drop x@4
                 drop @3
                 return
             },
             _ => {
-                @12 := ()
-                @3 := move (@12)
-                drop @11
+                drop @10
                 drop @3
                 panic(core::panicking::panic_explicit)
             },
diff --git a/charon/tests/ui/disambiguator.out b/charon/tests/ui/disambiguator.out
index 04f2f2a9d..306d52b90 100644
--- a/charon/tests/ui/disambiguator.out
+++ b/charon/tests/ui/disambiguator.out
@@ -3,10 +3,8 @@
 fn test_crate::nonzero_disambiguator::my_function()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -14,10 +12,8 @@ fn test_crate::nonzero_disambiguator::my_function()
 fn test_crate::nonzero_disambiguator::my_function#1()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/diverging.out b/charon/tests/ui/diverging.out
index 57df1f662..6649f10ad 100644
--- a/charon/tests/ui/diverging.out
+++ b/charon/tests/ui/diverging.out
@@ -11,10 +11,8 @@ fn test_crate::my_panic(@1: u32) -> !
 fn test_crate::do_something_else()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/dyn-trait.out b/charon/tests/ui/dyn-trait.out
index 271d67c7a..b5df3a76c 100644
--- a/charon/tests/ui/dyn-trait.out
+++ b/charon/tests/ui/dyn-trait.out
@@ -57,10 +57,8 @@ where
     let @0: (); // return
     let @1: &'_ (dyn (exists(TODO))); // arg #1
     let @2: &'_ (dyn (exists(TODO))); // arg #2
-    let @3: (); // anonymous local
 
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     @0 := ()
     return
 }
@@ -69,10 +67,8 @@ fn test_crate::bar<'_0>(@1: &'_0 (dyn (exists(TODO))))
 {
     let @0: (); // return
     let @1: &'_ (dyn (exists(TODO))); // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/external.out b/charon/tests/ui/external.out
index c56b81dab..7d818b37a 100644
--- a/charon/tests/ui/external.out
+++ b/charon/tests/ui/external.out
@@ -147,7 +147,6 @@ fn test_crate::test_vec_push()
     let v@1: alloc::vec::Vec<u32, alloc::alloc::Global>[core::marker::Sized<u32>, core::marker::Sized<alloc::alloc::Global>]; // local
     let @2: (); // anonymous local
     let @3: &'_ mut (alloc::vec::Vec<u32, alloc::alloc::Global>[core::marker::Sized<u32>, core::marker::Sized<alloc::alloc::Global>]); // anonymous local
-    let @4: (); // anonymous local
 
     v@1 := alloc::vec::{alloc::vec::Vec<T, alloc::alloc::Global>[@TraitClause0, core::marker::Sized<alloc::alloc::Global>]}::new<u32>[core::marker::Sized<u32>]()
     @fake_read(v@1)
@@ -155,8 +154,7 @@ fn test_crate::test_vec_push()
     @2 := alloc::vec::{alloc::vec::Vec<T, A>[@TraitClause0, @TraitClause1]}#1::push<'_, u32, alloc::alloc::Global>[core::marker::Sized<u32>, core::marker::Sized<alloc::alloc::Global>](move (@3), const (0 : u32))
     drop @3
     drop @2
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     drop v@1
     drop v@1
     @0 := ()
@@ -190,15 +188,13 @@ fn test_crate::incr<'_0>(@1: &'_0 mut (core::cell::Cell<u32>))
     let rc@1: &'_ mut (core::cell::Cell<u32>); // arg #1
     let @2: &'_ mut (u32); // anonymous local
     let @3: &'_ mut (core::cell::Cell<u32>); // anonymous local
-    let @4: (); // anonymous local
 
     @3 := &two-phase-mut *(rc@1)
     @2 := core::cell::{core::cell::Cell<T>}#11::get_mut<'_, u32>(move (@3))
     drop @3
     *(@2) := copy (*(@2)) + const (1 : u32)
     drop @2
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/impl-trait.out b/charon/tests/ui/impl-trait.out
index 8b83aa2fe..b5635e517 100644
--- a/charon/tests/ui/impl-trait.out
+++ b/charon/tests/ui/impl-trait.out
@@ -64,7 +64,6 @@ fn test_crate::use_foo()
     let @3: &'_ (u32); // anonymous local
     let @4: &'_ (u32); // anonymous local
     let @5: &'_ (()); // anonymous local
-    let @6: (); // anonymous local
 
     foo@1 := test_crate::mk_foo()
     @fake_read(foo@1)
@@ -78,8 +77,7 @@ fn test_crate::use_foo()
     drop @2
     drop @4
     drop @2
-    @6 := ()
-    @0 := move (@6)
+    @0 := ()
     drop foo@1
     drop foo@1
     @0 := ()
@@ -114,10 +112,8 @@ impl test_crate::{impl test_crate::RPITIT for ()}#1 : test_crate::RPITIT<()>
 fn test_crate::RPITIT::make_foo<Self>() -> Self::
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     return
 }
 
@@ -136,7 +132,6 @@ where
     let @3: &'_ (@TraitClause1::parent_clause1::Type); // anonymous local
     let @4: &'_ (@TraitClause1::parent_clause1::Type); // anonymous local
     let @5: &'_ (@TraitClause1::); // anonymous local
-    let @6: (); // anonymous local
 
     foo@1 := @TraitClause1::make_foo()
     @fake_read(foo@1)
@@ -150,8 +145,7 @@ where
     drop @2
     drop @4
     drop @2
-    @6 := ()
-    @0 := move (@6)
+    @0 := ()
     drop foo@1
     drop foo@1
     @0 := ()
@@ -223,7 +217,6 @@ fn test_crate::use_wrap()
     let @5: &'_ (u32); // anonymous local
     let @6: &'_ (u32); // anonymous local
     let @7: u32; // anonymous local
-    let @8: (); // anonymous local
 
     f@1 := test_crate::wrap<u32>[core::marker::Sized<u32>]()
     @fake_read(f@1)
@@ -240,8 +233,7 @@ fn test_crate::use_wrap()
     drop @7
     drop @6
     drop @2
-    @8 := ()
-    @0 := move (@8)
+    @0 := ()
     drop f@1
     drop f@1
     @0 := ()
diff --git a/charon/tests/ui/issue-114-opaque-bodies.out b/charon/tests/ui/issue-114-opaque-bodies.out
index 1b29c913d..f7e9c2c22 100644
--- a/charon/tests/ui/issue-114-opaque-bodies.out
+++ b/charon/tests/ui/issue-114-opaque-bodies.out
@@ -176,10 +176,8 @@ fn test_crate::vec(@1: alloc::vec::Vec<u32, alloc::alloc::Global>[core::marker::
 {
     let @0: (); // return
     let _x@1: alloc::vec::Vec<u32, alloc::alloc::Global>[core::marker::Sized<u32>, core::marker::Sized<alloc::alloc::Global>]; // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     drop _x@1
     @0 := ()
     return
@@ -218,10 +216,8 @@ where
 {
     let @0: (); // return
     let _x@1: T; // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     drop _x@1
     @0 := ()
     return
diff --git a/charon/tests/ui/issue-118-generic-copy.out b/charon/tests/ui/issue-118-generic-copy.out
index 82e13fe64..0eb5f55f6 100644
--- a/charon/tests/ui/issue-118-generic-copy.out
+++ b/charon/tests/ui/issue-118-generic-copy.out
@@ -41,14 +41,12 @@ fn test_crate::copy_foo(@1: test_crate::Foo)
     let x@1: test_crate::Foo; // arg #1
     let y@2: test_crate::Foo; // local
     let z@3: test_crate::Foo; // local
-    let @4: (); // anonymous local
 
     y@2 := copy (x@1)
     @fake_read(y@2)
     z@3 := copy (x@1)
     @fake_read(z@3)
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     drop z@3
     drop y@2
     @0 := ()
@@ -64,14 +62,12 @@ where
     let x@1: T; // arg #1
     let y@2: T; // local
     let z@3: T; // local
-    let @4: (); // anonymous local
 
     y@2 := copy (x@1)
     @fake_read(y@2)
     z@3 := copy (x@1)
     @fake_read(z@3)
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     drop z@3
     drop y@2
     @0 := ()
@@ -94,14 +90,12 @@ where
     let x@1: @TraitClause1::Ty; // arg #1
     let y@2: @TraitClause1::Ty; // local
     let z@3: @TraitClause1::Ty; // local
-    let @4: (); // anonymous local
 
     y@2 := copy (x@1)
     @fake_read(y@2)
     z@3 := copy (x@1)
     @fake_read(z@3)
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     drop z@3
     drop y@2
     @0 := ()
diff --git a/charon/tests/ui/issue-165-vec-macro.out b/charon/tests/ui/issue-165-vec-macro.out
index 7e3281b9b..4fe94215a 100644
--- a/charon/tests/ui/issue-165-vec-macro.out
+++ b/charon/tests/ui/issue-165-vec-macro.out
@@ -42,7 +42,6 @@ fn test_crate::foo()
     let @4: alloc::boxed::Box<Array<i32, 1 : usize>>[core::marker::Sized<alloc::alloc::Global>]; // anonymous local
     let _v2@5: alloc::vec::Vec<i32, alloc::alloc::Global>[core::marker::Sized<i32>, core::marker::Sized<alloc::alloc::Global>]; // local
     let @6: Array<i32, 1 : usize>; // anonymous local
-    let @7: (); // anonymous local
 
     @6 := [const (1 : i32); 1 : usize]
     @4 := @BoxNew<Array<i32, 1 : usize>>[core::marker::Sized<alloc::alloc::Global>](move (@6))
@@ -57,8 +56,7 @@ fn test_crate::foo()
     @fake_read(_v@1)
     _v2@5 := alloc::vec::from_elem<i32>[core::marker::Sized<i32>, core::clone::impls::{impl core::clone::Clone for i32}#14](const (1 : i32), const (10 : usize))
     @fake_read(_v2@5)
-    @7 := ()
-    @0 := move (@7)
+    @0 := ()
     drop _v2@5
     drop _v2@5
     drop _v@1
@@ -78,7 +76,6 @@ fn test_crate::bar()
     let @4: alloc::boxed::Box<Array<test_crate::Foo, 1 : usize>>[core::marker::Sized<alloc::alloc::Global>]; // anonymous local
     let @5: test_crate::Foo; // anonymous local
     let @6: Array<test_crate::Foo, 1 : usize>; // anonymous local
-    let @7: (); // anonymous local
 
     @5 := test_crate::Foo {  }
     @6 := [move (@5); 1 : usize]
@@ -95,8 +92,7 @@ fn test_crate::bar()
     @fake_read(@1)
     drop @1
     drop @1
-    @7 := ()
-    @0 := move (@7)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/issue-297-cfg.out b/charon/tests/ui/issue-297-cfg.out
index 3940a89ae..4dcf57379 100644
--- a/charon/tests/ui/issue-297-cfg.out
+++ b/charon/tests/ui/issue-297-cfg.out
@@ -12,47 +12,39 @@ fn test_crate::f1<'_0>(@1: &'_0 (Slice<u8>)) -> usize
     let @7: bool; // anonymous local
     let @8: u8; // anonymous local
     let @9: usize; // anonymous local
-    let @10: (); // anonymous local
-    let @11: (); // anonymous local
+    let @10: &'_ (Slice<u8>); // anonymous local
+    let @11: &'_ (u8); // anonymous local
     let @12: &'_ (Slice<u8>); // anonymous local
     let @13: &'_ (u8); // anonymous local
-    let @14: &'_ (Slice<u8>); // anonymous local
-    let @15: &'_ (u8); // anonymous local
 
     sampled@2 := const (0 : usize)
     @fake_read(sampled@2)
     @6 := const (0 : usize)
-    @12 := &*(a@1)
-    @13 := @SliceIndexShared<'_, u8>(move (@12), copy (@6))
-    @5 := copy (*(@13))
+    @10 := &*(a@1)
+    @11 := @SliceIndexShared<'_, u8>(move (@10), copy (@6))
+    @5 := copy (*(@11))
     @4 := move (@5) < const (42 : u8)
     if move (@4) {
         drop @6
         drop @5
         @9 := const (1 : usize)
-        @14 := &*(a@1)
-        @15 := @SliceIndexShared<'_, u8>(move (@14), copy (@9))
-        @8 := copy (*(@15))
+        @12 := &*(a@1)
+        @13 := @SliceIndexShared<'_, u8>(move (@12), copy (@9))
+        @8 := copy (*(@13))
         @7 := move (@8) < const (16 : u8)
         if move (@7) {
             drop @9
             drop @8
             sampled@2 := copy (sampled@2) + const (100 : usize)
-            @11 := ()
-            @3 := move (@11)
         }
         else {
             drop @9
             drop @8
-            @10 := ()
-            @3 := move (@10)
         }
     }
     else {
         drop @6
         drop @5
-        @10 := ()
-        @3 := move (@10)
     }
     drop @7
     drop @4
@@ -130,61 +122,54 @@ fn test_crate::f2<'_0, '_1>(@1: &'_0 (Slice<u8>), @2: &'_1 mut (Slice<i16>)) ->
     let @7: &'_ (Slice<u8>); // anonymous local
     let iter@8: core::slice::iter::Chunks<'_, u8>[core::marker::Sized<u8>]; // local
     let @9: (); // anonymous local
-    let @10: (); // anonymous local
-    let @11: core::option::Option<&'_ (Slice<u8>)>[core::marker::Sized<&'_ (Slice<u8>)>]; // anonymous local
+    let @10: core::option::Option<&'_ (Slice<u8>)>[core::marker::Sized<&'_ (Slice<u8>)>]; // anonymous local
+    let @11: &'_ mut (core::slice::iter::Chunks<'_, u8>[core::marker::Sized<u8>]); // anonymous local
     let @12: &'_ mut (core::slice::iter::Chunks<'_, u8>[core::marker::Sized<u8>]); // anonymous local
-    let @13: &'_ mut (core::slice::iter::Chunks<'_, u8>[core::marker::Sized<u8>]); // anonymous local
-    let bytes@14: &'_ (Slice<u8>); // local
-    let b1@15: i16; // local
-    let @16: u8; // anonymous local
-    let @17: usize; // anonymous local
-    let b2@18: i16; // local
-    let @19: u8; // anonymous local
-    let @20: usize; // anonymous local
-    let b3@21: i16; // local
-    let @22: u8; // anonymous local
-    let @23: usize; // anonymous local
-    let d1@24: i16; // local
+    let bytes@13: &'_ (Slice<u8>); // local
+    let b1@14: i16; // local
+    let @15: u8; // anonymous local
+    let @16: usize; // anonymous local
+    let b2@17: i16; // local
+    let @18: u8; // anonymous local
+    let @19: usize; // anonymous local
+    let b3@20: i16; // local
+    let @21: u8; // anonymous local
+    let @22: usize; // anonymous local
+    let d1@23: i16; // local
+    let @24: i16; // anonymous local
     let @25: i16; // anonymous local
     let @26: i16; // anonymous local
     let @27: i16; // anonymous local
-    let @28: i16; // anonymous local
-    let d2@29: i16; // local
+    let d2@28: i16; // local
+    let @29: i16; // anonymous local
     let @30: i16; // anonymous local
     let @31: i16; // anonymous local
     let @32: i16; // anonymous local
-    let @33: i16; // anonymous local
-    let @34: (); // anonymous local
-    let @35: bool; // anonymous local
-    let @36: i16; // anonymous local
-    let @37: bool; // anonymous local
-    let @38: usize; // anonymous local
-    let @39: i16; // anonymous local
-    let @40: usize; // anonymous local
-    let @41: bool; // anonymous local
-    let @42: i16; // anonymous local
-    let @43: bool; // anonymous local
-    let @44: usize; // anonymous local
-    let @45: i16; // anonymous local
-    let @46: usize; // anonymous local
-    let @47: (); // anonymous local
-    let @48: i16; // anonymous local
-    let @49: (); // anonymous local
-    let @50: (); // anonymous local
-    let @51: i16; // anonymous local
-    let @52: (); // anonymous local
-    let @53: (); // anonymous local
-    let @54: (); // anonymous local
-    let @55: &'_ (Slice<u8>); // anonymous local
-    let @56: &'_ (u8); // anonymous local
-    let @57: &'_ (Slice<u8>); // anonymous local
-    let @58: &'_ (u8); // anonymous local
-    let @59: &'_ (Slice<u8>); // anonymous local
-    let @60: &'_ (u8); // anonymous local
-    let @61: &'_ mut (Slice<i16>); // anonymous local
-    let @62: &'_ mut (i16); // anonymous local
-    let @63: &'_ mut (Slice<i16>); // anonymous local
-    let @64: &'_ mut (i16); // anonymous local
+    let @33: (); // anonymous local
+    let @34: bool; // anonymous local
+    let @35: i16; // anonymous local
+    let @36: bool; // anonymous local
+    let @37: usize; // anonymous local
+    let @38: i16; // anonymous local
+    let @39: usize; // anonymous local
+    let @40: bool; // anonymous local
+    let @41: i16; // anonymous local
+    let @42: bool; // anonymous local
+    let @43: usize; // anonymous local
+    let @44: i16; // anonymous local
+    let @45: usize; // anonymous local
+    let @46: i16; // anonymous local
+    let @47: i16; // anonymous local
+    let @48: &'_ (Slice<u8>); // anonymous local
+    let @49: &'_ (u8); // anonymous local
+    let @50: &'_ (Slice<u8>); // anonymous local
+    let @51: &'_ (u8); // anonymous local
+    let @52: &'_ (Slice<u8>); // anonymous local
+    let @53: &'_ (u8); // anonymous local
+    let @54: &'_ mut (Slice<i16>); // anonymous local
+    let @55: &'_ mut (i16); // anonymous local
+    let @56: &'_ mut (Slice<i16>); // anonymous local
+    let @57: &'_ mut (i16); // anonymous local
 
     sampled@3 := const (0 : usize)
     @fake_read(sampled@3)
@@ -196,148 +181,132 @@ fn test_crate::f2<'_0, '_1>(@1: &'_0 (Slice<u8>), @2: &'_1 mut (Slice<i16>)) ->
     @fake_read(@5)
     iter@8 := move (@5)
     loop {
-        @13 := &mut iter@8
-        @12 := &two-phase-mut *(@13)
-        @11 := core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::next<'_, '_, u8>[core::marker::Sized<u8>](move (@12))
-        drop @12
-        @fake_read(@11)
-        match @11 {
+        @12 := &mut iter@8
+        @11 := &two-phase-mut *(@12)
+        @10 := core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::next<'_, '_, u8>[core::marker::Sized<u8>](move (@11))
+        drop @11
+        @fake_read(@10)
+        match @10 {
             0 => {
                 break 0
             },
             1 => {
-                bytes@14 := copy ((@11 as variant @1).0)
-                @17 := const (0 : usize)
-                @59 := &*(bytes@14)
-                @60 := @SliceIndexShared<'_, u8>(move (@59), copy (@17))
-                @16 := copy (*(@60))
-                b1@15 := cast<u8, i16>(move (@16))
+                bytes@13 := copy ((@10 as variant @1).0)
+                @16 := const (0 : usize)
+                @52 := &*(bytes@13)
+                @53 := @SliceIndexShared<'_, u8>(move (@52), copy (@16))
+                @15 := copy (*(@53))
+                b1@14 := cast<u8, i16>(move (@15))
+                drop @15
+                @fake_read(b1@14)
                 drop @16
-                @fake_read(b1@15)
-                drop @17
-                @20 := const (1 : usize)
-                @57 := &*(bytes@14)
-                @58 := @SliceIndexShared<'_, u8>(move (@57), copy (@20))
-                @19 := copy (*(@58))
-                b2@18 := cast<u8, i16>(move (@19))
+                @19 := const (1 : usize)
+                @50 := &*(bytes@13)
+                @51 := @SliceIndexShared<'_, u8>(move (@50), copy (@19))
+                @18 := copy (*(@51))
+                b2@17 := cast<u8, i16>(move (@18))
+                drop @18
+                @fake_read(b2@17)
                 drop @19
-                @fake_read(b2@18)
-                drop @20
-                @23 := const (2 : usize)
-                @55 := &*(bytes@14)
-                @56 := @SliceIndexShared<'_, u8>(move (@55), copy (@23))
-                @22 := copy (*(@56))
-                b3@21 := cast<u8, i16>(move (@22))
+                @22 := const (2 : usize)
+                @48 := &*(bytes@13)
+                @49 := @SliceIndexShared<'_, u8>(move (@48), copy (@22))
+                @21 := copy (*(@49))
+                b3@20 := cast<u8, i16>(move (@21))
+                drop @21
+                @fake_read(b3@20)
                 drop @22
-                @fake_read(b3@21)
-                drop @23
-                @27 := copy (b2@18)
-                @26 := move (@27) & const (15 : i16)
-                drop @27
-                @25 := move (@26) << const (8 : i32)
+                @26 := copy (b2@17)
+                @25 := move (@26) & const (15 : i16)
                 drop @26
-                @28 := copy (b1@15)
-                d1@24 := move (@25) | move (@28)
-                drop @28
+                @24 := move (@25) << const (8 : i32)
                 drop @25
-                @fake_read(d1@24)
-                @31 := copy (b3@21)
-                @30 := move (@31) << const (4 : i32)
-                drop @31
-                @33 := copy (b2@18)
-                @32 := move (@33) >> const (4 : i32)
-                drop @33
-                d2@29 := move (@30) | move (@32)
-                drop @32
+                @27 := copy (b1@14)
+                d1@23 := move (@24) | move (@27)
+                drop @27
+                drop @24
+                @fake_read(d1@23)
+                @30 := copy (b3@20)
+                @29 := move (@30) << const (4 : i32)
                 drop @30
-                @fake_read(d2@29)
-                @36 := copy (d1@24)
-                @48 := test_crate::FIELD_MODULUS
-                @35 := move (@36) < move (@48)
-                if move (@35) {
-                    drop @36
-                    @38 := copy (sampled@3)
-                    @37 := move (@38) < const (16 : usize)
-                    if move (@37) {
+                @32 := copy (b2@17)
+                @31 := move (@32) >> const (4 : i32)
+                drop @32
+                d2@28 := move (@29) | move (@31)
+                drop @31
+                drop @29
+                @fake_read(d2@28)
+                @35 := copy (d1@23)
+                @46 := test_crate::FIELD_MODULUS
+                @34 := move (@35) < move (@46)
+                if move (@34) {
+                    drop @35
+                    @37 := copy (sampled@3)
+                    @36 := move (@37) < const (16 : usize)
+                    if move (@36) {
+                        drop @37
+                        @38 := copy (d1@23)
+                        @39 := copy (sampled@3)
+                        @54 := &mut *(result@2)
+                        @55 := @SliceIndexMut<'_, i16>(move (@54), copy (@39))
+                        *(@55) := move (@38)
                         drop @38
-                        @39 := copy (d1@24)
-                        @40 := copy (sampled@3)
-                        @61 := &mut *(result@2)
-                        @62 := @SliceIndexMut<'_, i16>(move (@61), copy (@40))
-                        *(@62) := move (@39)
                         drop @39
-                        drop @40
                         sampled@3 := copy (sampled@3) + const (1 : usize)
-                        @49 := ()
-                        @34 := move (@49)
                     }
                     else {
-                        drop @38
-                        @50 := ()
-                        @34 := move (@50)
+                        drop @37
                     }
                 }
                 else {
-                    drop @36
-                    @50 := ()
-                    @34 := move (@50)
+                    drop @35
                 }
-                drop @37
-                drop @35
+                drop @36
                 drop @34
-                @42 := copy (d2@29)
-                @51 := test_crate::FIELD_MODULUS
-                @41 := move (@42) < move (@51)
-                if move (@41) {
-                    drop @42
-                    @44 := copy (sampled@3)
-                    @43 := move (@44) < const (16 : usize)
-                    if move (@43) {
+                drop @33
+                @41 := copy (d2@28)
+                @47 := test_crate::FIELD_MODULUS
+                @40 := move (@41) < move (@47)
+                if move (@40) {
+                    drop @41
+                    @43 := copy (sampled@3)
+                    @42 := move (@43) < const (16 : usize)
+                    if move (@42) {
+                        drop @43
+                        @44 := copy (d2@28)
+                        @45 := copy (sampled@3)
+                        @56 := &mut *(result@2)
+                        @57 := @SliceIndexMut<'_, i16>(move (@56), copy (@45))
+                        *(@57) := move (@44)
                         drop @44
-                        @45 := copy (d2@29)
-                        @46 := copy (sampled@3)
-                        @63 := &mut *(result@2)
-                        @64 := @SliceIndexMut<'_, i16>(move (@63), copy (@46))
-                        *(@64) := move (@45)
                         drop @45
-                        drop @46
                         sampled@3 := copy (sampled@3) + const (1 : usize)
-                        @52 := ()
-                        @10 := move (@52)
                     }
                     else {
-                        drop @44
-                        @53 := ()
-                        @10 := move (@53)
+                        drop @43
                     }
                 }
                 else {
-                    drop @42
-                    @53 := ()
-                    @10 := move (@53)
+                    drop @41
                 }
-                drop @43
-                drop @41
-                drop d2@29
-                drop d1@24
-                drop b3@21
-                drop b2@18
-                drop b1@15
-                drop bytes@14
-                drop @13
-                drop @11
+                drop @42
+                drop @40
+                drop d2@28
+                drop d1@23
+                drop b3@20
+                drop b2@17
+                drop b1@14
+                drop bytes@13
+                drop @12
                 drop @10
-                @54 := ()
-                @9 := move (@54)
+                drop @9
                 continue 0
             },
         }
     }
-    @47 := ()
-    @4 := move (@47)
-    drop @13
-    drop @11
+    drop @12
     drop @10
+    drop @9
     drop iter@8
     drop @5
     drop @4
diff --git a/charon/tests/ui/issue-320-slice-pattern.out b/charon/tests/ui/issue-320-slice-pattern.out
index 2419ebbc8..562303293 100644
--- a/charon/tests/ui/issue-320-slice-pattern.out
+++ b/charon/tests/ui/issue-320-slice-pattern.out
@@ -7,28 +7,26 @@ fn test_crate::slice_pat1()
     let _a@2: i32; // local
     let _b@3: Array<i32, 2 : usize>; // local
     let _c@4: i32; // local
-    let @5: (); // anonymous local
-    let @6: &'_ (Array<i32, 4 : usize>); // anonymous local
-    let @7: &'_ (i32); // anonymous local
-    let @8: &'_ (Array<i32, 4 : usize>); // anonymous local
-    let @9: &'_ (Slice<i32>); // anonymous local
-    let @10: &'_ (Array<i32, 4 : usize>); // anonymous local
-    let @11: &'_ (i32); // anonymous local
+    let @5: &'_ (Array<i32, 4 : usize>); // anonymous local
+    let @6: &'_ (i32); // anonymous local
+    let @7: &'_ (Array<i32, 4 : usize>); // anonymous local
+    let @8: &'_ (Slice<i32>); // anonymous local
+    let @9: &'_ (Array<i32, 4 : usize>); // anonymous local
+    let @10: &'_ (i32); // anonymous local
 
     array@1 := @ArrayRepeat<'_, i32, 4 : usize>(const (0 : i32))
     @fake_read(array@1)
     @fake_read(array@1)
-    @10 := &array@1
-    @11 := @ArrayIndexShared<'_, i32, 4 : usize>(move (@10), const (0 : usize))
-    _a@2 := copy (*(@11))
-    @8 := &array@1
-    @9 := @ArraySubSliceShared<'_, i32, 4 : usize>(move (@8), const (1 : usize), const (3 : usize))
-    _b@3 := copy (*(@9))
-    @6 := &array@1
-    @7 := @ArrayIndexShared<'_, i32, 4 : usize>(move (@6), const (3 : usize))
-    _c@4 := copy (*(@7))
-    @5 := ()
-    @0 := move (@5)
+    @9 := &array@1
+    @10 := @ArrayIndexShared<'_, i32, 4 : usize>(move (@9), const (0 : usize))
+    _a@2 := copy (*(@10))
+    @7 := &array@1
+    @8 := @ArraySubSliceShared<'_, i32, 4 : usize>(move (@7), const (1 : usize), const (3 : usize))
+    _b@3 := copy (*(@8))
+    @5 := &array@1
+    @6 := @ArrayIndexShared<'_, i32, 4 : usize>(move (@5), const (3 : usize))
+    _c@4 := copy (*(@6))
+    @0 := ()
     drop _c@4
     drop _b@3
     drop _a@2
@@ -46,13 +44,12 @@ fn test_crate::slice_pat2()
     let _a@4: &'_ (i32); // local
     let _b@5: &'_ (Array<i32, 2 : usize>); // local
     let _c@6: &'_ (i32); // local
-    let @7: (); // anonymous local
-    let @8: &'_ (Array<i32, 4 : usize>); // anonymous local
-    let @9: &'_ (i32); // anonymous local
-    let @10: &'_ (Array<i32, 4 : usize>); // anonymous local
-    let @11: &'_ (Slice<i32>); // anonymous local
-    let @12: &'_ (Array<i32, 4 : usize>); // anonymous local
-    let @13: &'_ (i32); // anonymous local
+    let @7: &'_ (Array<i32, 4 : usize>); // anonymous local
+    let @8: &'_ (i32); // anonymous local
+    let @9: &'_ (Array<i32, 4 : usize>); // anonymous local
+    let @10: &'_ (Slice<i32>); // anonymous local
+    let @11: &'_ (Array<i32, 4 : usize>); // anonymous local
+    let @12: &'_ (i32); // anonymous local
 
     @3 := @ArrayRepeat<'_, i32, 4 : usize>(const (0 : i32))
     @2 := &@3
@@ -60,17 +57,16 @@ fn test_crate::slice_pat2()
     @fake_read(array_ref@1)
     drop @2
     @fake_read(array_ref@1)
-    @12 := &*(array_ref@1)
-    @13 := @ArrayIndexShared<'_, i32, 4 : usize>(move (@12), const (0 : usize))
-    _a@4 := &*(@13)
-    @10 := &*(array_ref@1)
-    @11 := @ArraySubSliceShared<'_, i32, 4 : usize>(move (@10), const (1 : usize), const (3 : usize))
-    _b@5 := &*(@11)
-    @8 := &*(array_ref@1)
-    @9 := @ArrayIndexShared<'_, i32, 4 : usize>(move (@8), const (3 : usize))
-    _c@6 := &*(@9)
-    @7 := ()
-    @0 := move (@7)
+    @11 := &*(array_ref@1)
+    @12 := @ArrayIndexShared<'_, i32, 4 : usize>(move (@11), const (0 : usize))
+    _a@4 := &*(@12)
+    @9 := &*(array_ref@1)
+    @10 := @ArraySubSliceShared<'_, i32, 4 : usize>(move (@9), const (1 : usize), const (3 : usize))
+    _b@5 := &*(@10)
+    @7 := &*(array_ref@1)
+    @8 := @ArrayIndexShared<'_, i32, 4 : usize>(move (@7), const (3 : usize))
+    _c@6 := &*(@8)
+    @0 := ()
     drop _c@6
     drop _b@5
     drop _a@4
@@ -93,17 +89,16 @@ fn test_crate::slice_pat3()
     let @8: usize; // anonymous local
     let @9: usize; // anonymous local
     let @10: bool; // anonymous local
-    let @11: (); // anonymous local
-    let @12: &'_ (Slice<i32>); // anonymous local
+    let @11: &'_ (Slice<i32>); // anonymous local
+    let @12: usize; // anonymous local
     let @13: usize; // anonymous local
-    let @14: usize; // anonymous local
-    let @15: &'_ (i32); // anonymous local
-    let @16: &'_ (Slice<i32>); // anonymous local
+    let @14: &'_ (i32); // anonymous local
+    let @15: &'_ (Slice<i32>); // anonymous local
+    let @16: usize; // anonymous local
     let @17: usize; // anonymous local
-    let @18: usize; // anonymous local
+    let @18: &'_ (Slice<i32>); // anonymous local
     let @19: &'_ (Slice<i32>); // anonymous local
-    let @20: &'_ (Slice<i32>); // anonymous local
-    let @21: &'_ (i32); // anonymous local
+    let @20: &'_ (i32); // anonymous local
 
     @4 := @ArrayRepeat<'_, i32, 4 : usize>(const (0 : i32))
     @3 := &@4
@@ -124,21 +119,20 @@ fn test_crate::slice_pat3()
         drop _a@5
         panic(core::panicking::panic_explicit)
     }
-    @20 := &*(slice@1)
-    @21 := @SliceIndexShared<'_, i32>(move (@20), const (0 : usize))
-    _a@5 := &*(@21)
-    @16 := &*(slice@1)
-    @17 := len(*(slice@1))
-    @18 := copy (@17) - const (1 : usize)
-    @19 := @SliceSubSliceShared<'_, i32>(move (@16), const (1 : usize), copy (@18))
-    _b@6 := &*(@19)
-    @12 := &*(slice@1)
-    @13 := len(*(slice@1))
-    @14 := copy (@13) - const (1 : usize)
-    @15 := @SliceIndexShared<'_, i32>(move (@12), copy (@14))
-    _c@7 := &*(@15)
-    @11 := ()
-    @0 := move (@11)
+    @19 := &*(slice@1)
+    @20 := @SliceIndexShared<'_, i32>(move (@19), const (0 : usize))
+    _a@5 := &*(@20)
+    @15 := &*(slice@1)
+    @16 := len(*(slice@1))
+    @17 := copy (@16) - const (1 : usize)
+    @18 := @SliceSubSliceShared<'_, i32>(move (@15), const (1 : usize), copy (@17))
+    _b@6 := &*(@18)
+    @11 := &*(slice@1)
+    @12 := len(*(slice@1))
+    @13 := copy (@12) - const (1 : usize)
+    @14 := @SliceIndexShared<'_, i32>(move (@11), copy (@13))
+    _c@7 := &*(@14)
+    @0 := ()
     drop _c@7
     drop _b@6
     drop _a@5
diff --git a/charon/tests/ui/issue-322-macro-disambiguator.out b/charon/tests/ui/issue-322-macro-disambiguator.out
index 071e50116..eef27f85a 100644
--- a/charon/tests/ui/issue-322-macro-disambiguator.out
+++ b/charon/tests/ui/issue-322-macro-disambiguator.out
@@ -11,24 +11,16 @@ fn test_crate::main()
     let @2: test_crate::main::AssertIsAsBytes; // anonymous local
     let @3: (); // anonymous local
     let @4: test_crate::main::AssertIsAsBytes#1; // anonymous local
-    let @5: (); // anonymous local
-    let @6: (); // anonymous local
-    let @7: (); // anonymous local
 
     @2 := test_crate::main::AssertIsAsBytes {  }
     @fake_read(@2)
     drop @2
-    @5 := ()
-    @1 := move (@5)
     drop @1
     @4 := test_crate::main::AssertIsAsBytes#1 {  }
     @fake_read(@4)
     drop @4
-    @6 := ()
-    @3 := move (@6)
     drop @3
-    @7 := ()
-    @0 := move (@7)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/issue-323-closure-borrow.out b/charon/tests/ui/issue-323-closure-borrow.out
index ac4bd9a67..b7b239732 100644
--- a/charon/tests/ui/issue-323-closure-borrow.out
+++ b/charon/tests/ui/issue-323-closure-borrow.out
@@ -6,10 +6,8 @@ fn test_crate::{test_crate::Rng}::next_u64<'_0>(@1: &'_0 mut (test_crate::Rng))
 {
     let @0: (); // return
     let self@1: &'_ mut (test_crate::Rng); // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -20,14 +18,12 @@ fn test_crate::new::closure<'_0, '_1>(@1: &'_0 mut ((&'_1 mut (test_crate::Rng))
     let state@1: &'_0 mut ((&'_1 mut (test_crate::Rng))); // arg #1
     let @2: (); // anonymous local
     let @3: &'_ mut (test_crate::Rng); // anonymous local
-    let @4: (); // anonymous local
 
     @3 := &two-phase-mut *((*(state@1)).0)
     @2 := test_crate::{test_crate::Rng}::next_u64<'_>(move (@3))
     drop @3
     drop @2
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     @0 := ()
     return
 }
@@ -38,15 +34,13 @@ fn test_crate::new<'_0>(@1: &'_0 mut (test_crate::Rng))
     let rng@1: &'_ mut (test_crate::Rng); // arg #1
     let @2: fn(); // anonymous local
     let @3: &'_ mut (test_crate::Rng); // anonymous local
-    let @4: (); // anonymous local
 
     @3 := &uniq *(rng@1)
     @2 := {test_crate::new::closure} {move (@3)}
     drop @3
     @fake_read(@2)
     drop @2
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/issue-372-type-param-out-of-range.out b/charon/tests/ui/issue-372-type-param-out-of-range.out
index f846387fb..e18ed8535 100644
--- a/charon/tests/ui/issue-372-type-param-out-of-range.out
+++ b/charon/tests/ui/issue-372-type-param-out-of-range.out
@@ -38,10 +38,8 @@ where
     for<'_0> @TraitClause2::parent_clause0::Output = (),
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -54,10 +52,8 @@ where
     for<'b> @TraitClause2::parent_clause0::Output = (),
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -71,10 +67,8 @@ where
     for<'_0> @TraitClause1::parent_clause0::Output = (),
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/issue-378-ctor-as-fn.out b/charon/tests/ui/issue-378-ctor-as-fn.out
index b455dddf0..580f9cc89 100644
--- a/charon/tests/ui/issue-378-ctor-as-fn.out
+++ b/charon/tests/ui/issue-378-ctor-as-fn.out
@@ -84,7 +84,6 @@ fn test_crate::main()
     let @15: &'_ (i32); // anonymous local
     let @16: &'_ (i32); // anonymous local
     let @17: i32; // anonymous local
-    let @18: (); // anonymous local
 
     f@1 := const (core::option::Option::Some<u8>[core::marker::Sized<u8>])
     @fake_read(f@1)
@@ -125,8 +124,7 @@ fn test_crate::main()
     drop @17
     drop @16
     drop @13
-    @18 := ()
-    @0 := move (@18)
+    @0 := ()
     drop f@12
     drop f@8
     drop f@4
diff --git a/charon/tests/ui/issue-4-slice-try-into-array.out b/charon/tests/ui/issue-4-slice-try-into-array.out
index a01c2c2b3..423152a43 100644
--- a/charon/tests/ui/issue-4-slice-try-into-array.out
+++ b/charon/tests/ui/issue-4-slice-try-into-array.out
@@ -100,7 +100,6 @@ fn test_crate::trait_error<'_0>(@1: &'_0 (Slice<u8>))
     let _array@2: Array<u8, 4 : usize>; // local
     let @3: core::result::Result<Array<u8, 4 : usize>, core::array::TryFromSliceError>[core::marker::Sized<Array<u8, 4 : usize>>, core::marker::Sized<core::array::TryFromSliceError>]; // anonymous local
     let @4: &'_ (Slice<u8>); // anonymous local
-    let @5: (); // anonymous local
 
     @4 := &*(s@1)
     @3 := core::convert::{impl core::convert::TryInto<U> for T}#6::try_into<&'_ (Slice<u8>), Array<u8, 4 : usize>>[core::marker::Sized<&'_ (Slice<u8>)>, core::marker::Sized<Array<u8, 4 : usize>>, core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7<'_, u8, 4 : usize>[core::marker::Sized<u8>, core::marker::{impl core::marker::Copy for u8}#38]](move (@4))
@@ -108,8 +107,7 @@ fn test_crate::trait_error<'_0>(@1: &'_0 (Slice<u8>))
     _array@2 := core::result::{core::result::Result<T, E>[@TraitClause0, @TraitClause1]}::unwrap<Array<u8, 4 : usize>, core::array::TryFromSliceError>[core::marker::Sized<Array<u8, 4 : usize>>, core::marker::Sized<core::array::TryFromSliceError>, core::array::{impl core::fmt::Debug for core::array::TryFromSliceError}#26](move (@3))
     drop @3
     @fake_read(_array@2)
-    @5 := ()
-    @0 := move (@5)
+    @0 := ()
     drop _array@2
     @0 := ()
     return
diff --git a/charon/tests/ui/issue-4-traits.out b/charon/tests/ui/issue-4-traits.out
index a01c2c2b3..423152a43 100644
--- a/charon/tests/ui/issue-4-traits.out
+++ b/charon/tests/ui/issue-4-traits.out
@@ -100,7 +100,6 @@ fn test_crate::trait_error<'_0>(@1: &'_0 (Slice<u8>))
     let _array@2: Array<u8, 4 : usize>; // local
     let @3: core::result::Result<Array<u8, 4 : usize>, core::array::TryFromSliceError>[core::marker::Sized<Array<u8, 4 : usize>>, core::marker::Sized<core::array::TryFromSliceError>]; // anonymous local
     let @4: &'_ (Slice<u8>); // anonymous local
-    let @5: (); // anonymous local
 
     @4 := &*(s@1)
     @3 := core::convert::{impl core::convert::TryInto<U> for T}#6::try_into<&'_ (Slice<u8>), Array<u8, 4 : usize>>[core::marker::Sized<&'_ (Slice<u8>)>, core::marker::Sized<Array<u8, 4 : usize>>, core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7<'_, u8, 4 : usize>[core::marker::Sized<u8>, core::marker::{impl core::marker::Copy for u8}#38]](move (@4))
@@ -108,8 +107,7 @@ fn test_crate::trait_error<'_0>(@1: &'_0 (Slice<u8>))
     _array@2 := core::result::{core::result::Result<T, E>[@TraitClause0, @TraitClause1]}::unwrap<Array<u8, 4 : usize>, core::array::TryFromSliceError>[core::marker::Sized<Array<u8, 4 : usize>>, core::marker::Sized<core::array::TryFromSliceError>, core::array::{impl core::fmt::Debug for core::array::TryFromSliceError}#26](move (@3))
     drop @3
     @fake_read(_array@2)
-    @5 := ()
-    @0 := move (@5)
+    @0 := ()
     drop _array@2
     @0 := ()
     return
diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out
index 1cac871f2..094d58e13 100644
--- a/charon/tests/ui/issue-45-misc.out
+++ b/charon/tests/ui/issue-45-misc.out
@@ -186,18 +186,14 @@ fn test_crate::cbd(@1: Array<u8, 33 : usize>)
     let @3: core::ops::range::Range<u8>[core::marker::Sized<u8>]; // anonymous local
     let iter@4: core::ops::range::Range<u8>[core::marker::Sized<u8>]; // local
     let @5: (); // anonymous local
-    let @6: (); // anonymous local
-    let @7: core::option::Option<u8>[core::marker::Sized<u8>]; // anonymous local
+    let @6: core::option::Option<u8>[core::marker::Sized<u8>]; // anonymous local
+    let @7: &'_ mut (core::ops::range::Range<u8>[core::marker::Sized<u8>]); // anonymous local
     let @8: &'_ mut (core::ops::range::Range<u8>[core::marker::Sized<u8>]); // anonymous local
-    let @9: &'_ mut (core::ops::range::Range<u8>[core::marker::Sized<u8>]); // anonymous local
-    let i@10: u8; // local
-    let @11: u8; // anonymous local
-    let @12: usize; // anonymous local
-    let @13: (); // anonymous local
-    let @14: (); // anonymous local
-    let @15: (); // anonymous local
-    let @16: &'_ mut (Array<u8, 33 : usize>); // anonymous local
-    let @17: &'_ mut (u8); // anonymous local
+    let i@9: u8; // local
+    let @10: u8; // anonymous local
+    let @11: usize; // anonymous local
+    let @12: &'_ mut (Array<u8, 33 : usize>); // anonymous local
+    let @13: &'_ mut (u8); // anonymous local
 
     @3 := core::ops::range::Range { start: const (0 : u8), end: const (3 : u8) }
     @2 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::ops::range::Range<u8>[core::marker::Sized<u8>]>[core::marker::Sized<core::ops::range::Range<u8>[core::marker::Sized<u8>]>, core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6<u8>[core::marker::Sized<u8>, core::iter::range::{impl core::iter::range::Step for u8}#35]](move (@3))
@@ -205,41 +201,36 @@ fn test_crate::cbd(@1: Array<u8, 33 : usize>)
     @fake_read(@2)
     iter@4 := move (@2)
     loop {
-        @9 := &mut iter@4
-        @8 := &two-phase-mut *(@9)
-        @7 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, u8>[core::marker::Sized<u8>, core::iter::range::{impl core::iter::range::Step for u8}#35](move (@8))
-        drop @8
-        @fake_read(@7)
-        match @7 {
+        @8 := &mut iter@4
+        @7 := &two-phase-mut *(@8)
+        @6 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, u8>[core::marker::Sized<u8>, core::iter::range::{impl core::iter::range::Step for u8}#35](move (@7))
+        drop @7
+        @fake_read(@6)
+        match @6 {
             0 => {
                 break 0
             },
             1 => {
-                i@10 := copy ((@7 as variant @1).0)
-                @11 := copy (i@10)
-                @12 := const (0 : usize)
-                @16 := &mut prf_input@1
-                @17 := @ArrayIndexMut<'_, u8, 33 : usize>(move (@16), copy (@12))
-                *(@17) := move (@11)
+                i@9 := copy ((@6 as variant @1).0)
+                @10 := copy (i@9)
+                @11 := const (0 : usize)
+                @12 := &mut prf_input@1
+                @13 := @ArrayIndexMut<'_, u8, 33 : usize>(move (@12), copy (@11))
+                *(@13) := move (@10)
+                drop @10
                 drop @11
-                drop @12
-                @14 := ()
-                @6 := move (@14)
-                drop i@10
-                drop @9
-                drop @7
+                drop i@9
+                drop @8
                 drop @6
-                @15 := ()
-                @5 := move (@15)
+                drop @5
                 continue 0
             },
         }
     }
-    @13 := ()
-    @0 := move (@13)
-    drop @9
-    drop @7
+    @0 := ()
+    drop @8
     drop @6
+    drop @5
     drop iter@4
     drop @2
     @0 := ()
@@ -287,10 +278,6 @@ fn test_crate::select<'_0, '_1>(@1: &'_0 (Slice<u8>), @2: &'_1 (Slice<u8>))
     let @22: &'_ (usize); // anonymous local
     let @23: &'_ (usize); // anonymous local
     let @24: core::option::Option<core::fmt::Arguments<'_>>[core::marker::Sized<core::fmt::Arguments<'_>>]; // anonymous local
-    let @25: (); // anonymous local
-    let @26: (); // anonymous local
-    let @27: (); // anonymous local
-    let @28: (); // anonymous local
 
     @4 := const (false)
     if move (@4) {
@@ -328,8 +315,6 @@ fn test_crate::select<'_0, '_1>(@1: &'_0 (Slice<u8>), @2: &'_1 (Slice<u8>))
         }
         drop @17
         drop @16
-        @27 := ()
-        @5 := move (@27)
         drop @15
         drop right_val@14
         drop left_val@13
@@ -337,17 +322,12 @@ fn test_crate::select<'_0, '_1>(@1: &'_0 (Slice<u8>), @2: &'_1 (Slice<u8>))
         drop @8
         drop @6
         drop @5
-        @28 := ()
-        @3 := move (@28)
     }
     else {
-        @25 := ()
-        @3 := move (@25)
     }
     drop @4
     drop @3
-    @26 := ()
-    @0 := move (@26)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/issue-507-cfg.out b/charon/tests/ui/issue-507-cfg.out
index e39340ab6..731961a71 100644
--- a/charon/tests/ui/issue-507-cfg.out
+++ b/charon/tests/ui/issue-507-cfg.out
@@ -17,35 +17,25 @@ fn test_crate::f0()
     let @2: (); // anonymous local
     let @3: bool; // anonymous local
     let x@4: u8; // local
-    let @5: (); // anonymous local
-    let @6: (); // anonymous local
-    let @7: (); // anonymous local
-    let @8: u8; // anonymous local
-    let @9: (); // anonymous local
+    let @5: u8; // anonymous local
 
     @1 := const (0 : i32) < const (1 : i32)
     if move (@1) {
         @3 := const (0 : i32) < const (1 : i32)
         if move (@3) {
-            @6 := ()
-            @2 := move (@6)
         }
         else {
-            @7 := ()
-            @2 := move (@7)
         }
         drop @3
         drop @2
-        @8 := test_crate::CONST
-        x@4 := move (@8)
+        @5 := test_crate::CONST
+        x@4 := move (@5)
         @fake_read(x@4)
-        @9 := ()
-        @0 := move (@9)
+        @0 := ()
         drop x@4
     }
     else {
-        @5 := ()
-        @0 := move (@5)
+        @0 := ()
     }
     drop @1
     @0 := ()
@@ -58,91 +48,74 @@ fn test_crate::f1<'_0>(@1: &'_0 (Array<u8, 1 : usize>))
     let serialized@1: &'_ (Array<u8, 1 : usize>); // arg #1
     let previous_true_hints_seen@2: usize; // local
     let i@3: i32; // local
-    let @4: (); // anonymous local
-    let @5: bool; // anonymous local
-    let @6: i32; // anonymous local
-    let @7: (); // anonymous local
+    let @4: bool; // anonymous local
+    let @5: i32; // anonymous local
+    let @6: (); // anonymous local
+    let @7: bool; // anonymous local
     let @8: bool; // anonymous local
-    let @9: bool; // anonymous local
-    let j@10: i32; // local
-    let @11: bool; // anonymous local
-    let @12: i32; // anonymous local
-    let x@13: u8; // local
+    let j@9: i32; // local
+    let @10: bool; // anonymous local
+    let @11: i32; // anonymous local
+    let x@12: u8; // local
+    let @13: (); // anonymous local
     let @14: (); // anonymous local
-    let @15: (); // anonymous local
-    let @16: (); // anonymous local
-    let @17: (); // anonymous local
-    let @18: (); // anonymous local
-    let @19: u8; // anonymous local
-    let @20: (); // anonymous local
-    let @21: (); // anonymous local
+    let @15: u8; // anonymous local
 
     previous_true_hints_seen@2 := const (0 : usize)
     @fake_read(previous_true_hints_seen@2)
     i@3 := const (0 : i32)
     @fake_read(i@3)
     loop {
-        @6 := copy (i@3)
-        @5 := move (@6) < const (1 : i32)
-        if move (@5) {
-            drop @6
-            @8 := const (0 : i32) < const (1 : i32)
-            if move (@8) {
-                @17 := ()
-                @7 := move (@17)
+        @5 := copy (i@3)
+        @4 := move (@5) < const (1 : i32)
+        if move (@4) {
+            drop @5
+            @7 := const (0 : i32) < const (1 : i32)
+            if move (@7) {
             }
             else {
-                @9 := const (1 : i32) > const (1 : i32)
-                if move (@9) {
-                    @17 := ()
-                    @7 := move (@17)
+                @8 := const (1 : i32) > const (1 : i32)
+                if move (@8) {
                 }
                 else {
-                    @18 := ()
-                    @7 := move (@18)
                 }
             }
-            drop @9
             drop @8
             drop @7
-            j@10 := const (0 : i32)
-            @fake_read(j@10)
+            drop @6
+            j@9 := const (0 : i32)
+            @fake_read(j@9)
             loop {
-                @12 := copy (j@10)
-                @11 := move (@12) < const (1 : i32)
-                if move (@11) {
-                    drop @12
-                    @19 := test_crate::CONST
-                    x@13 := move (@19)
-                    @fake_read(x@13)
-                    @20 := ()
-                    @4 := move (@20)
-                    drop x@13
+                @11 := copy (j@9)
+                @10 := move (@11) < const (1 : i32)
+                if move (@10) {
                     drop @11
+                    @15 := test_crate::CONST
+                    x@12 := move (@15)
+                    @fake_read(x@12)
+                    drop x@12
+                    drop @10
                     continue 0
                 }
                 else {
                     break 0
                 }
             }
-            drop @12
-            @21 := ()
-            @4 := move (@21)
-            drop @14
             drop @11
-            drop j@10
-            drop @5
+            drop @13
+            drop @10
+            drop j@9
+            drop @4
             continue 0
         }
         else {
             break 0
         }
     }
-    drop @6
-    @16 := ()
-    @0 := move (@16)
-    drop @15
     drop @5
+    @0 := ()
+    drop @14
+    drop @4
     drop i@3
     drop previous_true_hints_seen@2
     @0 := ()
diff --git a/charon/tests/ui/issue-70-override-provided-method.2.out b/charon/tests/ui/issue-70-override-provided-method.2.out
index 05529a101..48be14cbb 100644
--- a/charon/tests/ui/issue-70-override-provided-method.2.out
+++ b/charon/tests/ui/issue-70-override-provided-method.2.out
@@ -15,14 +15,12 @@ fn test_crate::{impl test_crate::Trait for test_crate::Foo}::required<'_0>(@1: &
     let self@1: &'_ (test_crate::Foo); // arg #1
     let @2: (); // anonymous local
     let @3: &'_ (test_crate::Foo); // anonymous local
-    let @4: (); // anonymous local
 
     @3 := &*(self@1)
     @2 := test_crate::{impl test_crate::Trait for test_crate::Foo}::provided1<'_>(move (@3))
     drop @3
     drop @2
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     @0 := ()
     return
 }
@@ -35,7 +33,6 @@ fn test_crate::{impl test_crate::Trait for test_crate::Foo}::provided1<'_0>(@1:
     let @3: &'_ (test_crate::Foo); // anonymous local
     let @4: (); // anonymous local
     let @5: &'_ (test_crate::Foo); // anonymous local
-    let @6: (); // anonymous local
 
     @3 := &*(self@1)
     @2 := test_crate::{impl test_crate::Trait for test_crate::Foo}::required<'_>(move (@3))
@@ -45,8 +42,7 @@ fn test_crate::{impl test_crate::Trait for test_crate::Foo}::provided1<'_0>(@1:
     @4 := test_crate::{impl test_crate::Trait for test_crate::Foo}::provided2<'_>(move (@5))
     drop @5
     drop @4
-    @6 := ()
-    @0 := move (@6)
+    @0 := ()
     @0 := ()
     return
 }
@@ -59,7 +55,6 @@ fn test_crate::{impl test_crate::Trait for test_crate::Foo}::provided2<'_0>(@1:
     let @3: &'_ (test_crate::Foo); // anonymous local
     let @4: (); // anonymous local
     let @5: &'_ (test_crate::Foo); // anonymous local
-    let @6: (); // anonymous local
 
     @3 := &*(self@1)
     @2 := test_crate::{impl test_crate::Trait for test_crate::Foo}::required<'_>(move (@3))
@@ -69,8 +64,7 @@ fn test_crate::{impl test_crate::Trait for test_crate::Foo}::provided2<'_0>(@1:
     @4 := test_crate::{impl test_crate::Trait for test_crate::Foo}::provided1<'_>(move (@5))
     drop @5
     drop @4
-    @6 := ()
-    @0 := move (@6)
+    @0 := ()
     @0 := ()
     return
 }
@@ -90,14 +84,12 @@ fn test_crate::{impl test_crate::Trait for test_crate::Bar}#1::required<'_0>(@1:
     let self@1: &'_ (test_crate::Bar); // arg #1
     let @2: (); // anonymous local
     let @3: &'_ (test_crate::Bar); // anonymous local
-    let @4: (); // anonymous local
 
     @3 := &*(self@1)
     @2 := test_crate::{impl test_crate::Trait for test_crate::Bar}#1::provided2<'_>(move (@3))
     drop @3
     drop @2
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     @0 := ()
     return
 }
@@ -108,14 +100,12 @@ fn test_crate::{impl test_crate::Trait for test_crate::Bar}#1::provided1<'_0>(@1
     let self@1: &'_ (test_crate::Bar); // arg #1
     let @2: (); // anonymous local
     let @3: &'_ (test_crate::Bar); // anonymous local
-    let @4: (); // anonymous local
 
     @3 := &*(self@1)
     @2 := test_crate::{impl test_crate::Trait for test_crate::Bar}#1::provided2<'_>(move (@3))
     drop @3
     drop @2
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     @0 := ()
     return
 }
@@ -128,7 +118,6 @@ fn test_crate::{impl test_crate::Trait for test_crate::Bar}#1::provided2<'_0>(@1
     let @3: &'_ (test_crate::Bar); // anonymous local
     let @4: (); // anonymous local
     let @5: &'_ (test_crate::Bar); // anonymous local
-    let @6: (); // anonymous local
 
     @3 := &*(self@1)
     @2 := test_crate::{impl test_crate::Trait for test_crate::Bar}#1::required<'_>(move (@3))
@@ -138,8 +127,7 @@ fn test_crate::{impl test_crate::Trait for test_crate::Bar}#1::provided2<'_0>(@1
     @4 := test_crate::{impl test_crate::Trait for test_crate::Bar}#1::provided1<'_>(move (@5))
     drop @5
     drop @4
-    @6 := ()
-    @0 := move (@6)
+    @0 := ()
     @0 := ()
     return
 }
@@ -161,7 +149,6 @@ fn test_crate::Trait::provided1<'_0, Self>(@1: &'_0 (Self))
     let @3: &'_ (Self); // anonymous local
     let @4: (); // anonymous local
     let @5: &'_ (Self); // anonymous local
-    let @6: (); // anonymous local
 
     @3 := &*(self@1)
     @2 := Self::required<'_>(move (@3))
@@ -171,8 +158,7 @@ fn test_crate::Trait::provided1<'_0, Self>(@1: &'_0 (Self))
     @4 := Self::provided2<'_>(move (@5))
     drop @5
     drop @4
-    @6 := ()
-    @0 := move (@6)
+    @0 := ()
     @0 := ()
     return
 }
@@ -185,7 +171,6 @@ fn test_crate::Trait::provided2<'_0, Self>(@1: &'_0 (Self))
     let @3: &'_ (Self); // anonymous local
     let @4: (); // anonymous local
     let @5: &'_ (Self); // anonymous local
-    let @6: (); // anonymous local
 
     @3 := &*(self@1)
     @2 := Self::required<'_>(move (@3))
@@ -195,8 +180,7 @@ fn test_crate::Trait::provided2<'_0, Self>(@1: &'_0 (Self))
     @4 := Self::provided1<'_>(move (@5))
     drop @5
     drop @4
-    @6 := ()
-    @0 := move (@6)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/issue-70-override-provided-method.3.out b/charon/tests/ui/issue-70-override-provided-method.3.out
index 7887201c4..d4bb021c0 100644
--- a/charon/tests/ui/issue-70-override-provided-method.3.out
+++ b/charon/tests/ui/issue-70-override-provided-method.3.out
@@ -62,10 +62,8 @@ where
     [@TraitClause1]: core::marker::Copy<T>,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -85,7 +83,6 @@ where
     let @3: bool; // anonymous local
     let @4: &'_ (U); // anonymous local
     let @5: &'_ (core::option::Option<T>[@TraitClause0]); // anonymous local
-    let @6: (); // anonymous local
 
     @4 := &y@2
     @5 := &x@1
@@ -98,8 +95,7 @@ where
     else {
         drop @5
         drop @4
-        @6 := ()
-        @0 := move (@6)
+        @0 := ()
     }
     drop @3
     drop y@2
@@ -132,10 +128,8 @@ where
     [@TraitClause1]: core::marker::Copy<T>,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -153,7 +147,6 @@ where
     let @3: bool; // anonymous local
     let @4: &'_ (U); // anonymous local
     let @5: &'_ (core::option::Option<T>[@TraitClause0]); // anonymous local
-    let @6: (); // anonymous local
 
     @4 := &y@2
     @5 := &x@1
@@ -166,8 +159,7 @@ where
     else {
         drop @5
         drop @4
-        @6 := ()
-        @0 := move (@6)
+        @0 := ()
     }
     drop @3
     drop y@2
@@ -200,7 +192,6 @@ where
     let @3: bool; // anonymous local
     let @4: &'_ (U); // anonymous local
     let @5: &'_ (T); // anonymous local
-    let @6: (); // anonymous local
 
     @4 := &y@2
     @5 := &x@1
@@ -213,8 +204,7 @@ where
     else {
         drop @5
         drop @4
-        @6 := ()
-        @0 := move (@6)
+        @0 := ()
     }
     drop @3
     drop y@2
diff --git a/charon/tests/ui/issue-70-override-provided-method.out b/charon/tests/ui/issue-70-override-provided-method.out
index cd17f3290..7fa341ccb 100644
--- a/charon/tests/ui/issue-70-override-provided-method.out
+++ b/charon/tests/ui/issue-70-override-provided-method.out
@@ -35,7 +35,6 @@ fn test_crate::main()
     let @3: core::option::Option<i32>[core::marker::Sized<i32>]; // anonymous local
     let @4: &'_ (core::option::Option<i32>[core::marker::Sized<i32>]); // anonymous local
     let @5: core::option::Option<i32>[core::marker::Sized<i32>]; // anonymous local
-    let @6: (); // anonymous local
 
     @3 := core::option::Option::Some { 0: const (1 : i32) }
     @2 := &@3
@@ -48,8 +47,7 @@ fn test_crate::main()
     drop @5
     drop @3
     drop @1
-    @6 := ()
-    @0 := move (@6)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/issue-72-hash-missing-impl.out b/charon/tests/ui/issue-72-hash-missing-impl.out
index d8dcbcf52..64687d8b8 100644
--- a/charon/tests/ui/issue-72-hash-missing-impl.out
+++ b/charon/tests/ui/issue-72-hash-missing-impl.out
@@ -21,10 +21,8 @@ where
     let @0: (); // return
     let self@1: &'_ (u32); // arg #1
     let _state@2: &'_ mut (H); // arg #2
-    let @3: (); // anonymous local
 
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     @0 := ()
     return
 }
@@ -43,7 +41,6 @@ fn test_crate::main()
     let @4: u32; // anonymous local
     let @5: &'_ mut (test_crate::DefaultHasher); // anonymous local
     let @6: &'_ mut (test_crate::DefaultHasher); // anonymous local
-    let @7: (); // anonymous local
 
     hasher@1 := test_crate::DefaultHasher {  }
     @fake_read(hasher@1)
@@ -57,8 +54,7 @@ fn test_crate::main()
     drop @6
     drop @4
     drop @2
-    @7 := ()
-    @0 := move (@7)
+    @0 := ()
     drop hasher@1
     @0 := ()
     return
diff --git a/charon/tests/ui/issue-73-extern.out b/charon/tests/ui/issue-73-extern.out
index 8be29fbf3..868084e97 100644
--- a/charon/tests/ui/issue-73-extern.out
+++ b/charon/tests/ui/issue-73-extern.out
@@ -12,10 +12,8 @@ fn test_crate::use_type<'_0>(@1: &'_0 (test_crate::Type))
 {
     let @0: (); // return
     let _x@1: &'_ (test_crate::Type); // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out
index ba60901ce..bd62715e3 100644
--- a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out
+++ b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out
@@ -66,7 +66,6 @@ fn test_crate::main()
     let @17: bool; // anonymous local
     let @18: bool; // anonymous local
     let @19: bool; // anonymous local
-    let @20: (); // anonymous local
 
     x@1 := test_crate::Foo::A {  }
     @fake_read(x@1)
@@ -125,8 +124,7 @@ fn test_crate::main()
     drop @14
     @fake_read(@13)
     drop @13
-    @20 := ()
-    @0 := move (@20)
+    @0 := ()
     drop x@12
     drop x@1
     @0 := ()
diff --git a/charon/tests/ui/issue-92-nonpositive-variant-indices.out b/charon/tests/ui/issue-92-nonpositive-variant-indices.out
index 3a075428e..c255695eb 100644
--- a/charon/tests/ui/issue-92-nonpositive-variant-indices.out
+++ b/charon/tests/ui/issue-92-nonpositive-variant-indices.out
@@ -10,24 +10,18 @@ fn test_crate::main()
 {
     let @0: (); // return
     let @1: test_crate::Ordering; // anonymous local
-    let @2: (); // anonymous local
-    let @3: (); // anonymous local
-    let @4: (); // anonymous local
 
     @1 := test_crate::Ordering::Less {  }
     @fake_read(@1)
     match @1 {
         0 => {
-            @2 := ()
-            @0 := move (@2)
+            @0 := ()
         },
         1 => {
-            @3 := ()
-            @0 := move (@3)
+            @0 := ()
         },
         2 => {
-            @4 := ()
-            @0 := move (@4)
+            @0 := ()
         },
     }
     drop @1
diff --git a/charon/tests/ui/issue-97-missing-parent-item-clause.out b/charon/tests/ui/issue-97-missing-parent-item-clause.out
index f0a2c8ed5..8338c4761 100644
--- a/charon/tests/ui/issue-97-missing-parent-item-clause.out
+++ b/charon/tests/ui/issue-97-missing-parent-item-clause.out
@@ -31,14 +31,12 @@ fn test_crate::test(@1: test_crate::AVLTree<u32>[core::marker::Sized<u32>])
     let tree@1: test_crate::AVLTree<u32>[core::marker::Sized<u32>]; // arg #1
     let @2: (); // anonymous local
     let @3: &'_ mut (test_crate::AVLTree<u32>[core::marker::Sized<u32>]); // anonymous local
-    let @4: (); // anonymous local
 
     @3 := &two-phase-mut tree@1
     @2 := test_crate::{test_crate::AVLTree<T>[@TraitClause0]}::insert<'_, u32>[core::marker::Sized<u32>, test_crate::{impl test_crate::Ord for u32}#1](move (@3))
     drop @3
     drop @2
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/iterator.out b/charon/tests/ui/iterator.out
index 3bf68db53..d5c366319 100644
--- a/charon/tests/ui/iterator.out
+++ b/charon/tests/ui/iterator.out
@@ -3280,77 +3280,62 @@ fn test_crate::main()
     let @6: Array<i32, 7 : usize>; // anonymous local
     let iter@7: core::array::iter::IntoIter<i32, 7 : usize>[core::marker::Sized<i32>]; // local
     let @8: (); // anonymous local
-    let @9: (); // anonymous local
-    let @10: core::option::Option<i32>[core::marker::Sized<i32>]; // anonymous local
+    let @9: core::option::Option<i32>[core::marker::Sized<i32>]; // anonymous local
+    let @10: &'_ mut (core::array::iter::IntoIter<i32, 7 : usize>[core::marker::Sized<i32>]); // anonymous local
     let @11: &'_ mut (core::array::iter::IntoIter<i32, 7 : usize>[core::marker::Sized<i32>]); // anonymous local
-    let @12: &'_ mut (core::array::iter::IntoIter<i32, 7 : usize>[core::marker::Sized<i32>]); // anonymous local
-    let v@13: i32; // local
-    let @14: i32; // anonymous local
-    let @15: (); // anonymous local
+    let v@12: i32; // local
+    let @13: i32; // anonymous local
+    let @14: (); // anonymous local
+    let @15: core::slice::iter::Iter<'_, i32>[core::marker::Sized<i32>]; // anonymous local
     let @16: core::slice::iter::Iter<'_, i32>[core::marker::Sized<i32>]; // anonymous local
-    let @17: core::slice::iter::Iter<'_, i32>[core::marker::Sized<i32>]; // anonymous local
-    let @18: &'_ (Slice<i32>); // anonymous local
-    let @19: &'_ (Array<i32, 7 : usize>); // anonymous local
-    let iter@20: core::slice::iter::Iter<'_, i32>[core::marker::Sized<i32>]; // local
-    let @21: (); // anonymous local
-    let @22: core::option::Option<&'_ (i32)>[core::marker::Sized<&'_ (i32)>]; // anonymous local
+    let @17: &'_ (Slice<i32>); // anonymous local
+    let @18: &'_ (Array<i32, 7 : usize>); // anonymous local
+    let iter@19: core::slice::iter::Iter<'_, i32>[core::marker::Sized<i32>]; // local
+    let @20: (); // anonymous local
+    let @21: core::option::Option<&'_ (i32)>[core::marker::Sized<&'_ (i32)>]; // anonymous local
+    let @22: &'_ mut (core::slice::iter::Iter<'_, i32>[core::marker::Sized<i32>]); // anonymous local
     let @23: &'_ mut (core::slice::iter::Iter<'_, i32>[core::marker::Sized<i32>]); // anonymous local
-    let @24: &'_ mut (core::slice::iter::Iter<'_, i32>[core::marker::Sized<i32>]); // anonymous local
-    let v@25: &'_ (i32); // local
-    let @26: (); // anonymous local
-    let @27: &'_ mut (i32); // anonymous local
-    let @28: &'_ (i32); // anonymous local
-    let @29: (); // anonymous local
+    let v@24: &'_ (i32); // local
+    let @25: (); // anonymous local
+    let @26: &'_ mut (i32); // anonymous local
+    let @27: &'_ (i32); // anonymous local
+    let @28: (); // anonymous local
+    let @29: core::slice::iter::Chunks<'_, i32>[core::marker::Sized<i32>]; // anonymous local
     let @30: core::slice::iter::Chunks<'_, i32>[core::marker::Sized<i32>]; // anonymous local
-    let @31: core::slice::iter::Chunks<'_, i32>[core::marker::Sized<i32>]; // anonymous local
-    let @32: &'_ (Slice<i32>); // anonymous local
-    let @33: &'_ (Array<i32, 7 : usize>); // anonymous local
-    let iter@34: core::slice::iter::Chunks<'_, i32>[core::marker::Sized<i32>]; // local
-    let @35: (); // anonymous local
-    let @36: core::option::Option<&'_ (Slice<i32>)>[core::marker::Sized<&'_ (Slice<i32>)>]; // anonymous local
+    let @31: &'_ (Slice<i32>); // anonymous local
+    let @32: &'_ (Array<i32, 7 : usize>); // anonymous local
+    let iter@33: core::slice::iter::Chunks<'_, i32>[core::marker::Sized<i32>]; // local
+    let @34: (); // anonymous local
+    let @35: core::option::Option<&'_ (Slice<i32>)>[core::marker::Sized<&'_ (Slice<i32>)>]; // anonymous local
+    let @36: &'_ mut (core::slice::iter::Chunks<'_, i32>[core::marker::Sized<i32>]); // anonymous local
     let @37: &'_ mut (core::slice::iter::Chunks<'_, i32>[core::marker::Sized<i32>]); // anonymous local
-    let @38: &'_ mut (core::slice::iter::Chunks<'_, i32>[core::marker::Sized<i32>]); // anonymous local
-    let @39: (); // anonymous local
+    let @38: (); // anonymous local
+    let @39: core::slice::iter::ChunksExact<'_, i32>[core::marker::Sized<i32>]; // anonymous local
     let @40: core::slice::iter::ChunksExact<'_, i32>[core::marker::Sized<i32>]; // anonymous local
-    let @41: core::slice::iter::ChunksExact<'_, i32>[core::marker::Sized<i32>]; // anonymous local
-    let @42: &'_ (Slice<i32>); // anonymous local
-    let @43: &'_ (Array<i32, 7 : usize>); // anonymous local
-    let iter@44: core::slice::iter::ChunksExact<'_, i32>[core::marker::Sized<i32>]; // local
-    let @45: (); // anonymous local
-    let @46: core::option::Option<&'_ (Slice<i32>)>[core::marker::Sized<&'_ (Slice<i32>)>]; // anonymous local
+    let @41: &'_ (Slice<i32>); // anonymous local
+    let @42: &'_ (Array<i32, 7 : usize>); // anonymous local
+    let iter@43: core::slice::iter::ChunksExact<'_, i32>[core::marker::Sized<i32>]; // local
+    let @44: (); // anonymous local
+    let @45: core::option::Option<&'_ (Slice<i32>)>[core::marker::Sized<&'_ (Slice<i32>)>]; // anonymous local
+    let @46: &'_ mut (core::slice::iter::ChunksExact<'_, i32>[core::marker::Sized<i32>]); // anonymous local
     let @47: &'_ mut (core::slice::iter::ChunksExact<'_, i32>[core::marker::Sized<i32>]); // anonymous local
-    let @48: &'_ mut (core::slice::iter::ChunksExact<'_, i32>[core::marker::Sized<i32>]); // anonymous local
-    let expected@49: i32; // local
-    let @50: (); // anonymous local
-    let @51: (&'_ (i32), &'_ (i32)); // anonymous local
+    let expected@48: i32; // local
+    let @49: (); // anonymous local
+    let @50: (&'_ (i32), &'_ (i32)); // anonymous local
+    let @51: &'_ (i32); // anonymous local
     let @52: &'_ (i32); // anonymous local
-    let @53: &'_ (i32); // anonymous local
-    let left_val@54: &'_ (i32); // local
-    let right_val@55: &'_ (i32); // local
-    let @56: bool; // anonymous local
+    let left_val@53: &'_ (i32); // local
+    let right_val@54: &'_ (i32); // local
+    let @55: bool; // anonymous local
+    let @56: i32; // anonymous local
     let @57: i32; // anonymous local
-    let @58: i32; // anonymous local
-    let kind@59: core::panicking::AssertKind; // local
-    let @60: core::panicking::AssertKind; // anonymous local
+    let kind@58: core::panicking::AssertKind; // local
+    let @59: core::panicking::AssertKind; // anonymous local
+    let @60: &'_ (i32); // anonymous local
     let @61: &'_ (i32); // anonymous local
     let @62: &'_ (i32); // anonymous local
     let @63: &'_ (i32); // anonymous local
-    let @64: &'_ (i32); // anonymous local
-    let @65: core::option::Option<core::fmt::Arguments<'_>>[core::marker::Sized<core::fmt::Arguments<'_>>]; // anonymous local
-    let @66: (); // anonymous local
-    let @67: (); // anonymous local
-    let @68: (); // anonymous local
-    let @69: (); // anonymous local
-    let @70: (); // anonymous local
-    let @71: (); // anonymous local
-    let @72: (); // anonymous local
-    let @73: (); // anonymous local
-    let @74: (); // anonymous local
-    let @75: (); // anonymous local
-    let @76: (); // anonymous local
-    let @77: (); // anonymous local
-    let @78: (); // anonymous local
-    let @79: (); // anonymous local
+    let @64: core::option::Option<core::fmt::Arguments<'_>>[core::marker::Sized<core::fmt::Arguments<'_>>]; // anonymous local
 
     a@1 := [const (0 : i32), const (1 : i32), const (2 : i32), const (3 : i32), const (4 : i32), const (5 : i32), const (6 : i32); 7 : usize]
     @fake_read(a@1)
@@ -3364,209 +3349,182 @@ fn test_crate::main()
     @fake_read(@4)
     iter@7 := move (@4)
     loop {
-        @12 := &mut iter@7
-        @11 := &two-phase-mut *(@12)
-        @10 := core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::next<'_, i32, 7 : usize>[core::marker::Sized<i32>](move (@11))
-        drop @11
-        @fake_read(@10)
-        match @10 {
+        @11 := &mut iter@7
+        @10 := &two-phase-mut *(@11)
+        @9 := core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::next<'_, i32, 7 : usize>[core::marker::Sized<i32>](move (@10))
+        drop @10
+        @fake_read(@9)
+        match @9 {
             0 => {
                 break 0
             },
             1 => {
-                v@13 := copy ((@10 as variant @1).0)
-                @14 := copy (v@13)
-                i@2 := copy (i@2) + move (@14)
-                drop @14
-                @67 := ()
-                @9 := move (@67)
-                drop v@13
-                drop @12
-                drop @10
+                v@12 := copy ((@9 as variant @1).0)
+                @13 := copy (v@12)
+                i@2 := copy (i@2) + move (@13)
+                drop @13
+                drop v@12
+                drop @11
                 drop @9
-                @68 := ()
-                @8 := move (@68)
+                drop @8
                 continue 0
             },
         }
     }
-    @66 := ()
-    @3 := move (@66)
-    drop @12
-    drop @10
+    drop @11
     drop @9
+    drop @8
     drop iter@7
     drop iter@7
     drop @4
     drop @4
     drop @3
-    @19 := &a@1
-    @18 := @ArrayToSliceShared<'_, i32, 7 : usize>(move (@19))
-    drop @19
-    @17 := core::slice::{Slice<T>}::iter<'_, i32>[core::marker::Sized<i32>](move (@18))
+    @18 := &a@1
+    @17 := @ArrayToSliceShared<'_, i32, 7 : usize>(move (@18))
     drop @18
-    @16 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::slice::iter::Iter<'_, i32>[core::marker::Sized<i32>]>[core::marker::Sized<core::slice::iter::Iter<'_, i32>[core::marker::Sized<i32>]>, core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182<'_, i32>[core::marker::Sized<i32>]](move (@17))
+    @16 := core::slice::{Slice<T>}::iter<'_, i32>[core::marker::Sized<i32>](move (@17))
     drop @17
-    @fake_read(@16)
-    iter@20 := move (@16)
+    @15 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::slice::iter::Iter<'_, i32>[core::marker::Sized<i32>]>[core::marker::Sized<core::slice::iter::Iter<'_, i32>[core::marker::Sized<i32>]>, core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182<'_, i32>[core::marker::Sized<i32>]](move (@16))
+    drop @16
+    @fake_read(@15)
+    iter@19 := move (@15)
     loop {
-        @24 := &mut iter@20
-        @23 := &two-phase-mut *(@24)
-        @22 := core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::next<'_, '_, i32>[core::marker::Sized<i32>](move (@23))
-        drop @23
-        @fake_read(@22)
-        match @22 {
+        @23 := &mut iter@19
+        @22 := &two-phase-mut *(@23)
+        @21 := core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::next<'_, '_, i32>[core::marker::Sized<i32>](move (@22))
+        drop @22
+        @fake_read(@21)
+        match @21 {
             0 => {
                 break 0
             },
             1 => {
-                v@25 := copy ((@22 as variant @1).0)
-                @27 := &two-phase-mut i@2
-                @28 := copy (v@25)
-                @26 := core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i32}#365::add_assign<'_, '_>(move (@27), move (@28))
-                drop @28
+                v@24 := copy ((@21 as variant @1).0)
+                @26 := &two-phase-mut i@2
+                @27 := copy (v@24)
+                @25 := core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i32}#365::add_assign<'_, '_>(move (@26), move (@27))
                 drop @27
                 drop @26
-                @70 := ()
-                @21 := move (@70)
-                drop v@25
-                drop @24
-                drop @22
+                drop @25
+                drop v@24
+                drop @23
                 drop @21
-                @71 := ()
-                @8 := move (@71)
+                drop @20
                 continue 0
             },
         }
     }
-    @69 := ()
-    @15 := move (@69)
-    drop @24
-    drop @22
+    drop @23
     drop @21
-    drop iter@20
-    drop @16
+    drop @20
+    drop iter@19
     drop @15
-    @33 := &a@1
-    @32 := @ArrayToSliceShared<'_, i32, 7 : usize>(move (@33))
-    drop @33
-    @31 := core::slice::{Slice<T>}::chunks<'_, i32>[core::marker::Sized<i32>](move (@32), const (2 : usize))
+    drop @14
+    @32 := &a@1
+    @31 := @ArrayToSliceShared<'_, i32, 7 : usize>(move (@32))
     drop @32
-    @30 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::slice::iter::Chunks<'_, i32>[core::marker::Sized<i32>]>[core::marker::Sized<core::slice::iter::Chunks<'_, i32>[core::marker::Sized<i32>]>, core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71<'_, i32>[core::marker::Sized<i32>]](move (@31))
+    @30 := core::slice::{Slice<T>}::chunks<'_, i32>[core::marker::Sized<i32>](move (@31), const (2 : usize))
     drop @31
-    @fake_read(@30)
-    iter@34 := move (@30)
+    @29 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::slice::iter::Chunks<'_, i32>[core::marker::Sized<i32>]>[core::marker::Sized<core::slice::iter::Chunks<'_, i32>[core::marker::Sized<i32>]>, core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71<'_, i32>[core::marker::Sized<i32>]](move (@30))
+    drop @30
+    @fake_read(@29)
+    iter@33 := move (@29)
     loop {
-        @38 := &mut iter@34
-        @37 := &two-phase-mut *(@38)
-        @36 := core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::next<'_, '_, i32>[core::marker::Sized<i32>](move (@37))
-        drop @37
-        @fake_read(@36)
-        match @36 {
+        @37 := &mut iter@33
+        @36 := &two-phase-mut *(@37)
+        @35 := core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::next<'_, '_, i32>[core::marker::Sized<i32>](move (@36))
+        drop @36
+        @fake_read(@35)
+        match @35 {
             0 => {
                 break 0
             },
             1 => {
                 i@2 := copy (i@2) + const (1 : i32)
-                @73 := ()
-                @35 := move (@73)
-                drop @38
-                drop @36
+                drop @37
                 drop @35
-                @74 := ()
-                @8 := move (@74)
+                drop @34
                 continue 0
             },
         }
     }
-    @72 := ()
-    @29 := move (@72)
-    drop @38
-    drop @36
+    drop @37
     drop @35
-    drop iter@34
-    drop @30
+    drop @34
+    drop iter@33
     drop @29
-    @43 := &a@1
-    @42 := @ArrayToSliceShared<'_, i32, 7 : usize>(move (@43))
-    drop @43
-    @41 := core::slice::{Slice<T>}::chunks_exact<'_, i32>[core::marker::Sized<i32>](move (@42), const (2 : usize))
+    drop @28
+    @42 := &a@1
+    @41 := @ArrayToSliceShared<'_, i32, 7 : usize>(move (@42))
     drop @42
-    @40 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::slice::iter::ChunksExact<'_, i32>[core::marker::Sized<i32>]>[core::marker::Sized<core::slice::iter::ChunksExact<'_, i32>[core::marker::Sized<i32>]>, core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90<'_, i32>[core::marker::Sized<i32>]](move (@41))
+    @40 := core::slice::{Slice<T>}::chunks_exact<'_, i32>[core::marker::Sized<i32>](move (@41), const (2 : usize))
     drop @41
-    @fake_read(@40)
-    iter@44 := move (@40)
+    @39 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::slice::iter::ChunksExact<'_, i32>[core::marker::Sized<i32>]>[core::marker::Sized<core::slice::iter::ChunksExact<'_, i32>[core::marker::Sized<i32>]>, core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90<'_, i32>[core::marker::Sized<i32>]](move (@40))
+    drop @40
+    @fake_read(@39)
+    iter@43 := move (@39)
     loop {
-        @48 := &mut iter@44
-        @47 := &two-phase-mut *(@48)
-        @46 := core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::next<'_, '_, i32>[core::marker::Sized<i32>](move (@47))
-        drop @47
-        @fake_read(@46)
-        match @46 {
+        @47 := &mut iter@43
+        @46 := &two-phase-mut *(@47)
+        @45 := core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::next<'_, '_, i32>[core::marker::Sized<i32>](move (@46))
+        drop @46
+        @fake_read(@45)
+        match @45 {
             0 => {
                 break 0
             },
             1 => {
                 i@2 := copy (i@2) + const (1 : i32)
-                @76 := ()
-                @45 := move (@76)
-                drop @48
-                drop @46
+                drop @47
                 drop @45
-                @77 := ()
-                @8 := move (@77)
+                drop @44
                 continue 0
             },
         }
     }
-    @75 := ()
-    @39 := move (@75)
-    drop @48
-    drop @46
+    drop @47
     drop @45
-    drop iter@44
-    drop @40
+    drop @44
+    drop iter@43
     drop @39
-    expected@49 := const (28 : i32)
-    @fake_read(expected@49)
-    @52 := &i@2
-    @53 := &expected@49
-    @51 := (move (@52), move (@53))
-    drop @53
+    drop @38
+    expected@48 := const (28 : i32)
+    @fake_read(expected@48)
+    @51 := &i@2
+    @52 := &expected@48
+    @50 := (move (@51), move (@52))
     drop @52
-    @fake_read(@51)
-    left_val@54 := copy ((@51).0)
-    right_val@55 := copy ((@51).1)
-    @57 := copy (*(left_val@54))
-    @58 := copy (*(right_val@55))
-    @56 := move (@57) == move (@58)
-    if move (@56) {
+    drop @51
+    @fake_read(@50)
+    left_val@53 := copy ((@50).0)
+    right_val@54 := copy ((@50).1)
+    @56 := copy (*(left_val@53))
+    @57 := copy (*(right_val@54))
+    @55 := move (@56) == move (@57)
+    if move (@55) {
     }
     else {
-        drop @58
         drop @57
-        kind@59 := core::panicking::AssertKind::Eq {  }
-        @fake_read(kind@59)
-        @60 := move (kind@59)
-        @62 := &*(left_val@54)
-        @61 := &*(@62)
-        @64 := &*(right_val@55)
-        @63 := &*(@64)
-        @65 := core::option::Option::None {  }
+        drop @56
+        kind@58 := core::panicking::AssertKind::Eq {  }
+        @fake_read(kind@58)
+        @59 := move (kind@58)
+        @61 := &*(left_val@53)
+        @60 := &*(@61)
+        @63 := &*(right_val@54)
+        @62 := &*(@63)
+        @64 := core::option::Option::None {  }
         panic(core::panicking::assert_failed)
     }
-    drop @58
     drop @57
-    @78 := ()
-    @50 := move (@78)
     drop @56
-    drop right_val@55
-    drop left_val@54
-    drop @51
+    drop @55
+    drop right_val@54
+    drop left_val@53
     drop @50
-    @79 := ()
-    @0 := move (@79)
-    drop expected@49
+    drop @49
+    @0 := ()
+    drop expected@48
     drop i@2
     drop a@1
     @0 := ()
diff --git a/charon/tests/ui/loops.out b/charon/tests/ui/loops.out
index 206ce4512..a07afdf6f 100644
--- a/charon/tests/ui/loops.out
+++ b/charon/tests/ui/loops.out
@@ -7,45 +7,38 @@ fn test_crate::test_loop1(@1: u32) -> u32
     let i@2: u32; // local
     let s@3: u32; // local
     let @4: (); // anonymous local
-    let @5: (); // anonymous local
-    let @6: bool; // anonymous local
+    let @5: bool; // anonymous local
+    let @6: u32; // anonymous local
     let @7: u32; // anonymous local
     let @8: u32; // anonymous local
-    let @9: u32; // anonymous local
-    let @10: (); // anonymous local
-    let @11: (); // anonymous local
-    let @12: (); // anonymous local
+    let @9: (); // anonymous local
 
     i@2 := const (0 : u32)
     @fake_read(i@2)
     s@3 := const (0 : u32)
     @fake_read(s@3)
     loop {
-        @7 := copy (i@2)
-        @8 := copy (max@1)
-        @6 := move (@7) < move (@8)
-        if move (@6) {
-            drop @8
+        @6 := copy (i@2)
+        @7 := copy (max@1)
+        @5 := move (@6) < move (@7)
+        if move (@5) {
             drop @7
-            @9 := copy (i@2)
-            s@3 := copy (s@3) + move (@9)
-            drop @9
-            i@2 := copy (i@2) + const (1 : u32)
-            @11 := ()
-            @5 := move (@11)
             drop @6
+            @8 := copy (i@2)
+            s@3 := copy (s@3) + move (@8)
+            drop @8
+            i@2 := copy (i@2) + const (1 : u32)
+            drop @5
             continue 0
         }
         else {
             break 0
         }
     }
-    drop @8
     drop @7
-    @12 := ()
-    @4 := move (@12)
-    drop @10
     drop @6
+    drop @9
+    drop @5
     drop @4
     s@3 := copy (s@3) * const (2 : u32)
     @0 := copy (s@3)
@@ -61,67 +54,54 @@ fn test_crate::test_loop2(@1: u32) -> u32
     let i@2: u32; // local
     let s@3: u32; // local
     let @4: (); // anonymous local
-    let @5: (); // anonymous local
-    let @6: bool; // anonymous local
+    let @5: bool; // anonymous local
+    let @6: u32; // anonymous local
     let @7: u32; // anonymous local
-    let @8: u32; // anonymous local
-    let @9: (); // anonymous local
-    let @10: bool; // anonymous local
+    let @8: (); // anonymous local
+    let @9: bool; // anonymous local
+    let @10: u32; // anonymous local
     let @11: u32; // anonymous local
-    let @12: u32; // anonymous local
-    let @13: (); // anonymous local
-    let @14: (); // anonymous local
-    let @15: (); // anonymous local
-    let @16: (); // anonymous local
-    let @17: (); // anonymous local
+    let @12: (); // anonymous local
 
     i@2 := const (0 : u32)
     @fake_read(i@2)
     s@3 := const (0 : u32)
     @fake_read(s@3)
     loop {
-        @7 := copy (i@2)
-        @8 := copy (max@1)
-        @6 := move (@7) < move (@8)
-        if move (@6) {
-            drop @8
+        @6 := copy (i@2)
+        @7 := copy (max@1)
+        @5 := move (@6) < move (@7)
+        if move (@5) {
             drop @7
-            @11 := copy (i@2)
-            @10 := move (@11) == const (17 : u32)
-            if move (@10) {
+            drop @6
+            @10 := copy (i@2)
+            @9 := move (@10) == const (17 : u32)
+            if move (@9) {
             }
             else {
-                drop @11
-                @16 := ()
-                @9 := move (@16)
                 drop @10
                 drop @9
-                @12 := copy (i@2)
-                s@3 := copy (s@3) + move (@12)
-                drop @12
+                drop @8
+                @11 := copy (i@2)
+                s@3 := copy (s@3) + move (@11)
+                drop @11
                 i@2 := copy (i@2) + const (1 : u32)
-                @17 := ()
-                @5 := move (@17)
-                drop @6
+                drop @5
                 continue 0
             }
-            drop @11
-            @15 := ()
-            @4 := move (@15)
             drop @10
             drop @9
+            drop @8
             break 0
         }
         else {
-            drop @8
             drop @7
-            @14 := ()
-            @4 := move (@14)
-            drop @13
+            drop @6
+            drop @12
             break 0
         }
     }
-    drop @6
+    drop @5
     drop @4
     @0 := copy (s@3)
     drop s@3
@@ -137,27 +117,22 @@ fn test_crate::test_loop3(@1: u32) -> u32
     let j@3: u32; // local
     let s@4: u32; // local
     let @5: (); // anonymous local
-    let @6: (); // anonymous local
-    let @7: bool; // anonymous local
+    let @6: bool; // anonymous local
+    let @7: u32; // anonymous local
     let @8: u32; // anonymous local
-    let @9: u32; // anonymous local
-    let @10: (); // anonymous local
-    let @11: bool; // anonymous local
+    let @9: (); // anonymous local
+    let @10: bool; // anonymous local
+    let @11: u32; // anonymous local
     let @12: u32; // anonymous local
-    let @13: u32; // anonymous local
-    let @14: (); // anonymous local
-    let @15: bool; // anonymous local
+    let @13: (); // anonymous local
+    let @14: bool; // anonymous local
+    let @15: u32; // anonymous local
     let @16: u32; // anonymous local
     let @17: u32; // anonymous local
     let @18: u32; // anonymous local
-    let @19: u32; // anonymous local
-    let @20: (); // anonymous local
-    let @21: u32; // anonymous local
-    let @22: (); // anonymous local
-    let @23: (); // anonymous local
-    let @24: (); // anonymous local
-    let @25: (); // anonymous local
-    let @26: (); // anonymous local
+    let @19: (); // anonymous local
+    let @20: u32; // anonymous local
+    let @21: (); // anonymous local
 
     i@2 := const (0 : u32)
     @fake_read(i@2)
@@ -166,79 +141,71 @@ fn test_crate::test_loop3(@1: u32) -> u32
     s@4 := const (0 : u32)
     @fake_read(s@4)
     loop {
-        @8 := copy (i@2)
-        @9 := copy (max@1)
-        @7 := move (@8) < move (@9)
-        if move (@7) {
-            drop @9
+        @7 := copy (i@2)
+        @8 := copy (max@1)
+        @6 := move (@7) < move (@8)
+        if move (@6) {
             drop @8
+            drop @7
             loop {
-                @12 := copy (j@3)
-                @13 := copy (max@1)
-                @11 := move (@12) < move (@13)
-                if move (@11) {
-                    drop @13
+                @11 := copy (j@3)
+                @12 := copy (max@1)
+                @10 := move (@11) < move (@12)
+                if move (@10) {
                     drop @12
-                    @17 := copy (i@2)
-                    @18 := copy (j@3)
-                    @16 := move (@17) + move (@18)
-                    drop @18
+                    drop @11
+                    @16 := copy (i@2)
+                    @17 := copy (j@3)
+                    @15 := move (@16) + move (@17)
                     drop @17
-                    @15 := move (@16) == const (17 : u32)
-                    if move (@15) {
+                    drop @16
+                    @14 := move (@15) == const (17 : u32)
+                    if move (@14) {
                     }
                     else {
-                        drop @16
-                        @26 := ()
-                        @14 := move (@26)
                         drop @15
                         drop @14
-                        @19 := copy (i@2)
-                        s@4 := copy (s@4) + move (@19)
-                        drop @19
+                        drop @13
+                        @18 := copy (i@2)
+                        s@4 := copy (s@4) + move (@18)
+                        drop @18
                         j@3 := copy (j@3) + const (1 : u32)
-                        drop @11
                         drop @10
-                        drop @7
+                        drop @9
+                        drop @6
                         continue 1
                     }
-                    drop @16
                     drop @15
                     drop @14
-                    drop @11
+                    drop @13
+                    drop @10
                     continue 0
                 }
                 else {
                     break 0
                 }
             }
-            drop @13
             drop @12
-            @24 := ()
-            @10 := move (@24)
-            drop @20
             drop @11
+            drop @19
             drop @10
+            drop @9
             j@3 := const (0 : u32)
-            @21 := copy (i@2)
-            s@4 := copy (s@4) + move (@21)
-            drop @21
+            @20 := copy (i@2)
+            s@4 := copy (s@4) + move (@20)
+            drop @20
             i@2 := copy (i@2) + const (1 : u32)
-            @25 := ()
-            @6 := move (@25)
-            drop @7
+            drop @6
             continue 0
         }
         else {
             break 0
         }
     }
-    drop @9
     drop @8
-    @23 := ()
-    @5 := move (@23)
-    drop @22
     drop @7
+    drop @21
+    drop @6
     drop @5
     @0 := copy (s@4)
     drop s@4
@@ -255,28 +222,22 @@ fn test_crate::test_loop4(@1: u32) -> u32
     let j@3: u32; // local
     let s@4: u32; // local
     let @5: (); // anonymous local
-    let @6: (); // anonymous local
-    let @7: bool; // anonymous local
+    let @6: bool; // anonymous local
+    let @7: u32; // anonymous local
     let @8: u32; // anonymous local
-    let @9: u32; // anonymous local
-    let @10: (); // anonymous local
-    let @11: bool; // anonymous local
+    let @9: (); // anonymous local
+    let @10: bool; // anonymous local
+    let @11: u32; // anonymous local
     let @12: u32; // anonymous local
-    let @13: u32; // anonymous local
-    let @14: (); // anonymous local
-    let @15: bool; // anonymous local
+    let @13: (); // anonymous local
+    let @14: bool; // anonymous local
+    let @15: u32; // anonymous local
     let @16: u32; // anonymous local
     let @17: u32; // anonymous local
     let @18: u32; // anonymous local
-    let @19: u32; // anonymous local
-    let @20: (); // anonymous local
-    let @21: u32; // anonymous local
-    let @22: (); // anonymous local
-    let @23: (); // anonymous local
-    let @24: (); // anonymous local
-    let @25: (); // anonymous local
-    let @26: (); // anonymous local
-    let @27: (); // anonymous local
+    let @19: (); // anonymous local
+    let @20: u32; // anonymous local
+    let @21: (); // anonymous local
 
     i@2 := const (1 : u32)
     @fake_read(i@2)
@@ -285,46 +246,42 @@ fn test_crate::test_loop4(@1: u32) -> u32
     s@4 := const (0 : u32)
     @fake_read(s@4)
     loop {
-        @8 := copy (i@2)
-        @9 := copy (max@1)
-        @7 := move (@8) < move (@9)
-        if move (@7) {
-            drop @9
+        @7 := copy (i@2)
+        @8 := copy (max@1)
+        @6 := move (@7) < move (@8)
+        if move (@6) {
             drop @8
+            drop @7
             loop {
-                @12 := copy (j@3)
-                @13 := copy (max@1)
-                @11 := move (@12) < move (@13)
-                if move (@11) {
-                    drop @13
+                @11 := copy (j@3)
+                @12 := copy (max@1)
+                @10 := move (@11) < move (@12)
+                if move (@10) {
                     drop @12
-                    @17 := copy (i@2)
-                    @18 := copy (j@3)
-                    @16 := move (@17) + move (@18)
-                    drop @18
+                    drop @11
+                    @16 := copy (i@2)
+                    @17 := copy (j@3)
+                    @15 := move (@16) + move (@17)
                     drop @17
-                    @15 := move (@16) == const (17 : u32)
-                    if move (@15) {
-                        drop @16
+                    drop @16
+                    @14 := move (@15) == const (17 : u32)
+                    if move (@14) {
                         drop @15
                         drop @14
-                        drop @11
+                        drop @13
+                        drop @10
                         continue 0
                     }
                     else {
-                        drop @16
-                        @26 := ()
-                        @14 := move (@26)
                         drop @15
                         drop @14
-                        @19 := copy (i@2)
-                        s@4 := copy (s@4) + move (@19)
-                        drop @19
+                        drop @13
+                        @18 := copy (i@2)
+                        s@4 := copy (s@4) + move (@18)
+                        drop @18
                         j@3 := copy (j@3) + const (1 : u32)
-                        @27 := ()
-                        @5 := move (@27)
-                        drop @11
                         drop @10
+                        drop @9
                         break 1
                     }
                 }
@@ -332,33 +289,27 @@ fn test_crate::test_loop4(@1: u32) -> u32
                     break 0
                 }
             }
-            drop @13
             drop @12
-            @24 := ()
-            @10 := move (@24)
-            drop @20
             drop @11
+            drop @19
             drop @10
+            drop @9
             j@3 := const (0 : u32)
-            @21 := copy (i@2)
-            s@4 := copy (s@4) + move (@21)
-            drop @21
+            @20 := copy (i@2)
+            s@4 := copy (s@4) + move (@20)
+            drop @20
             i@2 := copy (i@2) + const (1 : u32)
-            @25 := ()
-            @6 := move (@25)
-            drop @7
+            drop @6
             continue 0
         }
         else {
-            drop @9
             drop @8
-            @23 := ()
-            @5 := move (@23)
-            drop @22
+            drop @7
+            drop @21
             break 0
         }
     }
-    drop @7
+    drop @6
     drop @5
     @0 := copy (s@4)
     drop s@4
@@ -375,22 +326,17 @@ fn test_crate::test_loop5(@1: u32) -> u32
     let j@3: u32; // local
     let s@4: u32; // local
     let @5: (); // anonymous local
-    let @6: (); // anonymous local
-    let @7: bool; // anonymous local
+    let @6: bool; // anonymous local
+    let @7: u32; // anonymous local
     let @8: u32; // anonymous local
-    let @9: u32; // anonymous local
-    let @10: (); // anonymous local
-    let @11: bool; // anonymous local
+    let @9: (); // anonymous local
+    let @10: bool; // anonymous local
+    let @11: u32; // anonymous local
     let @12: u32; // anonymous local
     let @13: u32; // anonymous local
-    let @14: u32; // anonymous local
-    let @15: (); // anonymous local
-    let @16: u32; // anonymous local
-    let @17: (); // anonymous local
-    let @18: (); // anonymous local
-    let @19: (); // anonymous local
-    let @20: (); // anonymous local
-    let @21: (); // anonymous local
+    let @14: (); // anonymous local
+    let @15: u32; // anonymous local
+    let @16: (); // anonymous local
 
     i@2 := const (0 : u32)
     @fake_read(i@2)
@@ -399,58 +345,50 @@ fn test_crate::test_loop5(@1: u32) -> u32
     s@4 := const (0 : u32)
     @fake_read(s@4)
     loop {
-        @8 := copy (i@2)
-        @9 := copy (max@1)
-        @7 := move (@8) < move (@9)
-        if move (@7) {
-            drop @9
+        @7 := copy (i@2)
+        @8 := copy (max@1)
+        @6 := move (@7) < move (@8)
+        if move (@6) {
             drop @8
+            drop @7
             loop {
-                @12 := copy (j@3)
-                @13 := copy (max@1)
-                @11 := move (@12) < move (@13)
-                if move (@11) {
-                    drop @13
+                @11 := copy (j@3)
+                @12 := copy (max@1)
+                @10 := move (@11) < move (@12)
+                if move (@10) {
                     drop @12
-                    @14 := copy (j@3)
-                    s@4 := copy (s@4) + move (@14)
-                    drop @14
-                    j@3 := copy (j@3) + const (1 : u32)
-                    @19 := ()
-                    @6 := move (@19)
                     drop @11
+                    @13 := copy (j@3)
+                    s@4 := copy (s@4) + move (@13)
+                    drop @13
+                    j@3 := copy (j@3) + const (1 : u32)
+                    drop @10
                     continue 0
                 }
                 else {
                     break 0
                 }
             }
-            drop @13
             drop @12
-            @20 := ()
-            @10 := move (@20)
-            drop @15
             drop @11
+            drop @14
             drop @10
-            @16 := copy (i@2)
-            s@4 := copy (s@4) + move (@16)
-            drop @16
+            drop @9
+            @15 := copy (i@2)
+            s@4 := copy (s@4) + move (@15)
+            drop @15
             i@2 := copy (i@2) + const (1 : u32)
-            @21 := ()
-            @6 := move (@21)
-            drop @7
+            drop @6
             continue 0
         }
         else {
             break 0
         }
     }
-    drop @9
     drop @8
-    @18 := ()
-    @5 := move (@18)
-    drop @17
     drop @7
+    drop @16
+    drop @6
     drop @5
     @0 := copy (s@4)
     drop s@4
@@ -466,67 +404,54 @@ fn test_crate::test_loop6(@1: u32) -> u32
     let i@2: u32; // local
     let s@3: u32; // local
     let @4: (); // anonymous local
-    let @5: (); // anonymous local
-    let @6: bool; // anonymous local
+    let @5: bool; // anonymous local
+    let @6: u32; // anonymous local
     let @7: u32; // anonymous local
-    let @8: u32; // anonymous local
-    let @9: (); // anonymous local
-    let @10: bool; // anonymous local
+    let @8: (); // anonymous local
+    let @9: bool; // anonymous local
+    let @10: u32; // anonymous local
     let @11: u32; // anonymous local
-    let @12: u32; // anonymous local
-    let @13: (); // anonymous local
-    let @14: (); // anonymous local
-    let @15: (); // anonymous local
-    let @16: (); // anonymous local
-    let @17: (); // anonymous local
+    let @12: (); // anonymous local
 
     i@2 := const (0 : u32)
     @fake_read(i@2)
     s@3 := const (0 : u32)
     @fake_read(s@3)
     loop {
-        @7 := copy (i@2)
-        @8 := copy (max@1)
-        @6 := move (@7) < move (@8)
-        if move (@6) {
-            drop @8
+        @6 := copy (i@2)
+        @7 := copy (max@1)
+        @5 := move (@6) < move (@7)
+        if move (@5) {
             drop @7
-            @11 := copy (i@2)
-            @10 := move (@11) > const (3 : u32)
-            if move (@10) {
+            drop @6
+            @10 := copy (i@2)
+            @9 := move (@10) > const (3 : u32)
+            if move (@9) {
             }
             else {
-                drop @11
-                @16 := ()
-                @9 := move (@16)
                 drop @10
                 drop @9
-                @12 := copy (i@2)
-                s@3 := copy (s@3) + move (@12)
-                drop @12
+                drop @8
+                @11 := copy (i@2)
+                s@3 := copy (s@3) + move (@11)
+                drop @11
                 i@2 := copy (i@2) + const (1 : u32)
-                @17 := ()
-                @5 := move (@17)
-                drop @6
+                drop @5
                 continue 0
             }
-            drop @11
-            @15 := ()
-            @4 := move (@15)
             drop @10
             drop @9
+            drop @8
             break 0
         }
         else {
-            drop @8
             drop @7
-            @14 := ()
-            @4 := move (@14)
-            drop @13
+            drop @6
+            drop @12
             break 0
         }
     }
-    drop @6
+    drop @5
     drop @4
     // All the below nodes are exit candidates (each of them is referenced twice)
     s@3 := copy (s@3) + const (1 : u32)
@@ -546,20 +471,14 @@ fn test_crate::test_loop7(@1: u32) -> u32
     let @5: bool; // anonymous local
     let @6: u32; // anonymous local
     let @7: u32; // anonymous local
-    let @8: (); // anonymous local
-    let @9: bool; // anonymous local
+    let @8: bool; // anonymous local
+    let @9: u32; // anonymous local
     let @10: u32; // anonymous local
-    let @11: u32; // anonymous local
-    let @12: (); // anonymous local
-    let @13: bool; // anonymous local
+    let @11: (); // anonymous local
+    let @12: bool; // anonymous local
+    let @13: u32; // anonymous local
     let @14: u32; // anonymous local
-    let @15: u32; // anonymous local
-    let @16: (); // anonymous local
-    let @17: (); // anonymous local
-    let @18: (); // anonymous local
-    let @19: (); // anonymous local
-    let @20: (); // anonymous local
-    let @21: (); // anonymous local
+    let @15: (); // anonymous local
 
     i@2 := const (0 : u32)
     @fake_read(i@2)
@@ -572,55 +491,45 @@ fn test_crate::test_loop7(@1: u32) -> u32
         drop @7
         drop @6
         loop {
-            @10 := copy (i@2)
-            @11 := copy (max@1)
-            @9 := move (@10) < move (@11)
-            if move (@9) {
-                drop @11
+            @9 := copy (i@2)
+            @10 := copy (max@1)
+            @8 := move (@9) < move (@10)
+            if move (@8) {
                 drop @10
-                @14 := copy (i@2)
-                @13 := move (@14) > const (3 : u32)
-                if move (@13) {
+                drop @9
+                @13 := copy (i@2)
+                @12 := move (@13) > const (3 : u32)
+                if move (@12) {
                 }
                 else {
-                    drop @14
-                    @20 := ()
-                    @12 := move (@20)
                     drop @13
                     drop @12
-                    @15 := copy (i@2)
-                    s@3 := copy (s@3) + move (@15)
-                    drop @15
+                    drop @11
+                    @14 := copy (i@2)
+                    s@3 := copy (s@3) + move (@14)
+                    drop @14
                     i@2 := copy (i@2) + const (1 : u32)
-                    @21 := ()
-                    @8 := move (@21)
-                    drop @9
+                    drop @8
                     continue 0
                 }
-                drop @14
-                @19 := ()
-                @4 := move (@19)
                 drop @13
                 drop @12
+                drop @11
                 break 0
             }
             else {
-                drop @11
                 drop @10
-                @18 := ()
-                @4 := move (@18)
-                drop @16
+                drop @9
+                drop @15
                 break 0
             }
         }
-        drop @9
+        drop @8
     }
     else {
         drop @7
         drop @6
         s@3 := const (2 : u32)
-        @17 := ()
-        @4 := move (@17)
     }
     drop @5
     drop @4
@@ -658,13 +567,6 @@ fn test_crate::test_loops()
     let @22: (); // anonymous local
     let @23: bool; // anonymous local
     let @24: u32; // anonymous local
-    let @25: (); // anonymous local
-    let @26: (); // anonymous local
-    let @27: (); // anonymous local
-    let @28: (); // anonymous local
-    let @29: (); // anonymous local
-    let @30: (); // anonymous local
-    let @31: (); // anonymous local
 
     x@1 := test_crate::test_loop1(const (2 : u32))
     @fake_read(x@1)
@@ -677,8 +579,6 @@ fn test_crate::test_loops()
         panic(core::panicking::panic)
     }
     drop @4
-    @25 := ()
-    @2 := move (@25)
     drop @3
     drop @2
     x@5 := test_crate::test_loop2(const (2 : u32))
@@ -692,8 +592,6 @@ fn test_crate::test_loops()
         panic(core::panicking::panic)
     }
     drop @8
-    @26 := ()
-    @6 := move (@26)
     drop @7
     drop @6
     x@9 := test_crate::test_loop3(const (2 : u32))
@@ -707,8 +605,6 @@ fn test_crate::test_loops()
         panic(core::panicking::panic)
     }
     drop @12
-    @27 := ()
-    @10 := move (@27)
     drop @11
     drop @10
     x@13 := test_crate::test_loop4(const (20 : u32))
@@ -722,8 +618,6 @@ fn test_crate::test_loops()
         panic(core::panicking::panic)
     }
     drop @16
-    @28 := ()
-    @14 := move (@28)
     drop @15
     drop @14
     x@17 := test_crate::test_loop5(const (2 : u32))
@@ -737,8 +631,6 @@ fn test_crate::test_loops()
         panic(core::panicking::panic)
     }
     drop @20
-    @29 := ()
-    @18 := move (@29)
     drop @19
     drop @18
     x@21 := test_crate::test_loop6(const (2 : u32))
@@ -752,12 +644,9 @@ fn test_crate::test_loops()
         panic(core::panicking::panic)
     }
     drop @24
-    @30 := ()
-    @22 := move (@30)
     drop @23
     drop @22
-    @31 := ()
-    @0 := move (@31)
+    @0 := ()
     drop x@21
     drop x@17
     drop x@13
@@ -936,35 +825,26 @@ fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize
     let @6: core::ops::range::Range<i32>[core::marker::Sized<i32>]; // anonymous local
     let iter@7: core::ops::range::Range<i32>[core::marker::Sized<i32>]; // local
     let @8: (); // anonymous local
-    let @9: (); // anonymous local
-    let @10: core::option::Option<i32>[core::marker::Sized<i32>]; // anonymous local
+    let @9: core::option::Option<i32>[core::marker::Sized<i32>]; // anonymous local
+    let @10: &'_ mut (core::ops::range::Range<i32>[core::marker::Sized<i32>]); // anonymous local
     let @11: &'_ mut (core::ops::range::Range<i32>[core::marker::Sized<i32>]); // anonymous local
-    let @12: &'_ mut (core::ops::range::Range<i32>[core::marker::Sized<i32>]); // anonymous local
-    let @13: (); // anonymous local
+    let @12: (); // anonymous local
+    let @13: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // anonymous local
     let @14: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // anonymous local
-    let @15: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // anonymous local
-    let @16: usize; // anonymous local
-    let iter@17: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // local
-    let @18: (); // anonymous local
-    let @19: core::option::Option<usize>[core::marker::Sized<usize>]; // anonymous local
+    let @15: usize; // anonymous local
+    let iter@16: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // local
+    let @17: (); // anonymous local
+    let @18: core::option::Option<usize>[core::marker::Sized<usize>]; // anonymous local
+    let @19: &'_ mut (core::ops::range::Range<usize>[core::marker::Sized<usize>]); // anonymous local
     let @20: &'_ mut (core::ops::range::Range<usize>[core::marker::Sized<usize>]); // anonymous local
-    let @21: &'_ mut (core::ops::range::Range<usize>[core::marker::Sized<usize>]); // anonymous local
+    let @21: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // anonymous local
     let @22: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // anonymous local
-    let @23: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // anonymous local
-    let @24: usize; // anonymous local
-    let iter@25: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // local
-    let @26: (); // anonymous local
-    let @27: core::option::Option<usize>[core::marker::Sized<usize>]; // anonymous local
+    let @23: usize; // anonymous local
+    let iter@24: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // local
+    let @25: (); // anonymous local
+    let @26: core::option::Option<usize>[core::marker::Sized<usize>]; // anonymous local
+    let @27: &'_ mut (core::ops::range::Range<usize>[core::marker::Sized<usize>]); // anonymous local
     let @28: &'_ mut (core::ops::range::Range<usize>[core::marker::Sized<usize>]); // anonymous local
-    let @29: &'_ mut (core::ops::range::Range<usize>[core::marker::Sized<usize>]); // anonymous local
-    let @30: (); // anonymous local
-    let @31: (); // anonymous local
-    let @32: (); // anonymous local
-    let @33: (); // anonymous local
-    let @34: (); // anonymous local
-    let @35: (); // anonymous local
-    let @36: (); // anonymous local
-    let @37: (); // anonymous local
 
     s@3 := const (0 : usize)
     @fake_read(s@3)
@@ -974,108 +854,92 @@ fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize
     @fake_read(@5)
     iter@7 := move (@5)
     loop {
-        @12 := &mut iter@7
-        @11 := &two-phase-mut *(@12)
-        @10 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, i32>[core::marker::Sized<i32>, core::iter::range::{impl core::iter::range::Step for i32}#40](move (@11))
-        drop @11
-        @fake_read(@10)
-        match @10 {
+        @11 := &mut iter@7
+        @10 := &two-phase-mut *(@11)
+        @9 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, i32>[core::marker::Sized<i32>, core::iter::range::{impl core::iter::range::Step for i32}#40](move (@10))
+        drop @10
+        @fake_read(@9)
+        match @9 {
             0 => {
                 break 0
             },
             1 => {
                 s@3 := copy (s@3) + const (1 : usize)
-                @31 := ()
-                @9 := move (@31)
-                drop @12
-                drop @10
+                drop @11
                 drop @9
-                @32 := ()
-                @8 := move (@32)
+                drop @8
                 continue 0
             },
         }
     }
-    @30 := ()
-    @4 := move (@30)
-    drop @12
-    drop @10
+    drop @11
     drop @9
+    drop @8
     drop iter@7
     drop @5
     drop @4
-    @16 := copy (step_out@1)
-    @15 := core::ops::range::Range { start: const (0 : usize), end: move (@16) }
-    drop @16
-    @14 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::ops::range::Range<usize>[core::marker::Sized<usize>]>[core::marker::Sized<core::ops::range::Range<usize>[core::marker::Sized<usize>]>, core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6<usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43]](move (@15))
+    @15 := copy (step_out@1)
+    @14 := core::ops::range::Range { start: const (0 : usize), end: move (@15) }
     drop @15
-    @fake_read(@14)
-    iter@17 := move (@14)
+    @13 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::ops::range::Range<usize>[core::marker::Sized<usize>]>[core::marker::Sized<core::ops::range::Range<usize>[core::marker::Sized<usize>]>, core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6<usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43]](move (@14))
+    drop @14
+    @fake_read(@13)
+    iter@16 := move (@13)
     loop {
-        @21 := &mut iter@17
-        @20 := &two-phase-mut *(@21)
-        @19 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43](move (@20))
-        drop @20
-        @fake_read(@19)
-        match @19 {
+        @20 := &mut iter@16
+        @19 := &two-phase-mut *(@20)
+        @18 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43](move (@19))
+        drop @19
+        @fake_read(@18)
+        match @18 {
             0 => {
                 break 0
             },
             1 => {
-                @24 := copy (step_in@2)
-                @23 := core::ops::range::Range { start: const (0 : usize), end: move (@24) }
-                drop @24
-                @22 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::ops::range::Range<usize>[core::marker::Sized<usize>]>[core::marker::Sized<core::ops::range::Range<usize>[core::marker::Sized<usize>]>, core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6<usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43]](move (@23))
+                @23 := copy (step_in@2)
+                @22 := core::ops::range::Range { start: const (0 : usize), end: move (@23) }
                 drop @23
-                @fake_read(@22)
-                iter@25 := move (@22)
+                @21 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::ops::range::Range<usize>[core::marker::Sized<usize>]>[core::marker::Sized<core::ops::range::Range<usize>[core::marker::Sized<usize>]>, core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6<usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43]](move (@22))
+                drop @22
+                @fake_read(@21)
+                iter@24 := move (@21)
                 loop {
-                    @29 := &mut iter@25
-                    @28 := &two-phase-mut *(@29)
-                    @27 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43](move (@28))
-                    drop @28
-                    @fake_read(@27)
-                    match @27 {
+                    @28 := &mut iter@24
+                    @27 := &two-phase-mut *(@28)
+                    @26 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43](move (@27))
+                    drop @27
+                    @fake_read(@26)
+                    match @26 {
                         0 => {
                             break 0
                         },
                         1 => {
                             s@3 := copy (s@3) + const (1 : usize)
-                            @36 := ()
-                            @26 := move (@36)
-                            drop @29
-                            drop @27
+                            drop @28
                             drop @26
-                            @37 := ()
-                            @8 := move (@37)
+                            drop @25
                             continue 0
                         },
                     }
                 }
-                @34 := ()
-                @18 := move (@34)
-                drop @29
-                drop @27
+                drop @28
                 drop @26
-                drop iter@25
-                drop @22
+                drop @25
+                drop iter@24
                 drop @21
-                drop @19
+                drop @20
                 drop @18
-                @35 := ()
-                @8 := move (@35)
+                drop @17
                 continue 0
             },
         }
     }
-    @33 := ()
-    @13 := move (@33)
-    drop @21
-    drop @19
+    drop @20
     drop @18
-    drop iter@17
-    drop @14
+    drop @17
+    drop iter@16
     drop @13
+    drop @12
     @0 := copy (s@3)
     drop s@3
     return
@@ -1133,15 +997,11 @@ fn test_crate::loop_inside_if(@1: bool, @2: u32) -> u32
     let @8: u32; // anonymous local
     let iter@9: core::ops::range::Range<u32>[core::marker::Sized<u32>]; // local
     let @10: (); // anonymous local
-    let @11: (); // anonymous local
-    let @12: core::option::Option<u32>[core::marker::Sized<u32>]; // anonymous local
+    let @11: core::option::Option<u32>[core::marker::Sized<u32>]; // anonymous local
+    let @12: &'_ mut (core::ops::range::Range<u32>[core::marker::Sized<u32>]); // anonymous local
     let @13: &'_ mut (core::ops::range::Range<u32>[core::marker::Sized<u32>]); // anonymous local
-    let @14: &'_ mut (core::ops::range::Range<u32>[core::marker::Sized<u32>]); // anonymous local
-    let i@15: u32; // local
-    let @16: u32; // anonymous local
-    let @17: (); // anonymous local
-    let @18: (); // anonymous local
-    let @19: (); // anonymous local
+    let i@14: u32; // local
+    let @15: u32; // anonymous local
 
     @3 := copy (b@1)
     if move (@3) {
@@ -1155,37 +1015,31 @@ fn test_crate::loop_inside_if(@1: bool, @2: u32) -> u32
         @fake_read(@6)
         iter@9 := move (@6)
         loop {
-            @14 := &mut iter@9
-            @13 := &two-phase-mut *(@14)
-            @12 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, u32>[core::marker::Sized<u32>, core::iter::range::{impl core::iter::range::Step for u32}#39](move (@13))
-            drop @13
-            @fake_read(@12)
-            match @12 {
+            @13 := &mut iter@9
+            @12 := &two-phase-mut *(@13)
+            @11 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, u32>[core::marker::Sized<u32>, core::iter::range::{impl core::iter::range::Step for u32}#39](move (@12))
+            drop @12
+            @fake_read(@11)
+            match @11 {
                 0 => {
                     break 0
                 },
                 1 => {
-                    i@15 := copy ((@12 as variant @1).0)
-                    @16 := copy (i@15)
-                    s@4 := copy (s@4) + move (@16)
-                    drop @16
-                    @18 := ()
-                    @11 := move (@18)
-                    drop i@15
-                    drop @14
-                    drop @12
+                    i@14 := copy ((@11 as variant @1).0)
+                    @15 := copy (i@14)
+                    s@4 := copy (s@4) + move (@15)
+                    drop @15
+                    drop i@14
+                    drop @13
                     drop @11
-                    @19 := ()
-                    @10 := move (@19)
+                    drop @10
                     continue 0
                 },
             }
         }
-        @17 := ()
-        @5 := move (@17)
-        drop @14
-        drop @12
+        drop @13
         drop @11
+        drop @10
         drop iter@9
         drop @6
         drop @5
@@ -1206,45 +1060,38 @@ fn test_crate::sum(@1: u32) -> u32
     let i@2: u32; // local
     let s@3: u32; // local
     let @4: (); // anonymous local
-    let @5: (); // anonymous local
-    let @6: bool; // anonymous local
+    let @5: bool; // anonymous local
+    let @6: u32; // anonymous local
     let @7: u32; // anonymous local
     let @8: u32; // anonymous local
-    let @9: u32; // anonymous local
-    let @10: (); // anonymous local
-    let @11: (); // anonymous local
-    let @12: (); // anonymous local
+    let @9: (); // anonymous local
 
     i@2 := const (0 : u32)
     @fake_read(i@2)
     s@3 := const (0 : u32)
     @fake_read(s@3)
     loop {
-        @7 := copy (i@2)
-        @8 := copy (max@1)
-        @6 := move (@7) < move (@8)
-        if move (@6) {
-            drop @8
+        @6 := copy (i@2)
+        @7 := copy (max@1)
+        @5 := move (@6) < move (@7)
+        if move (@5) {
             drop @7
-            @9 := copy (i@2)
-            s@3 := copy (s@3) + move (@9)
-            drop @9
-            i@2 := copy (i@2) + const (1 : u32)
-            @11 := ()
-            @5 := move (@11)
             drop @6
+            @8 := copy (i@2)
+            s@3 := copy (s@3) + move (@8)
+            drop @8
+            i@2 := copy (i@2) + const (1 : u32)
+            drop @5
             continue 0
         }
         else {
             break 0
         }
     }
-    drop @8
     drop @7
-    @12 := ()
-    @4 := move (@12)
-    drop @10
     drop @6
+    drop @9
+    drop @5
     drop @4
     s@3 := copy (s@3) * const (2 : u32)
     @0 := copy (s@3)
@@ -1260,48 +1107,41 @@ fn test_crate::sum_array<const N : usize>(@1: Array<u32, const N : usize>) -> u3
     let i@2: usize; // local
     let s@3: u32; // local
     let @4: (); // anonymous local
-    let @5: (); // anonymous local
-    let @6: bool; // anonymous local
-    let @7: usize; // anonymous local
-    let @8: u32; // anonymous local
-    let @9: usize; // anonymous local
-    let @10: (); // anonymous local
-    let @11: (); // anonymous local
-    let @12: (); // anonymous local
-    let @13: &'_ (Array<u32, const N : usize>); // anonymous local
-    let @14: &'_ (u32); // anonymous local
+    let @5: bool; // anonymous local
+    let @6: usize; // anonymous local
+    let @7: u32; // anonymous local
+    let @8: usize; // anonymous local
+    let @9: (); // anonymous local
+    let @10: &'_ (Array<u32, const N : usize>); // anonymous local
+    let @11: &'_ (u32); // anonymous local
 
     i@2 := const (0 : usize)
     @fake_read(i@2)
     s@3 := const (0 : u32)
     @fake_read(s@3)
     loop {
-        @7 := copy (i@2)
-        @6 := move (@7) < const (const N : usize)
-        if move (@6) {
+        @6 := copy (i@2)
+        @5 := move (@6) < const (const N : usize)
+        if move (@5) {
+            drop @6
+            @8 := copy (i@2)
+            @10 := &a@1
+            @11 := @ArrayIndexShared<'_, u32, const N : usize>(move (@10), copy (@8))
+            @7 := copy (*(@11))
+            s@3 := copy (s@3) + move (@7)
             drop @7
-            @9 := copy (i@2)
-            @13 := &a@1
-            @14 := @ArrayIndexShared<'_, u32, const N : usize>(move (@13), copy (@9))
-            @8 := copy (*(@14))
-            s@3 := copy (s@3) + move (@8)
             drop @8
-            drop @9
             i@2 := copy (i@2) + const (1 : usize)
-            @11 := ()
-            @5 := move (@11)
-            drop @6
+            drop @5
             continue 0
         }
         else {
             break 0
         }
     }
-    drop @7
-    @12 := ()
-    @4 := move (@12)
-    drop @10
     drop @6
+    drop @9
+    drop @5
     drop @4
     @0 := copy (s@3)
     drop s@3
@@ -1387,52 +1227,46 @@ fn test_crate::clear<'_0>(@1: &'_0 mut (alloc::vec::Vec<u32, alloc::alloc::Globa
     let @0: (); // return
     let v@1: &'_ mut (alloc::vec::Vec<u32, alloc::alloc::Global>[core::marker::Sized<u32>, core::marker::Sized<alloc::alloc::Global>]); // arg #1
     let i@2: usize; // local
-    let @3: (); // anonymous local
-    let @4: bool; // anonymous local
+    let @3: bool; // anonymous local
+    let @4: usize; // anonymous local
     let @5: usize; // anonymous local
-    let @6: usize; // anonymous local
-    let @7: &'_ (alloc::vec::Vec<u32, alloc::alloc::Global>[core::marker::Sized<u32>, core::marker::Sized<alloc::alloc::Global>]); // anonymous local
-    let @8: &'_ mut (u32); // anonymous local
-    let @9: &'_ mut (alloc::vec::Vec<u32, alloc::alloc::Global>[core::marker::Sized<u32>, core::marker::Sized<alloc::alloc::Global>]); // anonymous local
-    let @10: usize; // anonymous local
-    let @11: (); // anonymous local
-    let @12: (); // anonymous local
-    let @13: (); // anonymous local
+    let @6: &'_ (alloc::vec::Vec<u32, alloc::alloc::Global>[core::marker::Sized<u32>, core::marker::Sized<alloc::alloc::Global>]); // anonymous local
+    let @7: &'_ mut (u32); // anonymous local
+    let @8: &'_ mut (alloc::vec::Vec<u32, alloc::alloc::Global>[core::marker::Sized<u32>, core::marker::Sized<alloc::alloc::Global>]); // anonymous local
+    let @9: usize; // anonymous local
+    let @10: (); // anonymous local
 
     i@2 := const (0 : usize)
     @fake_read(i@2)
     loop {
-        @5 := copy (i@2)
-        @7 := &*(v@1)
-        @6 := alloc::vec::{alloc::vec::Vec<T, A>[@TraitClause0, @TraitClause1]}#1::len<'_, u32, alloc::alloc::Global>[core::marker::Sized<u32>, core::marker::Sized<alloc::alloc::Global>](move (@7))
-        drop @7
-        @4 := move (@5) < move (@6)
-        if move (@4) {
-            drop @6
+        @4 := copy (i@2)
+        @6 := &*(v@1)
+        @5 := alloc::vec::{alloc::vec::Vec<T, A>[@TraitClause0, @TraitClause1]}#1::len<'_, u32, alloc::alloc::Global>[core::marker::Sized<u32>, core::marker::Sized<alloc::alloc::Global>](move (@6))
+        drop @6
+        @3 := move (@4) < move (@5)
+        if move (@3) {
             drop @5
-            @9 := &mut *(v@1)
-            @10 := copy (i@2)
-            @8 := alloc::vec::{impl core::ops::index::IndexMut<I> for alloc::vec::Vec<T, A>[@TraitClause0, @TraitClause2]}#14::index_mut<'_, u32, usize, alloc::alloc::Global>[core::marker::Sized<u32>, core::marker::Sized<usize>, core::marker::Sized<alloc::alloc::Global>, core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for usize}#2<u32>[core::marker::Sized<u32>]](move (@9), move (@10))
-            drop @10
+            drop @4
+            @8 := &mut *(v@1)
+            @9 := copy (i@2)
+            @7 := alloc::vec::{impl core::ops::index::IndexMut<I> for alloc::vec::Vec<T, A>[@TraitClause0, @TraitClause2]}#14::index_mut<'_, u32, usize, alloc::alloc::Global>[core::marker::Sized<u32>, core::marker::Sized<usize>, core::marker::Sized<alloc::alloc::Global>, core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for usize}#2<u32>[core::marker::Sized<u32>]](move (@8), move (@9))
             drop @9
-            *(@8) := const (0 : u32)
             drop @8
+            *(@7) := const (0 : u32)
+            drop @7
             i@2 := copy (i@2) + const (1 : usize)
-            @12 := ()
-            @3 := move (@12)
-            drop @4
+            drop @3
             continue 0
         }
         else {
             break 0
         }
     }
-    drop @6
     drop @5
-    @13 := ()
-    @0 := move (@13)
-    drop @11
     drop @4
+    @0 := ()
+    drop @10
+    drop @3
     drop i@2
     @0 := ()
     return
@@ -1451,45 +1285,41 @@ fn test_crate::get_elem_mut<'_0>(@1: &'_0 mut (test_crate::List<usize>[core::mar
     let @0: &'_ mut (usize); // return
     let ls@1: &'_ mut (test_crate::List<usize>[core::marker::Sized<usize>]); // arg #1
     let x@2: usize; // arg #2
-    let @3: (); // anonymous local
-    let y@4: &'_ mut (usize); // local
-    let tl@5: &'_ mut (alloc::boxed::Box<test_crate::List<usize>[core::marker::Sized<usize>]>[core::marker::Sized<alloc::alloc::Global>]); // local
-    let @6: bool; // anonymous local
+    let y@3: &'_ mut (usize); // local
+    let tl@4: &'_ mut (alloc::boxed::Box<test_crate::List<usize>[core::marker::Sized<usize>]>[core::marker::Sized<alloc::alloc::Global>]); // local
+    let @5: bool; // anonymous local
+    let @6: usize; // anonymous local
     let @7: usize; // anonymous local
-    let @8: usize; // anonymous local
-    let @9: &'_ mut (test_crate::List<usize>[core::marker::Sized<usize>]); // anonymous local
-    let @10: (); // anonymous local
+    let @8: &'_ mut (test_crate::List<usize>[core::marker::Sized<usize>]); // anonymous local
 
     loop {
         @fake_read(ls@1)
         match *(ls@1) {
             0 => {
-                y@4 := &mut (*(ls@1) as variant @0).0
-                tl@5 := &mut (*(ls@1) as variant @0).1
-                @7 := copy (*(y@4))
-                @8 := copy (x@2)
-                @6 := move (@7) == move (@8)
-                if move (@6) {
+                y@3 := &mut (*(ls@1) as variant @0).0
+                tl@4 := &mut (*(ls@1) as variant @0).1
+                @6 := copy (*(y@3))
+                @7 := copy (x@2)
+                @5 := move (@6) == move (@7)
+                if move (@5) {
                 }
                 else {
-                    drop @8
                     drop @7
-                    @9 := &mut *(*(tl@5))
-                    ls@1 := move (@9)
-                    drop @9
-                    @10 := ()
-                    @3 := move (@10)
                     drop @6
-                    drop tl@5
-                    drop y@4
+                    @8 := &mut *(*(tl@4))
+                    ls@1 := move (@8)
+                    drop @8
+                    drop @5
+                    drop tl@4
+                    drop y@3
                     continue 0
                 }
-                drop @8
                 drop @7
-                @0 := &mut *(y@4)
                 drop @6
-                drop tl@5
-                drop y@4
+                @0 := &mut *(y@3)
+                drop @5
+                drop tl@4
+                drop y@3
                 return
             },
             1 => {
@@ -1507,51 +1337,44 @@ where
     let ls@1: &'_ mut (test_crate::List<T>[@TraitClause0]); // arg #1
     let i@2: u32; // arg #2
     let @3: (); // anonymous local
-    let @4: (); // anonymous local
-    let x@5: &'_ mut (T); // local
-    let tl@6: &'_ mut (alloc::boxed::Box<test_crate::List<T>[@TraitClause0]>[core::marker::Sized<alloc::alloc::Global>]); // local
-    let @7: bool; // anonymous local
-    let @8: u32; // anonymous local
-    let @9: &'_ mut (test_crate::List<T>[@TraitClause0]); // anonymous local
-    let @10: (); // anonymous local
-    let @11: (); // anonymous local
-    let @12: (); // anonymous local
+    let x@4: &'_ mut (T); // local
+    let tl@5: &'_ mut (alloc::boxed::Box<test_crate::List<T>[@TraitClause0]>[core::marker::Sized<alloc::alloc::Global>]); // local
+    let @6: bool; // anonymous local
+    let @7: u32; // anonymous local
+    let @8: &'_ mut (test_crate::List<T>[@TraitClause0]); // anonymous local
+    let @9: (); // anonymous local
 
     loop {
         @fake_read(ls@1)
         match *(ls@1) {
             0 => {
-                x@5 := &mut (*(ls@1) as variant @0).0
-                tl@6 := &mut (*(ls@1) as variant @0).1
-                @8 := copy (i@2)
-                @7 := move (@8) == const (0 : u32)
-                if move (@7) {
+                x@4 := &mut (*(ls@1) as variant @0).0
+                tl@5 := &mut (*(ls@1) as variant @0).1
+                @7 := copy (i@2)
+                @6 := move (@7) == const (0 : u32)
+                if move (@6) {
                 }
                 else {
+                    drop @7
+                    @8 := &mut *(*(tl@5))
+                    ls@1 := move (@8)
                     drop @8
-                    @9 := &mut *(*(tl@6))
-                    ls@1 := move (@9)
-                    drop @9
                     i@2 := copy (i@2) - const (1 : u32)
-                    @12 := ()
-                    @4 := move (@12)
-                    drop @7
-                    drop tl@6
-                    drop x@5
+                    drop @6
+                    drop tl@5
+                    drop x@4
                     continue 0
                 }
-                drop @8
-                @0 := &mut *(x@5)
                 drop @7
-                drop tl@6
-                drop x@5
+                @0 := &mut *(x@4)
+                drop @6
+                drop tl@5
+                drop x@4
                 drop @3
                 return
             },
             _ => {
-                @11 := ()
-                @3 := move (@11)
-                drop @10
+                drop @9
                 drop @3
                 panic(core::panicking::panic_explicit)
             },
diff --git a/charon/tests/ui/method-impl-generalization.out b/charon/tests/ui/method-impl-generalization.out
index 997b5c451..22fbdd875 100644
--- a/charon/tests/ui/method-impl-generalization.out
+++ b/charon/tests/ui/method-impl-generalization.out
@@ -37,10 +37,8 @@ where
     let @0: (); // return
     let self@1: (); // arg #1
     let _other@2: T; // arg #2
-    let @3: (); // anonymous local
 
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     drop _other@2
     @0 := ()
     return
@@ -91,7 +89,6 @@ fn test_crate::main()
     let @9: &'_ (()); // anonymous local
     let @10: &'_ (()); // anonymous local
     let @11: (); // anonymous local
-    let @12: (); // anonymous local
 
     @2 := ()
     @5 := const (1 : u32)
@@ -121,8 +118,7 @@ fn test_crate::main()
     drop @10
     drop @8
     drop @6
-    @12 := ()
-    @0 := move (@12)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/ml-name-matcher-tests.out b/charon/tests/ui/ml-name-matcher-tests.out
index 76be287a8..70b19c9c7 100644
--- a/charon/tests/ui/ml-name-matcher-tests.out
+++ b/charon/tests/ui/ml-name-matcher-tests.out
@@ -3,10 +3,8 @@
 fn test_crate::foo::bar()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -35,10 +33,8 @@ where
     [@TraitClause1]: core::marker::Sized<U>,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -58,10 +54,8 @@ where
     [@TraitClause2]: core::marker::Sized<V>,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -161,7 +155,6 @@ fn test_crate::foo()
     let @9: &'_ (Slice<bool>); // anonymous local
     let @10: &'_ (Slice<bool>); // anonymous local
     let @11: core::ops::range::RangeFrom<usize>[core::marker::Sized<usize>]; // anonymous local
-    let @12: (); // anonymous local
 
     @3 := core::option::Option::Some { 0: const (0 : i32) }
     @2 := &@3
@@ -185,8 +178,7 @@ fn test_crate::foo()
     @8 := &*(@9)
     @fake_read(@8)
     drop @8
-    @12 := ()
-    @0 := move (@12)
+    @0 := ()
     drop @9
     drop @7
     drop slice@4
diff --git a/charon/tests/ui/no_nested_borrows.out b/charon/tests/ui/no_nested_borrows.out
index 9fb850e64..3cd340aa3 100644
--- a/charon/tests/ui/no_nested_borrows.out
+++ b/charon/tests/ui/no_nested_borrows.out
@@ -63,11 +63,9 @@ fn test_crate::use_tuple_struct<'_0>(@1: &'_0 mut (test_crate::Tuple<u32, u32>[c
 {
     let @0: (); // return
     let x@1: &'_ mut (test_crate::Tuple<u32, u32>[core::marker::Sized<u32>, core::marker::Sized<u32>]); // arg #1
-    let @2: (); // anonymous local
 
     (*(x@1)).0 := const (1 : u32)
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -189,7 +187,6 @@ fn test_crate::test2()
     let e0@11: test_crate::EmptyEnum; // local
     let e1@12: test_crate::EmptyEnum; // local
     let enum0@13: test_crate::Enum; // local
-    let @14: (); // anonymous local
 
     x@1 := const (23 : u32)
     @fake_read(x@1)
@@ -217,8 +214,7 @@ fn test_crate::test2()
     @fake_read(e1@12)
     enum0@13 := test_crate::Enum::Variant1 {  }
     @fake_read(enum0@13)
-    @14 := ()
-    @0 := move (@14)
+    @0 := ()
     drop enum0@13
     drop e1@12
     drop e0@11
@@ -264,7 +260,6 @@ fn test_crate::test_list1()
     let l@1: test_crate::List<i32>[core::marker::Sized<i32>]; // local
     let @2: alloc::boxed::Box<test_crate::List<i32>[core::marker::Sized<i32>]>[core::marker::Sized<alloc::alloc::Global>]; // anonymous local
     let @3: test_crate::List<i32>[core::marker::Sized<i32>]; // anonymous local
-    let @4: (); // anonymous local
 
     @3 := test_crate::List::Nil {  }
     @2 := @BoxNew<test_crate::List<i32>[core::marker::Sized<i32>]>[core::marker::Sized<test_crate::List<i32>[core::marker::Sized<i32>]>](move (@3))
@@ -273,8 +268,7 @@ fn test_crate::test_list1()
     drop @2
     drop @2
     @fake_read(l@1)
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     drop l@1
     drop l@1
     @0 := ()
@@ -300,8 +294,6 @@ fn test_crate::test_box1()
     let @6: (); // anonymous local
     let @7: bool; // anonymous local
     let @8: i32; // anonymous local
-    let @9: (); // anonymous local
-    let @10: (); // anonymous local
 
     b@1 := @BoxNew<i32>[core::marker::Sized<i32>](const (0 : i32))
     @fake_read(b@1)
@@ -323,12 +315,9 @@ fn test_crate::test_box1()
         panic(core::panicking::panic)
     }
     drop @8
-    @9 := ()
-    @6 := move (@9)
     drop @7
     drop @6
-    @10 := ()
-    @0 := move (@10)
+    @0 := ()
     drop x@4
     drop x@2
     drop b@1
@@ -351,12 +340,10 @@ fn test_crate::test_unreachable(@1: bool)
     let @0: (); // return
     let b@1: bool; // arg #1
     let @2: bool; // anonymous local
-    let @3: (); // anonymous local
 
     @2 := copy (b@1)
     assert(move (@2) == false)
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     drop @2
     @0 := ()
     return
@@ -507,38 +494,24 @@ fn test_crate::test_even_odd()
     let @6: bool; // anonymous local
     let @7: (); // anonymous local
     let @8: bool; // anonymous local
-    let @9: (); // anonymous local
-    let @10: (); // anonymous local
-    let @11: (); // anonymous local
-    let @12: (); // anonymous local
-    let @13: (); // anonymous local
 
     @2 := test_crate::even(const (0 : u32))
     assert(move (@2) == true)
-    @9 := ()
-    @1 := move (@9)
     drop @2
     drop @1
     @4 := test_crate::even(const (4 : u32))
     assert(move (@4) == true)
-    @10 := ()
-    @3 := move (@10)
     drop @4
     drop @3
     @6 := test_crate::odd(const (1 : u32))
     assert(move (@6) == true)
-    @11 := ()
-    @5 := move (@11)
     drop @6
     drop @5
     @8 := test_crate::odd(const (5 : u32))
     assert(move (@8) == true)
-    @12 := ()
-    @7 := move (@12)
     drop @8
     drop @7
-    @13 := ()
-    @0 := move (@13)
+    @0 := ()
     @0 := ()
     return
 }
@@ -611,11 +584,9 @@ fn test_crate::incr<'_0>(@1: &'_0 mut (u32))
 {
     let @0: (); // return
     let x@1: &'_ mut (u32); // arg #1
-    let @2: (); // anonymous local
 
     *(x@1) := copy (*(x@1)) + const (1 : u32)
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/opacity.out b/charon/tests/ui/opacity.out
index 803f83711..e70c110bc 100644
--- a/charon/tests/ui/opacity.out
+++ b/charon/tests/ui/opacity.out
@@ -78,7 +78,6 @@ fn test_crate::foo()
     let @6: &'_ (i32); // anonymous local
     let @7: &'_ (i32); // anonymous local
     let @8: i32; // anonymous local
-    let @9: (); // anonymous local
 
     @3 := core::option::Option::Some { 0: const (0 : i32) }
     @2 := &@3
@@ -99,8 +98,7 @@ fn test_crate::foo()
     drop @8
     drop @7
     drop @5
-    @9 := ()
-    @0 := move (@9)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/opaque-trait.out b/charon/tests/ui/opaque-trait.out
index a9bf53a29..ee4a13222 100644
--- a/charon/tests/ui/opaque-trait.out
+++ b/charon/tests/ui/opaque-trait.out
@@ -72,10 +72,8 @@ global test_crate::{impl test_crate::Trait for ()}#1::CONST3: usize = test_crate
 fn test_crate::{impl test_crate::Trait for ()}#1::method1()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -83,10 +81,8 @@ fn test_crate::{impl test_crate::Trait for ()}#1::method1()
 fn test_crate::{impl test_crate::Trait for ()}#1::method2()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -113,10 +109,8 @@ global test_crate::{impl test_crate::Trait for u8}::CONST2: usize = test_crate::
 fn test_crate::{impl test_crate::Trait for u8}::method1()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -124,10 +118,8 @@ fn test_crate::{impl test_crate::Trait for u8}::method1()
 fn test_crate::{impl test_crate::Trait for u8}::method2()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -146,10 +138,8 @@ trait core::marker::Sized<Self>
 fn test_crate::Trait::method1<Self>()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -162,14 +152,12 @@ where
     let @0: (); // return
     let @1: (); // anonymous local
     let @2: usize; // anonymous local
-    let @3: (); // anonymous local
 
     @1 := @TraitClause1::method1()
     drop @1
     @2 := const (@TraitClause1::CONST1)
     drop @2
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     @0 := ()
     return
 }
@@ -177,10 +165,8 @@ where
 fn test_crate::Trait::method2<Self>()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/opaque_attribute.out b/charon/tests/ui/opaque_attribute.out
index 353d51521..bb87aef34 100644
--- a/charon/tests/ui/opaque_attribute.out
+++ b/charon/tests/ui/opaque_attribute.out
@@ -91,13 +91,11 @@ fn test_crate::call_fn_in_opaque_module()
 {
     let @0: (); // return
     let @1: u32; // anonymous local
-    let @2: (); // anonymous local
 
     @1 := test_crate::opaque::fn_in_opaque_module()
     @fake_read(@1)
     drop @1
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/panics.out b/charon/tests/ui/panics.out
index b610c2399..b321ac21e 100644
--- a/charon/tests/ui/panics.out
+++ b/charon/tests/ui/panics.out
@@ -63,17 +63,12 @@ fn test_crate::panic4()
     let @0: (); // return
     let @1: (); // anonymous local
     let @2: bool; // anonymous local
-    let @3: (); // anonymous local
-    let @4: (); // anonymous local
 
     @2 := const (false)
     assert(move (@2) == true)
-    @3 := ()
-    @1 := move (@3)
     drop @2
     drop @1
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     @0 := ()
     return
 }
@@ -87,8 +82,6 @@ fn test_crate::panic5()
     let @4: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local
     let @5: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local
     let @6: Array<&'_ (Str), 1 : usize>; // anonymous local
-    let @7: (); // anonymous local
-    let @8: (); // anonymous local
 
     @2 := const (false)
     if move (@2) {
@@ -101,12 +94,9 @@ fn test_crate::panic5()
         drop @4
         panic(core::panicking::panic_fmt)
     }
-    @7 := ()
-    @1 := move (@7)
     drop @2
     drop @1
-    @8 := ()
-    @0 := move (@8)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/predicates-on-late-bound-vars.out b/charon/tests/ui/predicates-on-late-bound-vars.out
index 43ce5fd54..6fd1aed14 100644
--- a/charon/tests/ui/predicates-on-late-bound-vars.out
+++ b/charon/tests/ui/predicates-on-late-bound-vars.out
@@ -71,7 +71,6 @@ fn test_crate::foo()
     let ref_b@1: core::cell::RefCell<bool>; // local
     let @2: core::result::Result<core::cell::Ref<'_, bool>, core::cell::BorrowError>[core::marker::Sized<core::cell::Ref<'_, bool>>, core::marker::Sized<core::cell::BorrowError>]; // anonymous local
     let @3: &'_ (core::cell::RefCell<bool>); // anonymous local
-    let @4: (); // anonymous local
 
     ref_b@1 := core::cell::{core::cell::RefCell<T>}#21::new<bool>[core::marker::Sized<bool>](const (false))
     @fake_read(ref_b@1)
@@ -82,8 +81,7 @@ fn test_crate::foo()
     @fake_read(@2)
     drop @2
     drop @2
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     drop ref_b@1
     @0 := ()
     return
diff --git a/charon/tests/ui/ptr_to_promoted.out b/charon/tests/ui/ptr_to_promoted.out
index 6864b6c0e..7bb6b5c89 100644
--- a/charon/tests/ui/ptr_to_promoted.out
+++ b/charon/tests/ui/ptr_to_promoted.out
@@ -10,7 +10,6 @@ fn test_crate::main()
     let @5: &'_ (u8); // anonymous local
     let @6: u8; // anonymous local
     let @7: &'_ (u8); // anonymous local
-    let @8: (); // anonymous local
 
     @6 := const ([0])
     @7 := &@6
@@ -22,8 +21,7 @@ fn test_crate::main()
     @3 := cast<*const u8, usize>(move (@4))
     drop @4
     drop @3
-    @8 := ()
-    @0 := move (@8)
+    @0 := ()
     drop x@1
     @0 := ()
     return
diff --git a/charon/tests/ui/quantified-clause.out b/charon/tests/ui/quantified-clause.out
index 49ba05574..1756f9db2 100644
--- a/charon/tests/ui/quantified-clause.out
+++ b/charon/tests/ui/quantified-clause.out
@@ -29,10 +29,8 @@ where
 {
     let @0: (); // return
     let _f@1: F; // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     drop _f@1
     @0 := ()
     return
@@ -45,10 +43,8 @@ where
     for<'a> &'b (T) : 'a,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/reconstruct_early_return.out b/charon/tests/ui/reconstruct_early_return.out
index 205c77fd2..9a7fc03a8 100644
--- a/charon/tests/ui/reconstruct_early_return.out
+++ b/charon/tests/ui/reconstruct_early_return.out
@@ -6,78 +6,65 @@ fn test_crate::f() -> usize
     let i@1: i32; // local
     let j@2: i32; // local
     let @3: (); // anonymous local
-    let @4: (); // anonymous local
-    let @5: bool; // anonymous local
-    let @6: i32; // anonymous local
-    let @7: (); // anonymous local
-    let @8: bool; // anonymous local
-    let @9: i32; // anonymous local
-    let @10: bool; // anonymous local
-    let @11: i32; // anonymous local
-    let @12: (); // anonymous local
-    let @13: (); // anonymous local
-    let @14: (); // anonymous local
-    let @15: (); // anonymous local
-    let @16: (); // anonymous local
+    let @4: bool; // anonymous local
+    let @5: i32; // anonymous local
+    let @6: (); // anonymous local
+    let @7: bool; // anonymous local
+    let @8: i32; // anonymous local
+    let @9: bool; // anonymous local
+    let @10: i32; // anonymous local
+    let @11: (); // anonymous local
 
     i@1 := const (0 : i32)
     @fake_read(i@1)
     j@2 := const (0 : i32)
     @fake_read(j@2)
     loop {
-        @6 := copy (i@1)
-        @5 := move (@6) < const (32 : i32)
-        if move (@5) {
-            drop @6
+        @5 := copy (i@1)
+        @4 := move (@5) < const (32 : i32)
+        if move (@4) {
+            drop @5
             j@2 := copy (j@2) + const (1 : i32)
-            @9 := copy (j@2)
-            @8 := move (@9) > const (16 : i32)
-            if move (@8) {
-                drop @9
+            @8 := copy (j@2)
+            @7 := move (@8) > const (16 : i32)
+            if move (@7) {
+                drop @8
                 j@2 := copy (j@2) / const (2 : i32)
-                @14 := ()
-                @7 := move (@14)
             }
             else {
-                drop @9
-                @11 := copy (j@2)
-                @10 := move (@11) > const (32 : i32)
-                if move (@10) {
-                    drop @11
-                    @0 := const (1 : usize)
+                drop @8
+                @10 := copy (j@2)
+                @9 := move (@10) > const (32 : i32)
+                if move (@9) {
                     drop @10
-                    drop @8
+                    @0 := const (1 : usize)
+                    drop @9
                     drop @7
-                    drop @5
+                    drop @6
+                    drop @4
                     drop @3
                     drop j@2
                     drop i@1
                     return
                 }
                 else {
-                    drop @11
-                    @15 := ()
-                    @7 := move (@15)
                     drop @10
+                    drop @9
                 }
             }
-            drop @8
             drop @7
+            drop @6
             i@1 := copy (i@1) + const (1 : i32)
-            @16 := ()
-            @4 := move (@16)
-            drop @5
+            drop @4
             continue 0
         }
         else {
             break 0
         }
     }
-    drop @6
-    @13 := ()
-    @3 := move (@13)
-    drop @12
     drop @5
+    drop @11
+    drop @4
     drop @3
     @0 := const (0 : usize)
     drop j@2
diff --git a/charon/tests/ui/remove-dynamic-checks.out b/charon/tests/ui/remove-dynamic-checks.out
index 11c0e37cc..3e588e97e 100644
--- a/charon/tests/ui/remove-dynamic-checks.out
+++ b/charon/tests/ui/remove-dynamic-checks.out
@@ -32,11 +32,9 @@ fn test_crate::incr<'_0>(@1: &'_0 mut (u32))
 {
     let @0: (); // return
     let x@1: &'_ mut (u32); // arg #1
-    let @2: (); // anonymous local
 
     *(x@1) := copy (*(x@1)) + const (1 : u32)
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -572,19 +570,17 @@ fn test_crate::div_unsigned_to_slice<'_0>(@1: &'_0 mut (Slice<u32>), @2: u32)
     let x@2: u32; // arg #2
     let @3: u32; // anonymous local
     let @4: usize; // anonymous local
-    let @5: (); // anonymous local
-    let @6: &'_ mut (Slice<u32>); // anonymous local
-    let @7: &'_ mut (u32); // anonymous local
+    let @5: &'_ mut (Slice<u32>); // anonymous local
+    let @6: &'_ mut (u32); // anonymous local
 
     @3 := copy (x@2)
     @4 := const (0 : usize)
-    @6 := &mut *(result@1)
-    @7 := @SliceIndexMut<'_, u32>(move (@6), copy (@4))
-    *(@7) := move (@3) / const (3329 : u32)
+    @5 := &mut *(result@1)
+    @6 := @SliceIndexMut<'_, u32>(move (@5), copy (@4))
+    *(@6) := move (@3) / const (3329 : u32)
     drop @3
     drop @4
-    @5 := ()
-    @0 := move (@5)
+    @0 := ()
     @0 := ()
     return
 }
@@ -596,19 +592,17 @@ fn test_crate::div_signed_to_slice<'_0>(@1: &'_0 mut (Slice<i32>), @2: i32)
     let x@2: i32; // arg #2
     let @3: i32; // anonymous local
     let @4: usize; // anonymous local
-    let @5: (); // anonymous local
-    let @6: &'_ mut (Slice<i32>); // anonymous local
-    let @7: &'_ mut (i32); // anonymous local
+    let @5: &'_ mut (Slice<i32>); // anonymous local
+    let @6: &'_ mut (i32); // anonymous local
 
     @3 := copy (x@2)
     @4 := const (0 : usize)
-    @6 := &mut *(result@1)
-    @7 := @SliceIndexMut<'_, i32>(move (@6), copy (@4))
-    *(@7) := move (@3) / const (3329 : i32)
+    @5 := &mut *(result@1)
+    @6 := @SliceIndexMut<'_, i32>(move (@5), copy (@4))
+    *(@6) := move (@3) / const (3329 : i32)
     drop @3
     drop @4
-    @5 := ()
-    @0 := move (@5)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/rust-name-matcher-tests.out b/charon/tests/ui/rust-name-matcher-tests.out
index 9a4dc430f..9d051a02e 100644
--- a/charon/tests/ui/rust-name-matcher-tests.out
+++ b/charon/tests/ui/rust-name-matcher-tests.out
@@ -3,10 +3,8 @@
 fn test_crate::foo::bar()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -35,10 +33,8 @@ where
     [@TraitClause1]: core::marker::Sized<U>,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -57,10 +53,8 @@ where
     [@TraitClause1]: core::marker::Sized<U>,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -79,10 +73,8 @@ where
     [@TraitClause1]: core::marker::Sized<U>,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/rvalues.out b/charon/tests/ui/rvalues.out
index 355b7d264..95e4ca336 100644
--- a/charon/tests/ui/rvalues.out
+++ b/charon/tests/ui/rvalues.out
@@ -8,7 +8,6 @@ fn test_crate::addr_of()
     let @3: &'_ (u32); // anonymous local
     let @4: *const u32; // anonymous local
     let @5: *mut u32; // anonymous local
-    let @6: (); // anonymous local
 
     x@1 := const (0 : u32)
     @fake_read(x@1)
@@ -23,8 +22,7 @@ fn test_crate::addr_of()
     @5 := &raw mut x@1
     @fake_read(@5)
     drop @5
-    @6 := ()
-    @0 := move (@6)
+    @0 := ()
     drop x@1
     @0 := ()
     return
@@ -48,7 +46,6 @@ fn test_crate::literal_casts()
     let @5: f64; // anonymous local
     let @6: f64; // anonymous local
     let @7: f32; // anonymous local
-    let @8: (); // anonymous local
 
     @1 := cast<u64, u8>(const (0 : u64))
     @fake_read(@1)
@@ -67,8 +64,7 @@ fn test_crate::literal_casts()
     @5 := cast<f32, f64>(move (@7))
     @fake_read(@5)
     drop @5
-    @8 := ()
-    @0 := move (@8)
+    @0 := ()
     @0 := ()
     return
 }
@@ -76,10 +72,8 @@ fn test_crate::literal_casts()
 fn test_crate::ptr_casts::foo()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -104,7 +98,6 @@ fn test_crate::ptr_casts()
     let @15: *const u8; // anonymous local
     let @16: *const u8; // anonymous local
     let @17: fn(); // anonymous local
-    let @18: (); // anonymous local
 
     @3 := @ArrayRepeat<'_, u32, 64 : usize>(const (0 : u32))
     @2 := &@3
@@ -144,8 +137,7 @@ fn test_crate::ptr_casts()
     drop @17
     @fake_read(@16)
     drop @16
-    @18 := ()
-    @0 := move (@18)
+    @0 := ()
     drop x@7
     drop x@6
     drop @3
@@ -157,10 +149,8 @@ fn test_crate::ptr_casts()
 fn test_crate::fn_casts::foo()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -168,10 +158,8 @@ fn test_crate::fn_casts::foo()
 unsafe fn test_crate::fn_casts::bar()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -197,7 +185,6 @@ fn test_crate::fn_casts()
     let @5: fn(u8); // anonymous local
     let @6: fn(u8); // anonymous local
     let @7: fn(u8); // anonymous local
-    let @8: (); // anonymous local
 
     @1 := cast<fn(), fn()>(const (test_crate::fn_casts::foo))
     @fake_read(@1)
@@ -217,8 +204,7 @@ fn test_crate::fn_casts()
     drop @7
     @fake_read(@6)
     drop @6
-    @8 := ()
-    @0 := move (@8)
+    @0 := ()
     drop closure@3
     @0 := ()
     return
@@ -233,7 +219,6 @@ fn test_crate::boxes()
     let @0: (); // return
     let @1: alloc::boxed::Box<i32>[core::marker::Sized<alloc::alloc::Global>]; // anonymous local
     let @2: alloc::boxed::Box<i32>[core::marker::Sized<alloc::alloc::Global>]; // anonymous local
-    let @3: (); // anonymous local
 
     @2 := @BoxNew<i32>[core::marker::Sized<alloc::alloc::Global>](const (42 : i32))
     @1 := move (@2)
@@ -242,8 +227,7 @@ fn test_crate::boxes()
     @fake_read(@1)
     drop @1
     drop @1
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/send_bound.out b/charon/tests/ui/send_bound.out
index 927c6e0f3..7685a5a6f 100644
--- a/charon/tests/ui/send_bound.out
+++ b/charon/tests/ui/send_bound.out
@@ -11,10 +11,8 @@ where
 {
     let @0: (); // return
     let _msg@1: M; // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     drop _msg@1
     @0 := ()
     return
@@ -25,14 +23,12 @@ fn test_crate::main()
     let @0: (); // return
     let @1: (); // anonymous local
     let @2: (); // anonymous local
-    let @3: (); // anonymous local
 
     @2 := ()
     @1 := test_crate::foo<()>[core::marker::Sized<()>, core::marker::Send<()>](move (@2))
     drop @2
     drop @1
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out b/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out
index 19bc0e849..10cac5402 100644
--- a/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out
+++ b/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out
@@ -52,10 +52,8 @@ where
     [@TraitClause1]: test_crate::HasOutput2<T, Clause1_Clause0_Output>,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out
index e3121fdc1..97638a5b8 100644
--- a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out
+++ b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out
@@ -29,10 +29,8 @@ where
     let @0: (); // return
     let _x@1: test_crate::HashMap<S>[@TraitClause0]; // arg #1
     let _k@2: Q; // arg #2
-    let @3: (); // anonymous local
 
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     drop _k@2
     drop _x@1
     @0 := ()
@@ -48,10 +46,8 @@ where
     let @0: (); // return
     let _x@1: test_crate::HashMap<S>[@TraitClause0]; // arg #1
     let _k@2: Q; // arg #2
-    let @3: (); // anonymous local
 
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     drop _k@2
     drop _x@1
     @0 := ()
@@ -65,7 +61,6 @@ fn test_crate::test1(@1: test_crate::HashMap<()>[core::marker::Sized<()>])
     let @2: (); // anonymous local
     let @3: test_crate::HashMap<()>[core::marker::Sized<()>]; // anonymous local
     let @4: (); // anonymous local
-    let @5: (); // anonymous local
 
     @3 := move (map@1)
     @4 := ()
@@ -73,8 +68,7 @@ fn test_crate::test1(@1: test_crate::HashMap<()>[core::marker::Sized<()>])
     drop @4
     drop @3
     drop @2
-    @5 := ()
-    @0 := move (@5)
+    @0 := ()
     @0 := ()
     return
 }
@@ -86,7 +80,6 @@ fn test_crate::test2(@1: test_crate::HashMap<()>[core::marker::Sized<()>])
     let @2: (); // anonymous local
     let @3: test_crate::HashMap<()>[core::marker::Sized<()>]; // anonymous local
     let @4: (); // anonymous local
-    let @5: (); // anonymous local
 
     @3 := move (map@1)
     @4 := ()
@@ -94,8 +87,7 @@ fn test_crate::test2(@1: test_crate::HashMap<()>[core::marker::Sized<()>])
     drop @4
     drop @3
     drop @2
-    @5 := ()
-    @0 := move (@5)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/simple/call-method-via-supertrait-bound.out b/charon/tests/ui/simple/call-method-via-supertrait-bound.out
index bf3722915..b19799884 100644
--- a/charon/tests/ui/simple/call-method-via-supertrait-bound.out
+++ b/charon/tests/ui/simple/call-method-via-supertrait-bound.out
@@ -21,10 +21,8 @@ where
 {
     let @0: (); // return
     let self@1: &'_ (T); // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -46,15 +44,13 @@ where
     let x@1: T; // arg #1
     let @2: (); // anonymous local
     let @3: &'_ (T); // anonymous local
-    let @4: (); // anonymous local
 
     @3 := &x@1
     @2 := test_crate::{impl test_crate::HasMethod for T}::method<'_, T>[@TraitClause0, @TraitClause1::parent_clause0](move (@3))
     drop @3
     @fake_read(@2)
     drop @2
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     drop x@1
     @0 := ()
     return
diff --git a/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out b/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out
index e32a62a3b..69655e164 100644
--- a/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out
+++ b/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out
@@ -27,10 +27,8 @@ impl<T> test_crate::{impl test_crate::Trait for T}<T> : test_crate::Trait<T>
 fn test_crate::main()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/simple/fewer-clauses-in-method-impl.out b/charon/tests/ui/simple/fewer-clauses-in-method-impl.out
index 8f3c3db12..951bfbe16 100644
--- a/charon/tests/ui/simple/fewer-clauses-in-method-impl.out
+++ b/charon/tests/ui/simple/fewer-clauses-in-method-impl.out
@@ -24,10 +24,8 @@ where
     [@TraitClause1]: core::clone::Clone<T>,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/simple/generic-impl-with-defaulted-method-with-clause-with-assoc-ty.out b/charon/tests/ui/simple/generic-impl-with-defaulted-method-with-clause-with-assoc-ty.out
index 7bb8e2027..71818a953 100644
--- a/charon/tests/ui/simple/generic-impl-with-defaulted-method-with-clause-with-assoc-ty.out
+++ b/charon/tests/ui/simple/generic-impl-with-defaulted-method-with-clause-with-assoc-ty.out
@@ -26,10 +26,8 @@ where
     [@TraitClause1]: test_crate::HasType<core::option::Option<T>[@TraitClause0], Clause1_Type>,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -46,10 +44,8 @@ where
     [@TraitClause0]: test_crate::HasType<Self, Clause0_Type>,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/simple/generic-impl-with-defaulted-method.out b/charon/tests/ui/simple/generic-impl-with-defaulted-method.out
index fe855b8a0..2c32c4448 100644
--- a/charon/tests/ui/simple/generic-impl-with-defaulted-method.out
+++ b/charon/tests/ui/simple/generic-impl-with-defaulted-method.out
@@ -21,10 +21,8 @@ where
 {
     let @0: (); // return
     let self@1: &'_ (core::option::Option<T>[@TraitClause0]); // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -40,10 +38,8 @@ fn test_crate::BoolTrait::foo<'_0, Self>(@1: &'_0 (Self))
 {
     let @0: (); // return
     let self@1: &'_ (Self); // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/simple/generic-impl-with-method.out b/charon/tests/ui/simple/generic-impl-with-method.out
index 7e49226a5..0df419994 100644
--- a/charon/tests/ui/simple/generic-impl-with-method.out
+++ b/charon/tests/ui/simple/generic-impl-with-method.out
@@ -13,10 +13,8 @@ where
 {
     let @0: (); // return
     let self@1: &'_ (T); // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/simple/opaque-trait-with-clause-in-method.out b/charon/tests/ui/simple/opaque-trait-with-clause-in-method.out
index 7bbda6f24..cbb58cac3 100644
--- a/charon/tests/ui/simple/opaque-trait-with-clause-in-method.out
+++ b/charon/tests/ui/simple/opaque-trait-with-clause-in-method.out
@@ -10,10 +10,8 @@ where
     [@TraitClause1]: test_crate::opaque::Iterator<T>,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out
index e27e41498..3dba99ac0 100644
--- a/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out
+++ b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out
@@ -44,10 +44,8 @@ where
 {
     let @0: (); // return
     let @1: F; // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     drop @1
     @0 := ()
     return
@@ -57,12 +55,10 @@ fn test_crate::flibidi()
 {
     let @0: (); // return
     let @1: (); // anonymous local
-    let @2: (); // anonymous local
 
     @1 := test_crate::call<'_, fn<'a>(&'a (())) -> &'a (())>[core::marker::Sized<fn<'a>(&'a (())) -> &'a (())>, core::ops::function::Fn<fn<'a>(&'a (())) -> &'a (()), (&'_ (())), &'_ (())>](const (test_crate::flabada<'_>))
     drop @1
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/simple/quantified-trait-type-constraint.out b/charon/tests/ui/simple/quantified-trait-type-constraint.out
index ef41c5074..8d78fa903 100644
--- a/charon/tests/ui/simple/quantified-trait-type-constraint.out
+++ b/charon/tests/ui/simple/quantified-trait-type-constraint.out
@@ -13,10 +13,8 @@ where
     [@TraitClause1]: for<'_0> test_crate::Trait<'_0_0, T, &'_ (())>,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/simple/supertrait-impl-with-assoc-type-constraint.out b/charon/tests/ui/simple/supertrait-impl-with-assoc-type-constraint.out
index 10c03f743..8923c0d0f 100644
--- a/charon/tests/ui/simple/supertrait-impl-with-assoc-type-constraint.out
+++ b/charon/tests/ui/simple/supertrait-impl-with-assoc-type-constraint.out
@@ -33,10 +33,8 @@ where
 fn test_crate::main()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/skip-borrowck.out b/charon/tests/ui/skip-borrowck.out
index e67926095..5c206ffea 100644
--- a/charon/tests/ui/skip-borrowck.out
+++ b/charon/tests/ui/skip-borrowck.out
@@ -54,11 +54,6 @@ fn test_crate::choose_test()
     let @17: (); // anonymous local
     let @18: bool; // anonymous local
     let @19: i32; // anonymous local
-    let @20: (); // anonymous local
-    let @21: (); // anonymous local
-    let @22: (); // anonymous local
-    let @23: (); // anonymous local
-    let @24: (); // anonymous local
 
     x@1 := const (0 : i32)
     @fake_read(x@1)
@@ -84,8 +79,6 @@ fn test_crate::choose_test()
         panic(core::panicking::panic)
     }
     drop @10
-    @20 := ()
-    @8 := move (@20)
     drop @9
     drop @8
     // drop(z)
@@ -98,8 +91,6 @@ fn test_crate::choose_test()
         panic(core::panicking::panic)
     }
     drop @13
-    @21 := ()
-    @11 := move (@21)
     drop @12
     drop @11
     @16 := copy (y@2)
@@ -111,8 +102,6 @@ fn test_crate::choose_test()
         panic(core::panicking::panic)
     }
     drop @16
-    @22 := ()
-    @14 := move (@22)
     drop @15
     drop @14
     @19 := copy (*(z@3))
@@ -124,12 +113,9 @@ fn test_crate::choose_test()
         panic(core::panicking::panic)
     }
     drop @19
-    @23 := ()
-    @17 := move (@23)
     drop @18
     drop @17
-    @24 := ()
-    @0 := move (@24)
+    @0 := ()
     drop z@3
     drop y@2
     drop x@1
diff --git a/charon/tests/ui/statics.out b/charon/tests/ui/statics.out
index 0dbb8c99a..2c02b8e4f 100644
--- a/charon/tests/ui/statics.out
+++ b/charon/tests/ui/statics.out
@@ -21,7 +21,6 @@ fn test_crate::constant()
     let @6: usize; // anonymous local
     let @7: usize; // anonymous local
     let @8: usize; // anonymous local
-    let @9: (); // anonymous local
 
     @6 := test_crate::constant::CONST
     _val@1 := move (@6)
@@ -34,8 +33,7 @@ fn test_crate::constant()
     @5 := move (@8)
     _ref_mut@4 := &mut @5
     @fake_read(_ref_mut@4)
-    @9 := ()
-    @0 := move (@9)
+    @0 := ()
     drop @5
     drop _ref_mut@4
     drop @3
@@ -67,7 +65,6 @@ fn test_crate::shared_static()
     let @7: &'_ (usize); // anonymous local
     let @8: &'_ (usize); // anonymous local
     let @9: &'_ (usize); // anonymous local
-    let @10: (); // anonymous local
 
     @7 := &test_crate::shared_static::SHARED_STATIC
     @2 := move (@7)
@@ -82,8 +79,7 @@ fn test_crate::shared_static()
     @6 := move (@9)
     _ptr@5 := &raw const *(@6)
     @fake_read(_ptr@5)
-    @10 := ()
-    @0 := move (@10)
+    @0 := ()
     drop @6
     drop _ptr@5
     drop @4
@@ -121,7 +117,6 @@ fn test_crate::mut_static()
     let @13: *mut usize; // anonymous local
     let @14: *mut usize; // anonymous local
     let @15: *mut usize; // anonymous local
-    let @16: (); // anonymous local
 
     @11 := &raw mut test_crate::mut_static::MUT_STATIC
     @2 := move (@11)
@@ -144,8 +139,7 @@ fn test_crate::mut_static()
     @10 := move (@15)
     _ptr_mut@9 := &raw mut *(@10)
     @fake_read(_ptr_mut@9)
-    @16 := ()
-    @0 := move (@16)
+    @0 := ()
     drop @10
     drop _ptr_mut@9
     drop @8
@@ -175,10 +169,8 @@ fn test_crate::non_copy_static::{test_crate::non_copy_static::Foo}::method<'_0>(
 {
     let @0: (); // return
     let self@1: &'_ (test_crate::non_copy_static::Foo); // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/string-literal.out b/charon/tests/ui/string-literal.out
index 89e3b63a9..1ef3bfc45 100644
--- a/charon/tests/ui/string-literal.out
+++ b/charon/tests/ui/string-literal.out
@@ -40,7 +40,6 @@ fn test_crate::main()
     let _s@1: alloc::string::String; // local
     let @2: &'_ (Str); // anonymous local
     let @3: &'_ (Str); // anonymous local
-    let @4: (); // anonymous local
 
     @3 := const ("Hello")
     @2 := &*(@3)
@@ -48,8 +47,7 @@ fn test_crate::main()
     drop @2
     @fake_read(_s@1)
     drop @3
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     drop _s@1
     drop _s@1
     @0 := ()
diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out
index f2dc07410..17a7c32b7 100644
--- a/charon/tests/ui/traits.out
+++ b/charon/tests/ui/traits.out
@@ -527,10 +527,8 @@ fn test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::f<'_0, '_1
     let @0: (); // return
     let @1: &'_ mut (u64); // arg #1
     let @2: &'_ (Array<u8, 32 : usize>); // arg #2
-    let @3: (); // anonymous local
 
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     @0 := ()
     return
 }
@@ -565,10 +563,8 @@ where
 {
     let @0: (); // return
     let @1: @TraitClause1::W; // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     drop @1
     @0 := ()
     return
@@ -597,10 +593,8 @@ where
 {
     let @0: (); // return
     let _x@1: &'_ (T); // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -613,10 +607,8 @@ where
 {
     let @0: (); // return
     let _x@1: u32; // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
@@ -682,10 +674,8 @@ where
     @TraitClause2::W = @TraitClause3::W,
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -1011,10 +1001,8 @@ where
 {
     let @0: (); // return
     let @1: F; // arg #1
-    let @2: (); // anonymous local
 
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     drop @1
     @0 := ()
     return
@@ -1024,12 +1012,10 @@ fn test_crate::flibidi()
 {
     let @0: (); // return
     let @1: (); // anonymous local
-    let @2: (); // anonymous local
 
     @1 := test_crate::call<'_, fn<'a>(&'a (())) -> test_crate::Wrapper<(bool, &'a (()))>[core::marker::Sized<(bool, &'a (()))>]>[core::marker::Sized<fn<'a>(&'a (())) -> test_crate::Wrapper<(bool, &'a (()))>[core::marker::Sized<(bool, &'a (()))>]>, core::ops::function::Fn<fn<'a>(&'a (())) -> test_crate::Wrapper<(bool, &'a (()))>[core::marker::Sized<(bool, &'a (()))>], (&'_ (()))>](const (test_crate::flabada<'_>))
     drop @1
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/type_inference_is_order_dependent.out b/charon/tests/ui/type_inference_is_order_dependent.out
index 5019a8572..9fbe6ec17 100644
--- a/charon/tests/ui/type_inference_is_order_dependent.out
+++ b/charon/tests/ui/type_inference_is_order_dependent.out
@@ -83,7 +83,6 @@ where
     let @10: &'_ (U); // anonymous local
     let @11: &'_ (U); // anonymous local
     let @12: U; // anonymous local
-    let @13: (); // anonymous local
 
     @5 := [const (""), const ("
 "); 2 : usize]
@@ -111,8 +110,7 @@ where
     drop @5
     drop @4
     drop @1
-    @13 := ()
-    @0 := move (@13)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/typenum.out b/charon/tests/ui/typenum.out
index bd2b92610..41c49a264 100644
--- a/charon/tests/ui/typenum.out
+++ b/charon/tests/ui/typenum.out
@@ -15,10 +15,8 @@ type test_crate::LongType = test_crate::UInt<test_crate::UInt<test_crate::UInt<t
 fn test_crate::foo<T>()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }
@@ -27,12 +25,10 @@ fn test_crate::main()
 {
     let @0: (); // return
     let @1: (); // anonymous local
-    let @2: (); // anonymous local
 
     @1 := test_crate::foo<test_crate::UInt<test_crate::UInt<test_crate::UInt<test_crate::UInt<test_crate::UInt<test_crate::UInt<test_crate::UInt<test_crate::UInt<test_crate::UInt<test_crate::UTerm, test_crate::B0>, test_crate::B0>, test_crate::B0>, test_crate::B0>, test_crate::B0>, test_crate::B0>, test_crate::B0>, test_crate::B0>, test_crate::B0>>()
     drop @1
-    @2 := ()
-    @0 := move (@2)
+    @0 := ()
     @0 := ()
     return
 }
diff --git a/charon/tests/ui/ullbc-control-flow.out b/charon/tests/ui/ullbc-control-flow.out
index 324dc0814..ecc309ec5 100644
--- a/charon/tests/ui/ullbc-control-flow.out
+++ b/charon/tests/ui/ullbc-control-flow.out
@@ -168,42 +168,32 @@ fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize
     let @6: core::ops::range::Range<i32>[core::marker::Sized<i32>]; // anonymous local
     let iter@7: core::ops::range::Range<i32>[core::marker::Sized<i32>]; // local
     let @8: (); // anonymous local
-    let @9: (); // anonymous local
-    let @10: core::option::Option<i32>[core::marker::Sized<i32>]; // anonymous local
+    let @9: core::option::Option<i32>[core::marker::Sized<i32>]; // anonymous local
+    let @10: &'_ mut (core::ops::range::Range<i32>[core::marker::Sized<i32>]); // anonymous local
     let @11: &'_ mut (core::ops::range::Range<i32>[core::marker::Sized<i32>]); // anonymous local
-    let @12: &'_ mut (core::ops::range::Range<i32>[core::marker::Sized<i32>]); // anonymous local
-    let @13: isize; // anonymous local
-    let @14: (); // anonymous local
+    let @12: isize; // anonymous local
+    let @13: (); // anonymous local
+    let @14: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // anonymous local
     let @15: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // anonymous local
-    let @16: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // anonymous local
-    let @17: usize; // anonymous local
-    let iter@18: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // local
-    let @19: (); // anonymous local
-    let @20: core::option::Option<usize>[core::marker::Sized<usize>]; // anonymous local
+    let @16: usize; // anonymous local
+    let iter@17: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // local
+    let @18: (); // anonymous local
+    let @19: core::option::Option<usize>[core::marker::Sized<usize>]; // anonymous local
+    let @20: &'_ mut (core::ops::range::Range<usize>[core::marker::Sized<usize>]); // anonymous local
     let @21: &'_ mut (core::ops::range::Range<usize>[core::marker::Sized<usize>]); // anonymous local
-    let @22: &'_ mut (core::ops::range::Range<usize>[core::marker::Sized<usize>]); // anonymous local
-    let @23: isize; // anonymous local
+    let @22: isize; // anonymous local
+    let @23: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // anonymous local
     let @24: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // anonymous local
-    let @25: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // anonymous local
-    let @26: usize; // anonymous local
-    let iter@27: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // local
-    let @28: (); // anonymous local
-    let @29: core::option::Option<usize>[core::marker::Sized<usize>]; // anonymous local
+    let @25: usize; // anonymous local
+    let iter@26: core::ops::range::Range<usize>[core::marker::Sized<usize>]; // local
+    let @27: (); // anonymous local
+    let @28: core::option::Option<usize>[core::marker::Sized<usize>]; // anonymous local
+    let @29: &'_ mut (core::ops::range::Range<usize>[core::marker::Sized<usize>]); // anonymous local
     let @30: &'_ mut (core::ops::range::Range<usize>[core::marker::Sized<usize>]); // anonymous local
-    let @31: &'_ mut (core::ops::range::Range<usize>[core::marker::Sized<usize>]); // anonymous local
-    let @32: isize; // anonymous local
-    let @33: (); // anonymous local
-    let @34: bool; // anonymous local
-    let @35: usize; // anonymous local
-    let @36: (); // anonymous local
-    let @37: (); // anonymous local
-    let @38: (); // anonymous local
-    let @39: (); // anonymous local
-    let @40: (); // anonymous local
-    let @41: (); // anonymous local
-    let @42: (); // anonymous local
-    let @43: (); // anonymous local
-    let @44: (); // anonymous local
+    let @31: isize; // anonymous local
+    let @32: (); // anonymous local
+    let @33: bool; // anonymous local
+    let @34: usize; // anonymous local
 
     bb0: {
         s@3 := const (0 : usize);
@@ -217,148 +207,130 @@ fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize
     }
 
     bb1: {
-        @12 := &mut iter@7;
-        @11 := &two-phase-mut *(@12);
-        @10 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, i32>[core::marker::Sized<i32>, core::iter::range::{impl core::iter::range::Step for i32}#40](move (@11));
-        @storage_dead(@11);
-        @fake_read(@10);
-        @13 := @discriminant(@10);
-        switch move (@13) -> 0 : isize: bb2, 1 : isize: bb3, otherwise: bb4;
+        @11 := &mut iter@7;
+        @10 := &two-phase-mut *(@11);
+        @9 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, i32>[core::marker::Sized<i32>, core::iter::range::{impl core::iter::range::Step for i32}#40](move (@10));
+        @storage_dead(@10);
+        @fake_read(@9);
+        @12 := @discriminant(@9);
+        switch move (@12) -> 0 : isize: bb2, 1 : isize: bb3, otherwise: bb4;
     }
 
     bb2: {
-        @36 := ();
-        @4 := move (@36);
-        @storage_dead(@12);
-        @storage_dead(@10);
+        @storage_dead(@11);
         @storage_dead(@9);
+        @storage_dead(@8);
         @storage_dead(@7);
         @storage_dead(@5);
         @storage_dead(@4);
-        @17 := copy (step_out@1);
-        @16 := core::ops::range::Range { start: const (0 : usize), end: move (@17) };
-        @storage_dead(@17);
-        @15 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::ops::range::Range<usize>[core::marker::Sized<usize>]>[core::marker::Sized<core::ops::range::Range<usize>[core::marker::Sized<usize>]>, core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6<usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43]](move (@16));
+        @16 := copy (step_out@1);
+        @15 := core::ops::range::Range { start: const (0 : usize), end: move (@16) };
         @storage_dead(@16);
-        @fake_read(@15);
-        iter@18 := move (@15);
+        @14 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::ops::range::Range<usize>[core::marker::Sized<usize>]>[core::marker::Sized<core::ops::range::Range<usize>[core::marker::Sized<usize>]>, core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6<usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43]](move (@15));
+        @storage_dead(@15);
+        @fake_read(@14);
+        iter@17 := move (@14);
         goto bb5;
     }
 
     bb3: {
         s@3 := copy (s@3) + const (1 : usize);
-        @37 := ();
-        @9 := move (@37);
-        @storage_dead(@12);
-        @storage_dead(@10);
+        @storage_dead(@11);
         @storage_dead(@9);
-        @38 := ();
-        @8 := move (@38);
+        @storage_dead(@8);
         goto bb1;
     }
 
     bb4: {
-        @fake_read(@10);
+        @fake_read(@9);
         undefined_behavior;
     }
 
     bb5: {
-        @22 := &mut iter@18;
-        @21 := &two-phase-mut *(@22);
-        @20 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43](move (@21));
-        @storage_dead(@21);
-        @fake_read(@20);
-        @23 := @discriminant(@20);
-        switch move (@23) -> 0 : isize: bb6, 1 : isize: bb7, otherwise: bb8;
+        @21 := &mut iter@17;
+        @20 := &two-phase-mut *(@21);
+        @19 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43](move (@20));
+        @storage_dead(@20);
+        @fake_read(@19);
+        @22 := @discriminant(@19);
+        switch move (@22) -> 0 : isize: bb6, 1 : isize: bb7, otherwise: bb8;
     }
 
     bb6: {
-        @39 := ();
-        @14 := move (@39);
         // Test comment
-        @storage_dead(@22);
-        @storage_dead(@20);
+        @storage_dead(@21);
         @storage_dead(@19);
         @storage_dead(@18);
-        @storage_dead(@15);
+        @storage_dead(@17);
         @storage_dead(@14);
+        @storage_dead(@13);
         @0 := copy (s@3);
         @storage_dead(@3);
         return;
     }
 
     bb7: {
-        @26 := copy (step_in@2);
-        @25 := core::ops::range::Range { start: const (0 : usize), end: move (@26) };
-        @storage_dead(@26);
-        @24 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::ops::range::Range<usize>[core::marker::Sized<usize>]>[core::marker::Sized<core::ops::range::Range<usize>[core::marker::Sized<usize>]>, core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6<usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43]](move (@25));
+        @25 := copy (step_in@2);
+        @24 := core::ops::range::Range { start: const (0 : usize), end: move (@25) };
         @storage_dead(@25);
-        @fake_read(@24);
-        iter@27 := move (@24);
+        @23 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<core::ops::range::Range<usize>[core::marker::Sized<usize>]>[core::marker::Sized<core::ops::range::Range<usize>[core::marker::Sized<usize>]>, core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6<usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43]](move (@24));
+        @storage_dead(@24);
+        @fake_read(@23);
+        iter@26 := move (@23);
         goto bb9;
     }
 
     bb8: {
-        @fake_read(@20);
+        @fake_read(@19);
         undefined_behavior;
     }
 
     bb9: {
-        @31 := &mut iter@27;
-        @30 := &two-phase-mut *(@31);
-        @29 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43](move (@30));
-        @storage_dead(@30);
-        @fake_read(@29);
-        @32 := @discriminant(@29);
-        switch move (@32) -> 0 : isize: bb10, 1 : isize: bb11, otherwise: bb12;
+        @30 := &mut iter@26;
+        @29 := &two-phase-mut *(@30);
+        @28 := core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_, usize>[core::marker::Sized<usize>, core::iter::range::{impl core::iter::range::Step for usize}#43](move (@29));
+        @storage_dead(@29);
+        @fake_read(@28);
+        @31 := @discriminant(@28);
+        switch move (@31) -> 0 : isize: bb10, 1 : isize: bb11, otherwise: bb12;
     }
 
     bb10: {
-        @40 := ();
-        @19 := move (@40);
-        @storage_dead(@31);
-        @storage_dead(@29);
+        @storage_dead(@30);
         @storage_dead(@28);
         @storage_dead(@27);
-        @storage_dead(@24);
-        @storage_dead(@22);
-        @storage_dead(@20);
+        @storage_dead(@26);
+        @storage_dead(@23);
+        @storage_dead(@21);
         @storage_dead(@19);
-        @41 := ();
-        @8 := move (@41);
+        @storage_dead(@18);
         goto bb5;
     }
 
     bb11: {
         s@3 := copy (s@3) + const (1 : usize);
-        @35 := copy (s@3);
-        @34 := move (@35) >= const (1 : usize);
-        if move (@34) -> bb13 else -> bb14;
+        @34 := copy (s@3);
+        @33 := move (@34) >= const (1 : usize);
+        if move (@33) -> bb13 else -> bb14;
     }
 
     bb12: {
-        @fake_read(@29);
+        @fake_read(@28);
         undefined_behavior;
     }
 
     bb13: {
-        @storage_dead(@35);
-        @42 := ();
-        @33 := move (@42);
         @storage_dead(@34);
         @storage_dead(@33);
-        @43 := ();
-        @28 := move (@43);
-        @storage_dead(@31);
-        @storage_dead(@29);
+        @storage_dead(@32);
+        @storage_dead(@30);
         @storage_dead(@28);
-        @44 := ();
-        @8 := move (@44);
+        @storage_dead(@27);
         goto bb9;
     }
 
     bb14: {
-        @storage_dead(@35);
+        @storage_dead(@34);
         panic(core::panicking::panic);
     }
 }
diff --git a/charon/tests/ui/unions.out b/charon/tests/ui/unions.out
index c5e73c778..83d6c1272 100644
--- a/charon/tests/ui/unions.out
+++ b/charon/tests/ui/unions.out
@@ -12,19 +12,14 @@ fn test_crate::use_union()
     let one@1: test_crate::Foo; // local
     let @2: (); // anonymous local
     let _two@3: Array<u32, 2 : usize>; // local
-    let @4: (); // anonymous local
-    let @5: (); // anonymous local
 
     one@1 := test_crate::Foo { one: const (42 : u64) }
     @fake_read(one@1)
     (one@1).one := const (43 : u64)
-    @4 := ()
-    @2 := move (@4)
     drop @2
     _two@3 := copy ((one@1).two)
     @fake_read(_two@3)
-    @5 := ()
-    @0 := move (@5)
+    @0 := ()
     drop _two@3
     drop one@1
     @0 := ()
diff --git a/charon/tests/ui/unsafe.out b/charon/tests/ui/unsafe.out
index a4b22e85f..b0222d0d8 100644
--- a/charon/tests/ui/unsafe.out
+++ b/charon/tests/ui/unsafe.out
@@ -16,7 +16,6 @@ fn test_crate::call_unsafe_fn()
     let x@1: *const u32; // local
     let @2: u32; // anonymous local
     let @3: *const u32; // anonymous local
-    let @4: (); // anonymous local
 
     x@1 := core::ptr::null<u32>[core::ptr::metadata::Thin<u32>]()
     @fake_read(x@1)
@@ -25,8 +24,7 @@ fn test_crate::call_unsafe_fn()
     drop @3
     @fake_read(@2)
     drop @2
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     drop x@1
     @0 := ()
     return
@@ -37,15 +35,13 @@ fn test_crate::deref_raw_ptr()
     let @0: (); // return
     let x@1: *const u32; // local
     let @2: u32; // anonymous local
-    let @3: (); // anonymous local
 
     x@1 := core::ptr::null<u32>[core::ptr::metadata::Thin<u32>]()
     @fake_read(x@1)
     @2 := copy (*(x@1))
     @fake_read(@2)
     drop @2
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     drop x@1
     @0 := ()
     return
@@ -70,14 +66,12 @@ fn test_crate::access_mutable_static()
     let @0: (); // return
     let @1: *mut usize; // anonymous local
     let @2: *mut usize; // anonymous local
-    let @3: (); // anonymous local
 
     @2 := &raw mut test_crate::COUNTER
     @1 := move (@2)
     *(@1) := copy (*(@1)) + const (1 : usize)
     drop @1
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     @0 := ()
     return
 }
@@ -93,14 +87,12 @@ fn test_crate::access_union_field()
     let @0: (); // return
     let one@1: test_crate::Foo; // local
     let _two@2: Array<u32, 2 : usize>; // local
-    let @3: (); // anonymous local
 
     one@1 := test_crate::Foo { one: const (42 : u64) }
     @fake_read(one@1)
     _two@2 := copy ((one@1).two)
     @fake_read(_two@2)
-    @3 := ()
-    @0 := move (@3)
+    @0 := ()
     drop _two@2
     drop one@1
     @0 := ()
diff --git a/charon/tests/ui/unsize.out b/charon/tests/ui/unsize.out
index d5878631d..39c229843 100644
--- a/charon/tests/ui/unsize.out
+++ b/charon/tests/ui/unsize.out
@@ -43,7 +43,6 @@ fn test_crate::foo()
     let @20: alloc::rc::Rc<alloc::string::String, alloc::alloc::Global>[core::marker::Sized<alloc::alloc::Global>]; // anonymous local
     let @21: alloc::string::String; // anonymous local
     let @22: &'_ (alloc::string::String); // anonymous local
-    let @23: (); // anonymous local
 
     array@1 := [const (0 : i32), const (0 : i32); 2 : usize]
     @fake_read(array@1)
@@ -103,8 +102,7 @@ fn test_crate::foo()
     @fake_read(@19)
     drop @19
     drop @19
-    @23 := ()
-    @0 := move (@23)
+    @0 := ()
     drop string@11
     drop string@11
     drop array@1
diff --git a/charon/tests/ui/unsupported/issue-79-bound-regions.out b/charon/tests/ui/unsupported/issue-79-bound-regions.out
index 1331a3ecc..5cf799f79 100644
--- a/charon/tests/ui/unsupported/issue-79-bound-regions.out
+++ b/charon/tests/ui/unsupported/issue-79-bound-regions.out
@@ -35,7 +35,6 @@ fn test_crate::main()
     let @6: &'_ mut (core::slice::iter::Iter<'_, i32>[core::marker::Sized<i32>]); // anonymous local
     let @7: core::slice::iter::Iter<'_, i32>[core::marker::Sized<i32>]; // anonymous local
     let @8: &'_ (Slice<i32>); // anonymous local
-    let @9: (); // anonymous local
 
     @4 := [const (0 : i32); 1 : usize]
     @3 := &@4
@@ -53,8 +52,7 @@ fn test_crate::main()
     @fake_read(@5)
     drop @7
     drop @5
-    @9 := ()
-    @0 := move (@9)
+    @0 := ()
     drop @4
     drop slice@1
     @0 := ()