diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs
index d82dda80cc05..d3f2afc15d31 100644
--- a/kani-compiler/src/kani_middle/transform/body.rs
+++ b/kani-compiler/src/kani_middle/transform/body.rs
@@ -88,16 +88,20 @@ impl MutableBody {
 
     pub fn new_str_operand(&mut self, msg: &str, span: Span) -> Operand {
         let literal = MirConst::from_str(msg);
-        Operand::Constant(ConstOperand { span, user_ty: None, const_: literal })
+        self.new_const_operand(literal, span)
     }
 
-    pub fn new_const_operand(&mut self, val: u128, uint_ty: UintTy, span: Span) -> Operand {
+    pub fn new_uint_operand(&mut self, val: u128, uint_ty: UintTy, span: Span) -> Operand {
         let literal = MirConst::try_from_uint(val, uint_ty).unwrap();
+        self.new_const_operand(literal, span)
+    }
+
+    fn new_const_operand(&mut self, literal: MirConst, span: Span) -> Operand {
         Operand::Constant(ConstOperand { span, user_ty: None, const_: literal })
     }
 
     /// Create a raw pointer of `*mut type` and return a new local where that value is stored.
-    pub fn new_cast_ptr(
+    pub fn insert_ptr_cast(
         &mut self,
         from: Operand,
         pointee_ty: Ty,
@@ -108,13 +112,13 @@ impl MutableBody {
         assert!(from.ty(self.locals()).unwrap().kind().is_raw_ptr());
         let target_ty = Ty::new_ptr(pointee_ty, mutability);
         let rvalue = Rvalue::Cast(CastKind::PtrToPtr, from, target_ty);
-        self.new_assignment(rvalue, source, position)
+        self.insert_assignment(rvalue, source, position)
     }
 
     /// Add a new assignment for the given binary operation.
     ///
     /// Return the local where the result is saved.
-    pub fn new_binary_op(
+    pub fn insert_binary_op(
         &mut self,
         bin_op: BinOp,
         lhs: Operand,
@@ -123,13 +127,13 @@ impl MutableBody {
         position: InsertPosition,
     ) -> Local {
         let rvalue = Rvalue::BinaryOp(bin_op, lhs, rhs);
-        self.new_assignment(rvalue, source, position)
+        self.insert_assignment(rvalue, source, position)
     }
 
     /// Add a new assignment.
     ///
-    /// Return  local where the result is saved.
-    pub fn new_assignment(
+    /// Return the local where the result is saved.
+    pub fn insert_assignment(
         &mut self,
         rvalue: Rvalue,
         source: &mut SourceInstruction,
@@ -146,9 +150,10 @@ impl MutableBody {
     /// Add a new assert to the basic block indicated by the given index.
     ///
     /// The new assertion will have the same span as the source instruction, and the basic block
-    /// will be split. The source instruction will be adjusted to point to the first instruction in
-    /// the new basic block.
-    pub fn add_check(
+    /// will be split. If `InsertPosition` is `InsertPosition::Before`, `source` will point to the
+    /// same instruction as before. If `InsertPosition` is `InsertPosition::After`, `source` will
+    /// point to the new terminator.
+    pub fn insert_check(
         &mut self,
         tcx: TyCtxt,
         check_type: &CheckType,
@@ -183,7 +188,7 @@ impl MutableBody {
                     unwind: UnwindAction::Terminate,
                 };
                 let terminator = Terminator { kind, span };
-                self.split_bb(source, position, terminator);
+                self.insert_terminator(source, position, terminator);
             }
             CheckType::Panic | CheckType::NoCore => {
                 tcx.sess
@@ -199,10 +204,11 @@ impl MutableBody {
 
     /// Add a new call to the basic block indicated by the given index.
     ///
-    /// The new call will have the same span as the source instruction, and the basic block
-    /// will be split. The source instruction will be adjusted to point to the first instruction in
-    /// the new basic block.
-    pub fn add_call(
+    /// The new call will have the same span as the source instruction, and the basic block will be
+    /// split. If `InsertPosition` is `InsertPosition::Before`, `source` will point to the same
+    /// instruction as before. If `InsertPosition` is `InsertPosition::After`, `source` will point
+    /// to the new terminator.
+    pub fn insert_call(
         &mut self,
         callee: &Instance,
         source: &mut SourceInstruction,
@@ -222,13 +228,14 @@ impl MutableBody {
             unwind: UnwindAction::Terminate,
         };
         let terminator = Terminator { kind, span };
-        self.split_bb(source, position, terminator);
+        self.insert_terminator(source, position, terminator);
     }
 
-    /// Split a basic block and use the new terminator in the basic block that was split.
-    ///
-    /// The source is updated to point to the same instruction which is now in the new basic block.
-    pub fn split_bb(
+    /// Split a basic block and use the new terminator in the basic block that was split. If
+    /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as
+    /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the new
+    /// terminator.
+    fn split_bb(
         &mut self,
         source: &mut SourceInstruction,
         position: InsertPosition,
@@ -245,6 +252,7 @@ impl MutableBody {
     }
 
     /// Split a basic block right before the source location.
+    /// `source` will point to the same instruction as before after the function is done.
     fn split_bb_before(&mut self, source: &mut SourceInstruction, new_term: Terminator) {
         let new_bb_idx = self.blocks.len();
         let (idx, bb) = match source {
@@ -268,6 +276,7 @@ impl MutableBody {
     }
 
     /// Split a basic block right after the source location.
+    /// `source` will point to the new terminator after the function is done.
     fn split_bb_after(&mut self, source: &mut SourceInstruction, mut new_term: Terminator) {
         let new_bb_idx = self.blocks.len();
         match source {
@@ -275,39 +284,69 @@ impl MutableBody {
             // and move the remaining statements into the new one.
             SourceInstruction::Statement { idx, bb } => {
                 let (orig_idx, orig_bb) = (*idx, *bb);
-                *idx = 0;
-                *bb = new_bb_idx;
                 let old_term = mem::replace(&mut self.blocks[orig_bb].terminator, new_term);
                 let bb_stmts = &mut self.blocks[orig_bb].statements;
                 let remaining = bb_stmts.split_off(orig_idx + 1);
                 let new_bb = BasicBlock { statements: remaining, terminator: old_term };
                 self.blocks.push(new_bb);
+                // Update the source to point at the terminator.
+                *source = SourceInstruction::Terminator { bb: orig_bb };
             }
             // Make the terminator at `source` point at the new block,
             // the terminator of which is a simple Goto instruction.
             SourceInstruction::Terminator { bb } => {
-                let current_terminator = &mut self.blocks.get_mut(*bb).unwrap().terminator;
-                // Kani can only instrument function calls like this.
-                match (&mut current_terminator.kind, &mut new_term.kind) {
-                    (
-                        TerminatorKind::Call { target: Some(target_bb), .. },
-                        TerminatorKind::Call { target: Some(new_target_bb), .. },
-                    ) => {
-                        // Set the new terminator to point where previous terminator pointed.
-                        *new_target_bb = *target_bb;
-                        // Point the current terminator to the new terminator's basic block.
-                        *target_bb = new_bb_idx;
-                        // Update the current poisition.
-                        *bb = new_bb_idx;
-                        self.blocks.push(BasicBlock { statements: vec![], terminator: new_term });
-                    }
-                    _ => unimplemented!("Kani can only split blocks after calls."),
-                };
+                let current_term = &mut self.blocks.get_mut(*bb).unwrap().terminator;
+                let target_bb = get_mut_target_ref(current_term);
+                let new_target_bb = get_mut_target_ref(&mut new_term);
+                // Set the new terminator to point where previous terminator pointed.
+                *new_target_bb = *target_bb;
+                // Point the current terminator to the new terminator's basic block.
+                *target_bb = new_bb_idx;
+                // Update the source to point at the terminator.
+                *bb = new_bb_idx;
+                self.blocks.push(BasicBlock { statements: vec![], terminator: new_term });
             }
         };
     }
 
-    /// Insert statement before or after the source instruction and update the source as needed.
+    /// Insert basic block before or after the source instruction and update `source` accordingly. If
+    /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as
+    /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the
+    /// terminator of the newly inserted basic block.
+    pub fn insert_bb(
+        &mut self,
+        mut bb: BasicBlock,
+        source: &mut SourceInstruction,
+        position: InsertPosition,
+    ) {
+        // Splitting adds 1 block, so the added block index is len + 1;
+        let split_bb_idx = self.blocks().len();
+        let inserted_bb_idx = self.blocks().len() + 1;
+        // Update the terminator of the basic block to point at the remaining part of the split
+        // basic block.
+        let target = get_mut_target_ref(&mut bb.terminator);
+        *target = split_bb_idx;
+        let new_term = Terminator {
+            kind: TerminatorKind::Goto { target: inserted_bb_idx },
+            span: source.span(&self.blocks),
+        };
+        self.split_bb(source, position, new_term);
+        self.blocks.push(bb);
+    }
+
+    pub fn insert_terminator(
+        &mut self,
+        source: &mut SourceInstruction,
+        position: InsertPosition,
+        terminator: Terminator,
+    ) {
+        self.split_bb(source, position, terminator);
+    }
+
+    /// Insert statement before or after the source instruction and update the source as needed. If
+    /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as
+    /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the
+    /// newly inserted statement.
     pub fn insert_stmt(
         &mut self,
         new_stmt: Statement,
@@ -338,22 +377,18 @@ impl MutableBody {
                     SourceInstruction::Terminator { bb } => {
                         // Create a new basic block, as we need to append a statement after the terminator.
                         let current_terminator = &mut self.blocks.get_mut(*bb).unwrap().terminator;
-                        // Kani can only instrument function calls in this way.
-                        match &mut current_terminator.kind {
-                            TerminatorKind::Call { target: Some(target_bb), .. } => {
-                                *source = SourceInstruction::Statement { idx: 0, bb: new_bb_idx };
-                                let new_bb = BasicBlock {
-                                    statements: vec![new_stmt],
-                                    terminator: Terminator {
-                                        kind: TerminatorKind::Goto { target: *target_bb },
-                                        span,
-                                    },
-                                };
-                                *target_bb = new_bb_idx;
-                                self.blocks.push(new_bb);
-                            }
-                            _ => unimplemented!("Kani can only insert statements after calls."),
+                        // Update target of the terminator.
+                        let target_bb = get_mut_target_ref(current_terminator);
+                        *source = SourceInstruction::Statement { idx: 0, bb: new_bb_idx };
+                        let new_bb = BasicBlock {
+                            statements: vec![new_stmt],
+                            terminator: Terminator {
+                                kind: TerminatorKind::Goto { target: *target_bb },
+                                span,
+                            },
                         };
+                        *target_bb = new_bb_idx;
+                        self.blocks.push(new_bb);
                     }
                 }
             }
@@ -574,3 +609,15 @@ pub trait MutMirVisitor {
         }
     }
 }
+
+fn get_mut_target_ref(terminator: &mut Terminator) -> &mut BasicBlockIdx {
+    match &mut terminator.kind {
+        TerminatorKind::Assert { target, .. }
+        | TerminatorKind::Drop { target, .. }
+        | TerminatorKind::Goto { target }
+        | TerminatorKind::Call { target: Some(target), .. } => target,
+        _ => unimplemented!(
+            "Kani can only insert instructions after terminators that have a `target` field."
+        ),
+    }
+}
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
index 4f94f94d17f1..f46c143f16d1 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
@@ -230,7 +230,7 @@ impl UninitPass {
                     *pointee_info.ty(),
                 );
                 collect_skipped(&operation, body, skip_first);
-                body.add_call(
+                body.insert_call(
                     &is_ptr_initialized_instance,
                     source,
                     operation.position(),
@@ -257,7 +257,7 @@ impl UninitPass {
                 let layout_operand =
                     mk_layout_operand(body, source, operation.position(), &element_layout);
                 collect_skipped(&operation, body, skip_first);
-                body.add_call(
+                body.insert_call(
                     &is_ptr_initialized_instance,
                     source,
                     operation.position(),
@@ -276,7 +276,7 @@ impl UninitPass {
         // Make sure all non-padding bytes are initialized.
         collect_skipped(&operation, body, skip_first);
         let ptr_operand_ty = ptr_operand.ty(body.locals()).unwrap();
-        body.add_check(
+        body.insert_check(
             tcx,
             &self.check_type,
             source,
@@ -345,7 +345,7 @@ impl UninitPass {
                     *pointee_info.ty(),
                 );
                 collect_skipped(&operation, body, skip_first);
-                body.add_call(
+                body.insert_call(
                     &set_ptr_initialized_instance,
                     source,
                     operation.position(),
@@ -372,7 +372,7 @@ impl UninitPass {
                 let layout_operand =
                     mk_layout_operand(body, source, operation.position(), &element_layout);
                 collect_skipped(&operation, body, skip_first);
-                body.add_call(
+                body.insert_call(
                     &set_ptr_initialized_instance,
                     source,
                     operation.position(),
@@ -408,8 +408,8 @@ impl UninitPass {
             span,
             user_ty: None,
         }));
-        let result = body.new_assignment(rvalue, source, position);
-        body.add_check(tcx, &self.check_type, source, position, result, reason);
+        let result = body.insert_assignment(rvalue, source, position);
+        body.insert_check(tcx, &self.check_type, source, position, result, reason);
     }
 }
 
@@ -432,7 +432,7 @@ pub fn mk_layout_operand(
     layout_byte_mask: &[bool],
 ) -> Operand {
     Operand::Move(Place {
-        local: body.new_assignment(
+        local: body.insert_assignment(
             Rvalue::Aggregate(
                 AggregateKind::Array(Ty::bool_ty()),
                 layout_byte_mask
@@ -531,7 +531,7 @@ fn inject_memory_init_setup(
     )
     .unwrap();
 
-    new_body.add_call(
+    new_body.insert_call(
         &memory_initialization_init,
         &mut source,
         InsertPosition::Before,
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs
index 4c768aa2ee81..10a93b727a77 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs
@@ -57,7 +57,7 @@ impl MemoryInitOp {
                         Operand::Copy(place) | Operand::Move(place) => place,
                         Operand::Constant(_) => unreachable!(),
                     };
-                    body.new_assignment(
+                    body.insert_assignment(
                         Rvalue::AddressOf(Mutability::Not, place.clone()),
                         source,
                         self.position(),
diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs
index a7d0f14d270f..a81f76d25393 100644
--- a/kani-compiler/src/kani_middle/transform/check_values.rs
+++ b/kani-compiler/src/kani_middle/transform/check_values.rs
@@ -85,13 +85,13 @@ impl ValidValuePass {
         for operation in instruction.operations {
             match operation {
                 SourceOp::BytesValidity { ranges, target_ty, rvalue } => {
-                    let value = body.new_assignment(rvalue, &mut source, InsertPosition::Before);
+                    let value = body.insert_assignment(rvalue, &mut source, InsertPosition::Before);
                     let rvalue_ptr = Rvalue::AddressOf(Mutability::Not, Place::from(value));
                     for range in ranges {
                         let result = build_limits(body, &range, rvalue_ptr.clone(), &mut source);
                         let msg =
                             format!("Undefined Behavior: Invalid value of type `{target_ty}`",);
-                        body.add_check(
+                        body.insert_check(
                             tcx,
                             &self.check_type,
                             &mut source,
@@ -106,7 +106,7 @@ impl ValidValuePass {
                         let result = build_limits(body, &range, rvalue.clone(), &mut source);
                         let msg =
                             format!("Undefined Behavior: Invalid value of type `{pointee_ty}`",);
-                        body.add_check(
+                        body.insert_check(
                             tcx,
                             &self.check_type,
                             &mut source,
@@ -139,8 +139,8 @@ impl ValidValuePass {
             span,
             user_ty: None,
         }));
-        let result = body.new_assignment(rvalue, source, InsertPosition::Before);
-        body.add_check(tcx, &self.check_type, source, InsertPosition::Before, result, reason);
+        let result = body.insert_assignment(rvalue, source, InsertPosition::Before);
+        body.insert_check(tcx, &self.check_type, source, InsertPosition::Before, result, reason);
     }
 }
 
@@ -771,24 +771,25 @@ pub fn build_limits(
     let span = source.span(body.blocks());
     debug!(?req, ?rvalue_ptr, ?span, "build_limits");
     let primitive_ty = uint_ty(req.size.bytes());
-    let start_const = body.new_const_operand(req.valid_range.start, primitive_ty, span);
-    let end_const = body.new_const_operand(req.valid_range.end, primitive_ty, span);
+    let start_const = body.new_uint_operand(req.valid_range.start, primitive_ty, span);
+    let end_const = body.new_uint_operand(req.valid_range.end, primitive_ty, span);
     let orig_ptr = if req.offset != 0 {
-        let start_ptr = move_local(body.new_assignment(rvalue_ptr, source, InsertPosition::Before));
-        let byte_ptr = move_local(body.new_cast_ptr(
+        let start_ptr =
+            move_local(body.insert_assignment(rvalue_ptr, source, InsertPosition::Before));
+        let byte_ptr = move_local(body.insert_ptr_cast(
             start_ptr,
             Ty::unsigned_ty(UintTy::U8),
             Mutability::Not,
             source,
             InsertPosition::Before,
         ));
-        let offset_const = body.new_const_operand(req.offset as _, UintTy::Usize, span);
-        let offset = move_local(body.new_assignment(
+        let offset_const = body.new_uint_operand(req.offset as _, UintTy::Usize, span);
+        let offset = move_local(body.insert_assignment(
             Rvalue::Use(offset_const),
             source,
             InsertPosition::Before,
         ));
-        move_local(body.new_binary_op(
+        move_local(body.insert_binary_op(
             BinOp::Offset,
             byte_ptr,
             offset,
@@ -796,9 +797,9 @@ pub fn build_limits(
             InsertPosition::Before,
         ))
     } else {
-        move_local(body.new_assignment(rvalue_ptr, source, InsertPosition::Before))
+        move_local(body.insert_assignment(rvalue_ptr, source, InsertPosition::Before))
     };
-    let value_ptr = body.new_cast_ptr(
+    let value_ptr = body.insert_ptr_cast(
         orig_ptr,
         Ty::unsigned_ty(primitive_ty),
         Mutability::Not,
@@ -806,13 +807,18 @@ pub fn build_limits(
         InsertPosition::Before,
     );
     let value = Operand::Copy(Place { local: value_ptr, projection: vec![ProjectionElem::Deref] });
-    let start_result =
-        body.new_binary_op(BinOp::Ge, value.clone(), start_const, source, InsertPosition::Before);
+    let start_result = body.insert_binary_op(
+        BinOp::Ge,
+        value.clone(),
+        start_const,
+        source,
+        InsertPosition::Before,
+    );
     let end_result =
-        body.new_binary_op(BinOp::Le, value, end_const, source, InsertPosition::Before);
+        body.insert_binary_op(BinOp::Le, value, end_const, source, InsertPosition::Before);
     if req.valid_range.wraps_around() {
         // valid >= start || valid <= end
-        body.new_binary_op(
+        body.insert_binary_op(
             BinOp::BitOr,
             move_local(start_result),
             move_local(end_result),
@@ -821,7 +827,7 @@ pub fn build_limits(
         )
     } else {
         // valid >= start && valid <= end
-        body.new_binary_op(
+        body.insert_binary_op(
             BinOp::BitAnd,
             move_local(start_result),
             move_local(end_result),
diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
index c4534bf11b4d..d6475465d1b1 100644
--- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
+++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
@@ -136,11 +136,11 @@ impl IntrinsicGeneratorPass {
                     user_ty: None,
                 }));
                 let result =
-                    new_body.new_assignment(rvalue, &mut terminator, InsertPosition::Before);
+                    new_body.insert_assignment(rvalue, &mut terminator, InsertPosition::Before);
                 let reason = format!(
                     "Kani currently doesn't support checking validity of `{target_ty}`. {msg}"
                 );
-                new_body.add_check(
+                new_body.insert_check(
                     tcx,
                     &self.check_type,
                     &mut terminator,
@@ -212,7 +212,7 @@ impl IntrinsicGeneratorPass {
                             InsertPosition::Before,
                             &layout,
                         );
-                        new_body.add_call(
+                        new_body.insert_call(
                             &is_ptr_initialized_instance,
                             &mut terminator,
                             InsertPosition::Before,
@@ -242,7 +242,7 @@ impl IntrinsicGeneratorPass {
                             InsertPosition::Before,
                             &element_layout,
                         );
-                        new_body.add_call(
+                        new_body.insert_call(
                             &is_ptr_initialized_instance,
                             &mut terminator,
                             InsertPosition::Before,
@@ -256,14 +256,14 @@ impl IntrinsicGeneratorPass {
                             span,
                             user_ty: None,
                         }));
-                        let result = new_body.new_assignment(
+                        let result = new_body.insert_assignment(
                             rvalue,
                             &mut terminator,
                             InsertPosition::Before,
                         );
                         let reason: &str = "Kani does not support reasoning about memory initialization of pointers to trait objects.";
 
-                        new_body.add_check(
+                        new_body.insert_check(
                             tcx,
                             &self.check_type,
                             &mut terminator,
@@ -282,11 +282,11 @@ impl IntrinsicGeneratorPass {
                     user_ty: None,
                 }));
                 let result =
-                    new_body.new_assignment(rvalue, &mut terminator, InsertPosition::Before);
+                    new_body.insert_assignment(rvalue, &mut terminator, InsertPosition::Before);
                 let reason = format!(
                     "Kani currently doesn't support checking memory initialization of `{target_ty}`. {msg}"
                 );
-                new_body.add_check(
+                new_body.insert_check(
                     tcx,
                     &self.check_type,
                     &mut terminator,